From 08d3e926558e53db04482e4e090d9a038a345bfc Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 31 Oct 2019 11:45:32 +0100
Subject: [PATCH] [ghost] Checks consistency of ghost decl/def
---
src/kernel_internals/typing/cabs2cil.ml | 10 +++-
tests/syntax/inconsistent_global_ghost_spec.c | 50 +++++++++++++++++++
...nconsistent_global_ghost_spec.0.res.oracle | 13 +++++
...nconsistent_global_ghost_spec.1.res.oracle | 13 +++++
...nconsistent_global_ghost_spec.2.res.oracle | 13 +++++
...nconsistent_global_ghost_spec.3.res.oracle | 13 +++++
6 files changed, 110 insertions(+), 2 deletions(-)
create mode 100644 tests/syntax/inconsistent_global_ghost_spec.c
create mode 100644 tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
create mode 100644 tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
create mode 100644 tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
create mode 100644 tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 89a968608b2..a411a59c7f2 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2971,8 +2971,14 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
Kernel.debug ~dkey:Kernel.dkey_typing_global
"makeGlobalVarinfo isadef=%B vi.vname=%s(%d), vreferenced=%B"
isadef vi.vname vi.vid vi.vreferenced;
- (* This may throw an exception Not_found *)
- let oldvi, oldloc = lookupGlobalVar vi.vghost vi.vname in
+ (* This may throw an exception Not_found
+ Note that we always search in all the context, including ghost *)
+ let oldvi, oldloc = lookupGlobalVar true vi.vname in
+ if oldvi.vghost <> vi.vghost then
+ abort_context "Inconsistent ghost specification for %s.@ \
+ Previous declaration was at: %a"
+ vi.vname Cil_datatype.Location.pretty oldloc ;
+
Kernel.debug ~dkey:Kernel.dkey_typing_global
" %s(%d) already in the env at loc %a"
vi.vname oldvi.vid Cil_printer.pp_location oldloc;
diff --git a/tests/syntax/inconsistent_global_ghost_spec.c b/tests/syntax/inconsistent_global_ghost_spec.c
new file mode 100644
index 00000000000..8a3aa44011c
--- /dev/null
+++ b/tests/syntax/inconsistent_global_ghost_spec.c
@@ -0,0 +1,50 @@
+/* run.config
+OPT: -cpp-extra-args="-DNON_GHOST_DECL_GHOST_DEF"
+OPT: -cpp-extra-args="-DGHOST_DECL_NON_GHOST_DEF"
+OPT: -cpp-extra-args="-DGHOST_DEF_NON_GHOST_DECL"
+OPT: -cpp-extra-args="-DNON_GHOST_DEF_GHOST_DECL"
+*/
+
+#ifdef NON_GHOST_DECL_GHOST_DEF
+
+void function(void) ;
+/*@ ghost void function(void){ } */
+
+void user(void){
+ function();
+}
+
+#endif
+
+#ifdef GHOST_DECL_NON_GHOST_DEF
+
+/*@ ghost void function(void) ; */
+void function(void){ }
+
+void user(void){
+ function();
+}
+
+#endif
+
+#ifdef GHOST_DEF_NON_GHOST_DECL
+
+/*@ ghost void function(void){ } */
+void function(void) ;
+
+void user(void){
+ function();
+}
+
+#endif
+
+#ifdef NON_GHOST_DEF_GHOST_DECL
+
+void function(void){ }
+/*@ ghost void function(void) ; */
+
+void user(void){
+ function();
+}
+
+#endif
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
new file mode 100644
index 00000000000..1a6ff7363d2
--- /dev/null
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/inconsistent_global_ghost_spec.c (with preprocessing)
+[kernel] tests/syntax/inconsistent_global_ghost_spec.c:11: User Error:
+ Inconsistent ghost specification for function.
+ Previous declaration was at: tests/syntax/inconsistent_global_ghost_spec.c:10
+ 9
+ 10 void function(void) ;
+ 11 /*@ ghost void function(void){ } */
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 12
+ 13 void user(void){
+[kernel] User Error: stopping on file "tests/syntax/inconsistent_global_ghost_spec.c" that has
+ errors. Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
new file mode 100644
index 00000000000..f44d6920240
--- /dev/null
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/inconsistent_global_ghost_spec.c (with preprocessing)
+[kernel] tests/syntax/inconsistent_global_ghost_spec.c:22: User Error:
+ Inconsistent ghost specification for function.
+ Previous declaration was at: tests/syntax/inconsistent_global_ghost_spec.c:21
+ 20
+ 21 /*@ ghost void function(void) ; */
+ 22 void function(void){ }
+ ^^^^^^^^^^^^^^^^^^^^^^
+ 23
+ 24 void user(void){
+[kernel] User Error: stopping on file "tests/syntax/inconsistent_global_ghost_spec.c" that has
+ errors. Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
new file mode 100644
index 00000000000..ce9a25fb882
--- /dev/null
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/inconsistent_global_ghost_spec.c (with preprocessing)
+[kernel] tests/syntax/inconsistent_global_ghost_spec.c:33: User Error:
+ Inconsistent ghost specification for function.
+ Previous declaration was at: tests/syntax/inconsistent_global_ghost_spec.c:32
+ 31
+ 32 /*@ ghost void function(void){ } */
+ 33 void function(void) ;
+ ^^^^^^^^^^^^^^^^^^^^^
+ 34
+ 35 void user(void){
+[kernel] User Error: stopping on file "tests/syntax/inconsistent_global_ghost_spec.c" that has
+ errors. Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
new file mode 100644
index 00000000000..70bc963d684
--- /dev/null
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/inconsistent_global_ghost_spec.c (with preprocessing)
+[kernel] tests/syntax/inconsistent_global_ghost_spec.c:44: User Error:
+ Inconsistent ghost specification for function.
+ Previous declaration was at: tests/syntax/inconsistent_global_ghost_spec.c:43
+ 42
+ 43 void function(void){ }
+ 44 /*@ ghost void function(void) ; */
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 45
+ 46 void user(void){
+[kernel] User Error: stopping on file "tests/syntax/inconsistent_global_ghost_spec.c" that has
+ errors. Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
--
GitLab