Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001062Frama-CPlug-in > jessiepublic2012-01-12 11:462012-01-12 11:46
Reporterkarpulevich 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001062: Jessie incorrectly handles initialization of static array with {} initialization
DescriptionWhen 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 InformationStarting 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).
TagsNo tags attached.
Attached Files

- Relationships
has duplicate 0001061closedcmarche Jessie incorrectly handles initialization of array 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2012-01-12 11:46 karpulevich New Issue
2012-01-12 11:46 karpulevich Status new => assigned
2012-01-12 11:46 karpulevich Assigned To => cmarche
2012-07-05 00:04 yakobowski Relationship added has duplicate 0001061


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker