Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001058Frama-CPlug-in > jessiepublic2012-01-04 17:112012-01-04 17:11
Reportervirgile 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0001058: Jessie incorrectly handles labels
DescriptionWhen using \at(x,L) in annotation where L is a C label, Jessie does not put the label at its correct place, resulting in unprovable formulæ.
Steps To ReproduceStarting from the following file:

int f(void) {

  int x = 0;
 L:
  x++;
  //@ assert \at(x,L) == x - 1;

}


frama-c -jessie -jessie-why-opt="-tc" bug.i file.i

produces a correct file.jessie/file.jc but an incorrect file.jessie/why/file.why
(label L gets placed at the beginning of the function).
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2012-01-04 17:11 virgile New Issue
2012-01-04 17:11 virgile Status new => assigned
2012-01-04 17:11 virgile Assigned To => cmarche


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker