Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001061Frama-CPlug-in > jessiepublic2012-01-12 10:142012-07-05 00:05
Reporterkarpulevich 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionduplicate 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001061: Jessie incorrectly handles initialization of array
DescriptionWhen 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 InformationStarting 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).
TagsNo tags attached.
Attached Files

- Relationships
duplicate of 0001062assignedcmarche Jessie incorrectly handles initialization of static array with {} initialization 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2012-01-12 10:14 karpulevich New Issue
2012-01-12 10:14 karpulevich Status new => assigned
2012-01-12 10:14 karpulevich Assigned To => cmarche
2012-07-05 00:04 yakobowski Relationship added duplicate of 0001062
2012-07-05 00:05 yakobowski Status assigned => closed
2012-07-05 00:05 yakobowski Resolution open => duplicate


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker