Jessie incorrectly handles initialization of array

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

---

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

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

Description :

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

Additional Information :

Starting from the following file:

//@ ensures \result = 1; int init_array() { int arr[] = {1, 2, 3}; //assert arr[0] == 1; //forall integer i; 0 <= i < 3 ==> arr[i] < 4;

return arr[0]; }

frama-c -jessie file.i

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