--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on March 2009 ---
Hello, Suppose I have following code: === #define MAX 5 int c[5] = {0, }; int global = 0; void main(void) { //@ assert global == 0; //@ assert \forall integer i; 0 <= i < MAX ==> c[i] == 0; return; } === The two assertions are not proven by Alt-Ergo (\?/ state[1]). However, if I write the code like this: === #define MAX 5 int c[5]; int global; void main(void) { int i; /*@ loop invariant \forall integer j; 0 <= j < i ==> c[j] == 0; loop invariant 0 <= i && i <= MAX; */ for (i = 0; i < MAX; i++) c[i] = 0; global = 0; //@ assert global == 0; //@ assert \forall integer i; 0 <= i < MAX ==> c[i] == 0; return; } === My assertions are correctly proven. Am I forced to do all global initializations manually or I have missed something? This is not a big issue but is a bit cumbersome. I'm calling Jessie like this: frama-c -jessie-analysis -jessie-atp alt-ergo -jessie-cpu-limit 2 -jessie-gui init-issue.c Sincerely yours, david [1] What does that exactly mean? (cf. http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000425.html)