diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml index 2422075600dcb2b0715b2e1e9a2fa5210b295a31..1939cabd184c8827aac4c57c5a8b2929fa480466 100644 --- a/src/plugins/e-acsl/src/code_generator/injector.ml +++ b/src/plugins/e-acsl/src/code_generator/injector.ml @@ -568,9 +568,13 @@ let inject_in_fundec main fundec = let kf = try Globals.Functions.get vi with Not_found -> assert false in (* convert ghost variables *) vi.vghost <- false; - List.iter (fun vi -> vi.vghost <- false) fundec.slocals; + let unghost_local vi = + vi.vtype <- Cil.typeRemoveAttributesDeep ["ghost"] vi.vtype ; + vi.vghost <- false + in + List.iter unghost_local fundec.slocals; let unghost_formal vi = - vi.vghost <- false ; + unghost_local vi ; vi.vattr <- Cil.dropAttribute Cil.frama_c_ghost_formal vi.vattr in List.iter unghost_formal fundec.sformals; @@ -602,6 +606,7 @@ let unghost_vi vi = (* do not convert extern ghost variables, because they can't be linked, see bts #1392 *) if vi.vstorage <> Extern then vi.vghost <- false; + vi.vtype <- Cil.typeRemoveAttributesDeep ["ghost"] vi.vtype ; match Cil.unrollType vi.vtype with | TFun(res, Some l, va, attr) -> (* unghostify function's parameters *) diff --git a/src/plugins/e-acsl/tests/constructs/ghost.i b/src/plugins/e-acsl/tests/constructs/ghost.i index 18ac737e97542b1211c83c895183393224314927..9f76188f2356ebab7a7499902a9e3ab8de30b030 100644 --- a/src/plugins/e-acsl/tests/constructs/ghost.i +++ b/src/plugins/e-acsl/tests/constructs/ghost.i @@ -3,13 +3,13 @@ */ /*@ ghost int G = 0; */ -/*@ ghost int *P; */ +/*@ ghost int \ghost *P; */ // /*@ ghost int foo(int *x) { return *x + 1; } */ int main(void) { /*@ ghost P = &G; */ ; - /*@ ghost int *q = P; */ + /*@ ghost int \ghost *q = P; */ /*@ ghost (*P)++; */ /*@ assert *q == G; */ // /*@ ghost G = foo(&G); */ diff --git a/src/plugins/variadic/tests/declared/called_in_ghost.i b/src/plugins/variadic/tests/declared/called_in_ghost.i index 5526129011507eacfdd38c4dc89734cc8958e40d..7d6ccc4f7f67ae5be501a3d5806fb645b6219623 100644 --- a/src/plugins/variadic/tests/declared/called_in_ghost.i +++ b/src/plugins/variadic/tests/declared/called_in_ghost.i @@ -1,6 +1,7 @@ /* run.config - OPT: -load-script tests/declared/called_in_ghost.ml -print + OPT: -kernel-warn-key ghost:bad-use=inactive -load-script tests/declared/called_in_ghost.ml -print */ +// Note: we deactivate "ghost:bad-use" to check that printing goes right /*@ assigns \nothing ; */ void function(int e, ...);