From db17427204bc3d92b44fac9e840ba88483ceb4b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 26 Nov 2020 10:17:31 +0100
Subject: [PATCH] [kernel] Allows calling builtins Frama_C_show_each & cie in
ghost code.
---
src/kernel_internals/typing/ghost_accesses.ml | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index ce796a384de..6af1cadc349 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -172,16 +172,17 @@ class visitor = object(self)
| { enode = Lval ( (Var vi), NoOffset ) } -> Some vi
| _ -> None
in
+ let is_ghost vi = vi.vghost || Ast_info.is_frama_c_builtin vi.vname in
let failed = match i with
| Call(_, fexp, _, _) ->
begin match call_varinfo fexp with
- | Some fct when not fct.vghost ->
+ | Some fct when not (is_ghost fct) ->
Error.non_ghost_function_call_in_ghost ~current:true () ; true
| None ->
Error.function_pointer_call ~current:true () ; true
| _ -> false
end
- | Local_init(_, ConsInit(fct, _, _), _) when not fct.vghost ->
+ | Local_init(_, ConsInit(fct, _, _), _) when not (is_ghost fct) ->
Error.non_ghost_function_call_in_ghost ~current:true () ; true
| _ -> false
in
--
GitLab