Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001328Frama-CKernel > ACSL implementationpublic2012-12-13 09:512013-04-19 11:05
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001328: Incorrect AST in presence of local ghost variables
Description$ less tests/syntax/ghost_lexing.i int G = 0; const char* foo = "foo"; void test(const char */*name*/); void test2(int x) { /*@ ghost int y = 0; if (x>0) { y = x * x; }; */ G = x * x; test(foo); } $ frama-c -print tests/syntax/ghost_lexing.i /* Generated by Frama-C */ int G = 0; char const *foo = "foo"; extern void test(char const *); void test2(int x) { int y; y = 0; if (x > 0) { /*@ ghost y = x * x; */ } G = x * x; test(foo); return; }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0003630)
signoles (manager)
2012-12-18 09:53

The issue occurs for any ghost declaration (even for global declarations).

- Issue History
Date Modified Username Field Change
2012-12-13 09:51 signoles New Issue
2012-12-13 09:51 signoles Status new => assigned
2012-12-13 09:51 signoles Assigned To => virgile
2012-12-18 09:53 signoles Note Added: 0003630
2013-02-01 15:59 svn Checkin
2013-02-01 15:59 svn Status assigned => resolved
2013-02-01 15:59 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker