Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] [Jessie] loop invariant
- Subject: [Frama-c-discuss] [Jessie] loop invariant
- From: dmentre at linux-france.org (David MENTRE)
- Date: Wed, 18 Sep 2013 10:15:51 +0200
- In-reply-to: <CAEtoXR1+Y1C9rU5b-tJouTmGn6bCKFWiZZrJ5mNDxY10LGsnHg@mail.gmail.com>
- References: <CAEtoXR21n9RPnwGE_UQ7zDjqrNPjhhRMuG5kQdzM=SjH7z+9CA@mail.gmail.com> <52162B8A.4080703@inria.fr> <CAEtoXR2DsVLvtKZM9PiFNPxx-=w11eY0sr2WNQ4ymdv74P-h4A@mail.gmail.com> <5216629A.5080303@inria.fr> <CAEtoXR3XiHDCd49mKyKh4GLL6ozO48u97AmeMc5qSCrhhgthow@mail.gmail.com> <CA+yPOViR89rE7Bg5Zkx5Lu5PQs8xz6RDAhSBZ1m-afYzgdgVAA@mail.gmail.com> <522AEA5A.3080809@inria.fr> <522AEE91.5080402@inria.fr> <CAEtoXR3-R2u+0CVmN7t4dwiO_-kDyK3s7DMFrLdvonsZboEqaQ@mail.gmail.com> <52342B94.9070309@inria.fr> <CAEtoXR1+Y1C9rU5b-tJouTmGn6bCKFWiZZrJ5mNDxY10LGsnHg@mail.gmail.com>
Hello, 2013/9/17 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>: > After inserting the two annotations below, there were some not proved VCs > (401/405): > assigns Gbl_Eventos[9].Gbl_Ativo; There is no "Gbl_Eventos" variable in the code you sent. You probably meant: assigns Eventos[9].Ativo; > ensures (pri == 1) && (ID == 1) && (\old(Eventos[9].Ativo) == 0) && > average > 12.0 ==> Eventos[9].Ativo == 1; I cannot test as I don't have Jessie installed so take my remarks with a grain of salt. Jessie loops are somewhat "opaque", so you need to state in loop invariants properties that are true when entering the loop, even if the loop does not modify this property, e.g. "loop invariant pri == 1". The best way to debug such cases is to add various assert in your code to check that properties you think are true at a given code point are indeed seen true by Jessie (or WP or Value analysis). You can for example try to add "assert pri == 1;" before and within the for loop. I hope it helps, Best regards, david
- References:
- [Frama-c-discuss] [Jessie] loop invariant
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] [Jessie] loop invariant
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] [Jessie] loop invariant
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] [Jessie] loop invariant
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] [Jessie] loop invariant
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] [Jessie] loop invariant
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] [Jessie] loop invariant
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] [Jessie] loop invariant
- Prev by Date: [Frama-c-discuss] Patch for ocaml 4.01.0
- Next by Date: [Frama-c-discuss] Jessie3 detecting issue Z3,3.2
- Previous by thread: [Frama-c-discuss] [Jessie] loop invariant
- Next by thread: [Frama-c-discuss] How would one annotate a function in an external header?
- Index(es):