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] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
- Subject: [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
- From: dmentre at linux-france.org (David MENTRE)
- Date: Thu, 19 Mar 2009 09:40:47 +0100
- In-reply-to: <20090318175434.1b258458@is005115>
- References: <3d13dcfc0903180831t1002ccafhfa254b70595fac6a@mail.gmail.com> <20090318175434.1b258458@is005115>
Hello Virgile, On Wed, Mar 18, 2009 at 17:54, Virgile Prevosto <virgile.prevosto at cea.fr> wrote: > if the code of the reduced example is exactly like above, the assertion > is not proved, since the lack of '@' means that it is not seen as an > ACSL annotation. Ohh! I'm ashamed. :-( > If you put back the '@', there is another issue: the > assertion is false. Namely, if you call f with n == 0, the loop is not > entered, and total is still 0 at this point. Ah yes. I realized that in my larger example that's why I wrote the following pre-condition. > Now the larger example has a stronger pre-condition (0< > num_candidates). So why does alt-ergo still fail on the assertion? > Well, remember that the only thing that jessie 'knows' after a loop is > its invariant, I realized that more or less by trial and error. Is this written somewhere in Jessie documentation? I have probably read it but overlooked it. By the way, I have seen that some "global" knowledge is also kept (assertions about global variables? function pre-condition?). Is this correct? Is this described somewhere? > and here the loop invariant is too weak: it gives an > upper bound for total, but no lower bound. A possibility (short of the > ACSL construction \sum which is currently unsupported by jessie) would > be to add the following invariant: > > loop invariant \forall integer j; 0<=j<i ==> total >= counters[j]; Thank you. I'll try that. I have a side question: I usually write \forall assertions with an int: "\forall int i; [...]". You write your assertion with "integer", "\forall integer i; [...]". Is there any difference? Any reason to prefer one over the other? Sincerely yours, david
- Follow-Ups:
- [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
- References:
- [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
- Prev by Date: [Frama-c-discuss] Getting a node from its id for a particular pdg
- Next by Date: [Frama-c-discuss] Semantics of Jessie icons?
- Previous by thread: [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
- Next by thread: [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
- Index(es):