2021-02-24 19:29 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000245Frama-CKernelpublic2014-02-12 16:56
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000245: Blocks are removed from the AST
DescriptionSome blocks are removed from the AST. This makes the value analysis incorrect wrt block-local variables.

int R,*p,S,*q;

void main(int c, int d)
{
  int a,i;
  a=2;
  p = q = &a;
  // for(i=0; i<2; i++)
  {
    int u=a;
    p = &u;
      toto:
    {
      int v;
      v = 3;
      v++;
      q = &v;
    }
  }
  if (c) R = *p;
  if (d) S = *q;
  // if (a-a) goto toto;
}

 bin/toplevel.byte -val u.c

  p ? {{}} or ESCAPINGADDR
  q ? {{ &v ;}}

Expected results: q ? {{}} or ESCAPINGADDR

Note that the label on the block participates in the problem.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2009-09-15 19:24 pascal New Issue
2009-09-18 14:40 signoles Status new => assigned
2009-09-18 14:40 signoles Assigned To => virgile
2009-09-24 10:40 svn
2009-09-24 10:40 svn Status assigned => resolved
2009-09-24 10:40 svn Resolution open => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron
2013-12-19 01:13 Source_changeset_attached => framac master 11535dfc
2014-02-12 16:56 Source_changeset_attached => framac stable/neon 11535dfc
+Issue History