Incorrect AST in presence of local ghost variables
ID0001328: This issue was created automatically from Mantis Issue 1328. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001328 | Frama-C | Kernel > ACSL implementation | public | 2012-12-13 | 2013-04-19 |
| Reporter | signoles | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Fluorine-20130401 |
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; }