From 5ce29e51826ba66c4709449dada064e4d7437faf Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 3 Oct 2019 18:02:40 +0200
Subject: [PATCH] [Kernel] Cabs2Cil - ensures that formals inherit the ghost
status from the function
---
src/kernel_internals/typing/cabs2cil.ml | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 262085f0224..9b466e0e394 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6678,6 +6678,8 @@ and doExp local_env
List.partition (fun d -> not (isGhostFormalVarDecl d) || ghost) argTypesList
in
let args = if ghost then args @ ghost_args else args in
+
+ (* Again, we process arguments in REVERSE order. *)
let (sghost, ghosts') = loopArgs ~are_ghost:true (ghostArgTypes, ghost_args) in
let (sargs, args') = loopArgs (argTypes, args) in
@@ -9020,7 +9022,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
(* Create the formals and add them to the environment. *)
(* sfg: extract tsets for the formals from dt *)
let doFormal (loc : location) ((fn, ft, fa) as fd) =
- let ghost = isGhostFormalVarDecl fd in
+ let ghost = ghost || isGhostFormalVarDecl fd in
let f = makeVarinfo ~ghost ~temp:false false true fn ft in
(f.vdecl <- loc;
f.vattr <- fa;
--
GitLab