From 506306c787ca5ad588b5a140a17338bd0aedc70c Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 31 Mar 2022 22:57:27 +0200
Subject: [PATCH] [Eva] multidim: more precise oracles for indexes increment
---
src/plugins/value/domains/multidim_domain.ml | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 823572a226e..8b0cbf60dca 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -661,7 +661,7 @@ struct
let update valuation state =
assume_valuation valuation state
- let update_array_segmentation_bounds vi expr (base_map,tracked as state) =
+ let update_array_segmentation_bounds ~oracle vi expr (base_map,tracked) =
let incr = Option.bind expr (fun expr ->
match expr.Cil_types.enode with
| BinOp ((PlusA|PlusPI), { enode=Lval (Var vi', NoOffset) }, exp, _typ)
@@ -678,7 +678,6 @@ struct
(* Very important : oracle must be the oracle before a non-invertible
assignement of the bound to allow removing of eventual empty slice
before the bound leaves the segmentation. *)
- let oracle = mk_oracle state in
let references = snd (BaseMap.find_or_top base_map (Base.of_varinfo vi)) in
let update_ref base base_map =
let update (memory, refs) =
@@ -701,7 +700,7 @@ struct
in
base_map, tracked
- let update_array_segmentation lval expr state =
+ let update_array_segmentation ~oracle lval expr state =
match lval with
| Mem _, _ -> state (* Do nothing *)
| Var vi, offset ->
@@ -709,7 +708,7 @@ struct
| NoOffset -> expr
| _ -> None
in
- update_array_segmentation_bounds vi expr state
+ update_array_segmentation_bounds ~oracle vi expr state
let assign_lval lval assigned_value oracle state =
match Location.of_lval oracle lval with
@@ -728,7 +727,7 @@ struct
let assign _kinstr left expr assigned_value valuation state =
let oracle = valuation_to_oracle state valuation in
- let state = update_array_segmentation left.lval (Some expr) state in
+ let state = update_array_segmentation ~oracle left.lval (Some expr) state in
assume_valuation valuation state >>-: fun state ->
assign_lval left.lval assigned_value oracle state
@@ -775,9 +774,10 @@ struct
List.fold_left enter_one state vars
let leave_scope _kf vars state =
+ let oracle = mk_oracle state in
let state =
List.fold_left
- (fun state vi -> update_array_segmentation_bounds vi None state)
+ (fun state vi -> update_array_segmentation_bounds ~oracle vi None state)
state vars
in
let (base_map,tracked) = state in
--
GitLab