Jessie incorrectly handles initialization of static array with {} initialization

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

---

Id	Project	Category	View	Due Date	Updated
ID0001062	Frama-C	Plug-in > jessie	public	2012-01-12	2012-01-12

Reporter	karpulevich	Assigned To	cmarche	Resolution	open
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Nitrogen-20111001	Target Version	-	Fixed in Version	-

Description :

When using assert arr[0] == 0 in annotation where arr is static array with initialization like this: arr[] = {0, 1}, Jessie does not see information about initialization, resulting in unprovable formula.

Additional Information :

Starting from the following file:

/* @ ensures \result == 1; */ int wtf() { static int a[] = {0,1};

//@ assert a[0] == 0;

a[0] = 5;
return a[1];

}

command: frama-c -jessie file.c

produces a correct file.jessie/file.jc but an incorrect file.jessie/why/file.why (assert doesn't work).