Inability to prove assigns clauses on simple array code

ID0000041: This issue was created automatically from Mantis Issue 41. Further discussion may take place here.

Id	Project	Category	View	Due Date	Updated
ID0000041	Frama-C	Plug-in > jessie	public	2009-04-07	2009-06-23


Reporter	virgile	Assigned To	cmarche	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Lithium-20081201	Target Version	Frama-C Beryllium-20090601-beta1	Fixed in Version	Frama-C Beryllium-20090601-beta1

Description :

[bug 7560 from old bts, reported by David Mentré] Hello,

With this 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.

Is assigns broken?

Yours, d.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

Inability to prove assigns clauses on simple array code

Description :

With this code:

/*@ assigns a[..]; assigns c[..]; */ void main(void) { assign_int(); assign_char(); }

/@ assigns a[..]; assigns c[..]; / void main(void) { assign_int(); assign_char(); }