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