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: virgile.prevosto at cea.fr (Virgile Prevosto)
- Date: Wed, 18 Mar 2009 17:54:34 +0100
- In-reply-to: <3d13dcfc0903180831t1002ccafhfa254b70595fac6a@mail.gmail.com>
- References: <3d13dcfc0903180831t1002ccafhfa254b70595fac6a@mail.gmail.com>
Le mer 18 mar 2009 16:31:52 CET, David MENTRE <dmentre at linux-france.org> a ?crit : > Hello, > > I have following test case : > === > #define MAX 1000 > #define N 4 > > int counters[N]; > > /*@ requires \forall int i; 0 <= i < N ==> counters[i] >= 0 && > counters[i] < MAX; > requires 0 <= n && n <= N; > assigns \nothing; > */ > int f(int n) > { > int total = 0; > int total_min_0; > int i; > > /*@ loop invariant total >= 0; > loop invariant 0 <= i && i <= n; > loop invariant total <= i * MAX; > */ > for (i = 0; i < n; i++) { > total += counters[i]; > } > > /* assert total >= counters[0]; > */ > total_min_0 = total - counters[0]; > > return total_min_0; > } > > void main(void) > { > counters[0] = 1; > counters[1] = 0; > counters[2] = 3; > counters[3] = 4; > f(N); > return; > } > For me the code is exactly the same as in the reduced test case > (except that "num_candidates" is a global variable instead of a > function parameter). However, on this code, I am unable to prove the > assertion "assert total >= counters[0];", while exactly the same > assertion is proven in the reduced test case without any issue. That's > puzzling me! 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. 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. 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, 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]; Best regards, -- E tutto per oggi, a la prossima volta. Virgile
- 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
- 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
- Prev by Date: [Frama-c-discuss] Getting a node from its id for a particular pdg
- Next by Date: [Frama-c-discuss] Getting a node from its id for a particular pdg
- 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):