Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000245Frama-CKernelpublic2009-09-15 19:242014-02-12 16:56
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
There are no notes attached to this issue.

- 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 Checkin
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker