From 671dd517c2cfccce6e2818192642f07c11cbb4cd Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@inria.fr>
Date: Mon, 26 Nov 2018 10:20:53 +0100
Subject: [PATCH] [Kernel] Assure that queued or changed instructions remains
ghost when needed
---
src/kernel_services/ast_queries/cil.ml | 26 ++++++++++++++++++--------
1 file changed, 18 insertions(+), 8 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 23e9a642239..14dc2695c4b 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -277,13 +277,20 @@ let mkStmt ?(ghost=false) ?(valid_sid=false) ?(sattr=[]) (sk: stmtkind) : stmt =
ghost = ghost;
sattr = sattr;}
-let stmt_of_instr_list ?(loc=Location.unknown) = function
+(* This function is considered unsafe since the ghost parameter can only be
+ taken in account if the list contains at least two elements.
+ It should not be exposed by the API.
+*)
+let unsafe_stmt_of_instr_list ?(loc=Location.unknown) ?(ghost=false) = function
| [] -> Instr (Skip loc)
| [i] -> Instr i
| il ->
- let b = mkBlockNonScoping (List.map (fun i -> mkStmt (Instr i)) il) in
+ let b = mkBlockNonScoping (List.map (fun i -> mkStmt ~ghost (Instr i)) il) in
Block b
+let stmt_of_instr_list ?(loc=Location.unknown) =
+ unsafe_stmt_of_instr_list ~loc ~ghost:false
+
(**** Utility functions ******)
(**** ATTRIBUTES ****)
@@ -2218,8 +2225,8 @@ let flatten_transient_sub_blocks b =
b.bstmts <- List.concat (List.map treat_one_stmt b.bstmts);
b
-let stmt_of_instr_list_visitor ?loc l =
- let res = stmt_of_instr_list ?loc l in
+let stmt_of_instr_list_visitor ?loc ?ghost l =
+ let res = unsafe_stmt_of_instr_list ?loc ?ghost l in
match res with
| Block b -> Block (transient_block b)
| _ -> res
@@ -3351,6 +3358,7 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
(* visit all nodes in a Cil statement tree in preorder *)
and visitCilStmt (vis:cilVisitor) (s: stmt) : stmt =
+ let ghost = s.ghost in
let oldloc = CurrentLoc.get () in
CurrentLoc.set (Stmt.loc s) ;
vis#push_stmt s; (*(vis#behavior.memo_stmt s);*)
@@ -3366,8 +3374,8 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
| _ ->
let b =
mkBlockNonScoping
- ((List.map (fun i -> mkStmt (Instr i)) !toPrepend)
- @ [mkStmt res.skind])
+ ((List.map (fun i -> mkStmt ~ghost (Instr i)) !toPrepend)
+ @ [mkStmt ~ghost res.skind])
in
b.battrs <- addAttribute (Attr (vis_tmp_attr, [])) b.battrs;
(* Make our statement contain the instructions to prepend *)
@@ -3447,7 +3455,8 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
| Instr i ->
begin match fInst i with
| [i'] when i' == i -> s.skind
- | il -> stmt_of_instr_list_visitor ~loc:(Cil_datatype.Instr.loc i) il
+ | il -> stmt_of_instr_list_visitor
+ ~ghost:s.ghost ~loc:(Cil_datatype.Instr.loc i) il
end
| Block b ->
let b' = fBlock b in
@@ -6638,7 +6647,8 @@ let childrenFileSameGlobals vis f =
List.iter
(fun s ->
match s.skind with
- | Instr i -> s.skind <- stmt_of_instr_list (doInstrList [i])
+ | Instr i -> s.skind <-
+ unsafe_stmt_of_instr_list ~ghost:s.ghost (doInstrList [i])
| If (_e, tb, eb, _) ->
peepHole1 doone tb.bstmts;
peepHole1 doone eb.bstmts
--
GitLab