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
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityhave not tried
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker