From 10a813abaa45a039ed7a65ae9003be0f74991b7f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 31 Oct 2019 12:10:42 +0100
Subject: [PATCH] [ghost] Using a ghost function in a non-ghost context is an
error
---
src/kernel_internals/typing/cabs2cil.ml | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index a411a59c7f2..a1f20a0caa8 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6505,9 +6505,10 @@ and doExp local_env
(* 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.abort ~current:true
+ "Function %s is a ghost symbol. \
+ It cannot be used in non-ghost context. \
+ Did you forget a /*@@ ghost ... /?" n ;
Kernel.debug ~level:3
"Calling function %s without prototype." n ;
let ftype = TFun(intType, None, false,
--
GitLab