Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001135Frama-CKernelpublic2012-03-27 10:522014-02-12 16:59
Reporterpatrick 
Assigned Topatrick 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001135: unrolling loop statements with labels into there annotations are not handled correctly (in conjunction with -ulevel)
DescriptionFresh labels and correct gotos are introduced when unrolling loop statements,
but labels into code annotations are not handled correctly.

Into the given example, the assertion is not unrolled correctly.
Additional Information> cat file.c
int X ;
void main (int c) {
  for (int i = 0 ; i < 10 ;) {
    if (c) goto there ;
    X++;
  there: i++;
    //@ assert c==0 ==> \at(X,there)==i+1;
  }
}

> frama-c file.c -ulevel 1 -print
int X;
void main(int c)
{
  int i;
  i = 0;
  if (! (i < 10)) { goto unrolling_2_loop; }
  if (c) { goto there_unrolling_4_loop; }
  X ++;
  there_unrolling_4_loop: /* internal */ i ++;
  /*@ assert c ? 0 ? \at(X,there) ? i+1; */ ;
  unrolling_3_loop: /* internal */ ;
  while (i < 10) {
    if (c) { goto there; }
    X ++;
    there: i ++;
    /*@ assert c ? 0 ? \at(X,there) ? i+1; */ ;
  }
  unrolling_2_loop: /* internal */ ;
  return;
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004710)
patrick (developer)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-03-27 10:52 patrick New Issue
2012-03-27 10:55 patrick Status new => assigned
2012-03-27 10:55 patrick Assigned To => patrick
2012-03-27 11:02 signoles Assigned To patrick => virgile
2012-03-28 08:12 svn Checkin
2012-03-28 08:12 svn Status assigned => resolved
2012-03-28 08:12 svn Resolution open => fixed
2012-04-02 13:59 svn Checkin
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:59 patrick Note Added: 0004710
2014-02-12 16:59 patrick Assigned To virgile => patrick
2014-02-12 16:59 patrick Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker