Frama-C Bug Tracking System - Frama-C
View Issue Details
0000041Frama-CPlug-in > jessiepublic2009-04-07 15:362009-06-23 18:03
virgile 
cmarche 
normalminoralways
closedfixed 
Frama-C Lithium-20081201 
Frama-C Beryllium-20090601-beta1Frama-C Beryllium-20090601-beta1 
0000041: Inability to prove assigns clauses on simple array code
[bug 7560 from old bts, reported by David Mentré] Hello, With this code: ---- #include #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. Is assigns broken? Boris had a similar issue: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-April/000487.html Yours, d.
No tags attached.
Issue History
2009-04-07 15:36virgileNew Issue
2009-04-07 15:40signolesStatusnew => acknowledged
2009-04-30 16:48monateStatusacknowledged => assigned
2009-04-30 16:48monateAssigned To => cmarche
2009-06-04 15:16cmarcheTarget Version => Frama-C Beryllium
2009-06-18 13:41cmarcheResolutionopen => fixed
2009-06-18 13:42cmarcheStatusassigned => resolved
2009-06-23 18:02signolesStatusresolved => closed
2009-06-23 18:03signolesFixed in Version => Frama-C Beryllium beta-1

There are no notes attached to this issue.