Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001047Frama-CPlug-in > jessiepublic2011-12-12 15:432011-12-12 15:43
Reporterchernikova 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in Version 
Summary0001047: labels defined before loops and used after loops are not correctly translated in jessie
DescriptionAn example with a label in a ghost (or not) statement: void main(){ int p = 1; int i; //@ ghost L: for (i=0; i<10; i++) p = 2; //@ assert \at(p,L)==p-1; } frama-c -jessie labels-bug.c results as: ... File "labels-bug.jc", line 52, characters 38-46: typing error: label `L' not found ... labels-bug.jc contains label L: .... (C_1 : (p = 1)); (L : ()); (C_2 : (i = 0)); loop while (true) { ... }; (while_0_break : ()); { (assert for default: (C_7 : (\at(p,L) == (p - 1)))); () };
TagsNo tags attached.
Attached Filesc file icon labels-bug.c [^] (118 bytes) 2011-12-12 15:43 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-12-12 15:43 chernikova New Issue
2011-12-12 15:43 chernikova Status new => assigned
2011-12-12 15:43 chernikova Assigned To => cmarche
2011-12-12 15:43 chernikova File Added: labels-bug.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker