--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on March 2009 ---
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; } === All invariant and properties are proven without any issue using alt-ergo, especially the assertion "assert total >= counters[0];". Now my real program is like this (I have deleted uneeded lines) : === #define MAX_CANDIDATES 20 #define MAX_VOTES_PER_CANDIDATE 100000 int num_candidates; int counters[MAX_CANDIDATES] = { 0, }; [...] /*@ requires 0 < num_candidates && num_candidates < MAX_CANDIDATES; requires \forall int i; 0 <= i < MAX_CANDIDATES ==> counters[i] < MAX_VOTES_PER_CANDIDATE && counters[i] >= 0; assigns \nothing; */ void compute_results(void) { int total = 0; int i, winner, valid_total; /*@ loop invariant 0 <= i && i <= num_candidates; loop invariant 0 <= counters[i] < MAX_VOTES_PER_CANDIDATE; loop invariant total >= 0; loop invariant total <= i * MAX_VOTES_PER_CANDIDATE; */ for (i = 0; i < num_candidates; i++) { total += counters[i]; } //@ assert total < MAX_CANDIDATES * MAX_VOTES_PER_CANDIDATE; //@ assert total >= counters[0]; //@ assert counters[0] >= 0; valid_total = total - counters[0]; } === 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! What I am missing? Is there something I haven't seen? Many thanks in advance for any light, Sincerely yours, david PS: I can provide the full code on request, I just don't want to make it public.