Frama-C Bug Tracking System - Frama-C
View Issue Details
0001062Frama-CPlug-in > jessiepublic2012-01-12 11:462012-01-12 11:46
karpulevich 
cmarche 
normalmajoralways
assignedopen 
Frama-C Nitrogen-20111001 
 
0001062: Jessie incorrectly handles initialization of static array with {} initialization
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.
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).
No tags attached.
has duplicate 0001061closed cmarche Jessie incorrectly handles initialization of array 
Issue History
2012-01-12 11:46karpulevichNew Issue
2012-01-12 11:46karpulevichStatusnew => assigned
2012-01-12 11:46karpulevichAssigned To => cmarche
2012-07-05 00:04yakobowskiRelationship addedhas duplicate 0001061

There are no notes attached to this issue.