2021-02-24 18:46 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001328Frama-CKernel > ACSL implementationpublic2013-04-19 11:05
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0003630

signoles (manager)

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

-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
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
+Issue History