From 403765b3a97d96d0be441dd63f09a67eeaedd418 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@inria.fr>
Date: Tue, 27 Nov 2018 11:12:16 +0100
Subject: [PATCH] Ensures that ghost function declarations lead to ghost
formals
---
src/kernel_services/ast_queries/cil.ml | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index c45a165d3b6..8d784488115 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -635,6 +635,13 @@ let makeFormalsVarDecl (n,t,a) =
let setFormalsDecl vi typ =
match unrollType typ with
| TFun(_, Some args, _, _) ->
+ let args = if vi.vghost then
+ let ghost_attr = Attr (frama_c_ghost, []) in
+ let add_attr a = addAttribute ghost_attr a in
+ List.map (fun (n,t,a) -> (n,t, add_attr a)) args
+ else
+ args
+ in
FormalsDecl.replace vi (List.map makeFormalsVarDecl args)
| TFun(_,None,_,_) -> ()
| _ ->
--
GitLab