From 1cdece355c1ac3b19ca2cadba7289bc288b02810 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 19 Feb 2019 10:42:57 +0100
Subject: [PATCH] [Inout] Fixes the operational_inputs on initializations of
const local variables.
Initialized const variables should be included as outputs of the function.
---
src/plugins/inout/operational_inputs.ml | 20 ++++++++++++--------
1 file changed, 12 insertions(+), 8 deletions(-)
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 2cb17a9f311..e1e981e872a 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -285,10 +285,13 @@ end) = struct
{data with over_inputs_d = Zone.join data.over_inputs_d new_inputs}
;;
- let add_out state lv deps data =
+ (* Initialized const variables should be included as outputs of the function,
+ so [for_writing] must be false for local initializations. It should be
+ true for all other instructions. *)
+ let add_out ~for_writing state lv deps data =
let deps, new_outs, exact =
!Db.Value.lval_to_zone_with_deps_state state
- ~deps:(Some deps) ~for_writing:true lv
+ ~deps:(Some deps) ~for_writing lv
in
store_non_terminating_outputs new_outs;
let new_inputs = Zone.diff deps data.under_outputs_d in
@@ -304,7 +307,7 @@ end) = struct
over_inputs_d = Zone.join data.over_inputs_d new_inputs;
over_outputs_d = Zone.join data.over_outputs_d new_outs }
- let transfer_call s dest f args _loc data =
+ let transfer_call ~for_writing s dest f args _loc data =
let state = X.stmt_state s in
let f_inputs, called =
!Db.Value.expr_to_kernel_function_state
@@ -349,7 +352,7 @@ end) = struct
(* Treatment for the possible assignment of the call result *)
(match dest with
| None -> result
- | Some lv -> add_out state lv Zone.bottom result)
+ | Some lv -> add_out ~for_writing state lv Zone.bottom result)
in result
(* Transfer function on instructions. *)
@@ -360,14 +363,14 @@ end) = struct
let e_inputs =
!Db.From.find_deps_no_transitivity_state state exp
in
- add_out state lv e_inputs data
+ add_out ~for_writing:true state lv e_inputs data
| Local_init (v, AssignInit i, _) ->
let state = X.stmt_state stmt in
let rec aux lv i acc =
match i with
| SingleInit e ->
let e_inputs = !Db.From.find_deps_no_transitivity_state state e in
- add_out state lv e_inputs acc
+ add_out ~for_writing:false state lv e_inputs acc
| CompoundInit(ct, initl) ->
let implicit = true in
let doinit o i _ data = aux (Cil.addOffsetLval o lv) i data in
@@ -375,9 +378,10 @@ end) = struct
in
aux (Cil.var v) i data
| Call (lvaloption,funcexp,argl,loc) ->
- transfer_call stmt lvaloption funcexp argl loc data
+ transfer_call ~for_writing:true stmt lvaloption funcexp argl loc data
| Local_init(v, ConsInit(f, args, kind), loc) ->
- Cil.treat_constructor_as_func (transfer_call stmt) v f args kind loc data
+ let transfer = transfer_call ~for_writing:false stmt in
+ Cil.treat_constructor_as_func transfer v f args kind loc data
| Asm _ | Code_annot _ | Skip _ -> data
;;
--
GitLab