2021-02-27 05:01 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001135Frama-CKernelpublic2012-03-27 10:522014-02-12 16:59
Reporterpatrick 
Assigned Topatrick 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0004710

patrick (developer)

2014-02-12 16:59

 Fix committed to stable/neon branch.
+Notes

-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
2012-03-28 08:12 svn Status assigned => resolved
2012-03-28 08:12 svn Resolution open => fixed
2012-04-02 13:59 svn
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 patrick Source_changeset_attached => framac master 70965aad
2013-12-19 01:12 patrick Source_changeset_attached => framac master 07b38ef2
2014-02-12 16:54 patrick Source_changeset_attached => framac stable/neon 70965aad
2014-02-12 16:54 patrick Source_changeset_attached => framac stable/neon 07b38ef2
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
+Issue History