Frama-C Bug Tracking System - Frama-C
View Issue Details
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

Notes
(0004710)
patrick   
2014-02-12 16:59   
Fix committed to stable/neon branch.

Issue History
2012-03-27 10:52patrickNew Issue
2012-03-27 10:55patrickStatusnew => assigned
2012-03-27 10:55patrickAssigned To => patrick
2012-03-27 11:02signolesAssigned Topatrick => virgile
2012-03-28 08:12svn
2012-03-28 08:12svnStatusassigned => resolved
2012-03-28 08:12svnResolutionopen => fixed
2012-04-02 13:59svn
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2013-12-19 01:12patrickSource_changeset_attached => framac master 70965aad
2013-12-19 01:12patrickSource_changeset_attached => framac master 07b38ef2
2014-02-12 16:54patrickSource_changeset_attached => framac stable/neon 70965aad
2014-02-12 16:54patrickSource_changeset_attached => framac stable/neon 07b38ef2
2014-02-12 16:59patrickNote Added: 0004710
2014-02-12 16:59patrickAssigned Tovirgile => patrick
2014-02-12 16:59patrickStatusclosed => resolved