From 8b1aa75926266e82d03265f699a3581472d55ae7 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 28 Oct 2019 11:42:31 +0100
Subject: [PATCH] [ghost] specialized error msg when ghost symbol appears in
non-ghost context
---
src/kernel_internals/typing/cabs2cil.ml | 23 +++++++++++++++----
tests/syntax/ghost_local_ill_formed.i | 6 +++++
.../oracle/ghost_local_ill_formed.res.oracle | 2 ++
3 files changed, 27 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index c0aa7ec4d8c..70b3ca2ccd9 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1085,6 +1085,12 @@ let lookupVar ghost name =
| (EnvVar vi), loc -> vi, loc
| _ -> raise Not_found
+let only_ghost_symbol name =
+ try ignore (lookupVar false name); false
+ with Not_found ->
+ try ignore (lookupVar true name); true
+ with Not_found -> false
+
let lookupGlobalVar ghost name =
let env = if ghost then ghost_global_env else global_env in
match Datatype.String.Hashtbl.find env name with
@@ -5687,13 +5693,18 @@ and doExp local_env
| _ -> raise Not_found
with Not_found -> begin
if isOldStyleVarArgName n then
- Kernel.fatal ~current:true
+ Kernel.abort ~current:true
"Cannot resolve variable %s. \
- This could be a CIL bug due to the handling of old-style variable argument \
- functions"
+ This could be a CIL bug due to \
+ the handling of old-style variable argument functions"
n
+ else if only_ghost_symbol n then
+ Kernel.abort ~current:true
+ "Variable %s is a ghost symbol. \
+ It cannot be used in non-ghost context. \
+ Did you forget a /*@@ ghost ... /?" n
else
- Kernel.fatal ~current:true "Cannot resolve variable %s" n
+ Kernel.abort ~current:true "Cannot resolve variable %s" n
end
end
| A.INDEX (e1, e2) -> begin
@@ -6487,6 +6498,10 @@ and doExp local_env
new_exp ~loc:f.expr_loc (Lval(var vi)), vi.vtype)
(* Found. Do not use finishExp. Simulate what = AExp None *)
with Not_found -> begin
+ if only_ghost_symbol n then
+ Kernel.warning
+ "calling ghost function %s in non-ghost code. Did you \
+ forget a /*@ ghost ... */ ?" n;
Kernel.debug ~level:3
"Calling function %s without prototype." n ;
let ftype = TFun(intType, None, false,
diff --git a/tests/syntax/ghost_local_ill_formed.i b/tests/syntax/ghost_local_ill_formed.i
index 964f39e9080..d3d786b2880 100644
--- a/tests/syntax/ghost_local_ill_formed.i
+++ b/tests/syntax/ghost_local_ill_formed.i
@@ -10,3 +10,9 @@ void titi() {
/*@ assert \at(c,L1) == 1; */
/*@ assert c == 2; */
}
+
+void toto () {
+ //@ ghost int c = 0;
+ // ill-formed: the instruction should be ghost as well
+ c++;
+}
diff --git a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
index 7e293cd87e7..f1017ea0fd6 100644
--- a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
+++ b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
@@ -2,5 +2,7 @@
[kernel] tests/syntax/ghost_local_ill_formed.i:5: User Error:
redefinition of 'c' in the same scope.
Previous declaration was at tests/syntax/ghost_local_ill_formed.i:2
+[kernel] tests/syntax/ghost_local_ill_formed.i:17: User Error:
+ Variable c is a ghost symbol. It cannot be used in non-ghost context. Did you forget a /*@ ghost ... /?
[kernel] User Error: stopping on file "tests/syntax/ghost_local_ill_formed.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
--
GitLab