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