From 475f9a906d412ecabfbc75e17d13da6c2923d8ab Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 5 Nov 2019 16:07:16 +0100
Subject: [PATCH] [E-ACSL] Compatibility with ghost qualifier
---
src/plugins/e-acsl/src/code_generator/injector.ml | 9 +++++++--
src/plugins/e-acsl/tests/constructs/ghost.i | 4 ++--
src/plugins/variadic/tests/declared/called_in_ghost.i | 3 ++-
3 files changed, 11 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 2422075600d..1939cabd184 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 18ac737e975..9f76188f235 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 55261290115..7d6ccc4f7f6 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, ...);
--
GitLab