GitLab

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; }