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 - 2019 MantisBT Team
Powered by Mantis Bugtracker