[E-ACSL] Compatibility with ghost qualifier

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 *)

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); */

src/plugins/variadic/tests/declared/called_in_ghost.i

 /* 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, ...);