--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on March 2009 ---
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