--- layout: fc_discuss_archives title: Message 88 from Frama-C-discuss on March 2009 ---
Hello, I have following code: ------ #include <string.h> #define MAX 12 int a[MAX]; char *c[MAX]; /*@ assigns a[..]; */ void assign_int(void) { int i; //@ loop invariant 0 <= i && i <= MAX; for (i = 0; i < MAX; i++) { a[i] = 0x45; } } /*@ assigns c[..]; */ void assign_char(void) { int i; //@ loop invariant 0 <= i && i <= MAX; for (i = 0; i < MAX; i++) { c[i] = strndup("something", MAX); } } /*@ assigns a[..]; assigns c[..]; */ void main(void) { assign_int(); assign_char(); } ------ On this code, I cannot prove properties "assigns a[..];" for assign_int() and "assigns c[..];" for assign_char(). However the assignation seems obvious to me. I have tried "assigns a[0..11];" without success. Could somebody explain to me what I have overlooked? Yours, david