diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index c0aa7ec4d8c4dc503bfcacd4540d6b9f8817bb79..70b3ca2ccd9ce9264e28c12df185b5d771f69073 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 964f39e9080b1b48322ced91f4e64b08284ff3fb..d3d786b2880f1a69d94a0826f3379c43ea25f692 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 7e293cd87e770fb0adfaf4233fed392b3654648e..f1017ea0fd6d2995e921f0f11b879852e02a5d53 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.