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).