diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index b1b06f70f1de294cd7e568cd67b2a971da8feb78..cc7d69a289e2b01cb05a874c13a16a31bab624e0 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -358,12 +358,13 @@ module type S = sig
(** Logical evaluation. This API is subject to changes. *)
(* TODO: cooperative evaluation of predicates in the engine. *)
- (** [logic_assign from loc_asgn pre state] applies the effect of the
- [assigns ... \from ...] clause [from] to [state]. [pre] is the state
- before the assign clauses, in which the terms of the clause are evaluated.
- [loc_asgn] is the result of the evaluation of the [assigns] part of [from]
- in [pre]. *)
- val logic_assign: logic_assign -> location -> pre:state -> state -> state
+ (** [logic_assign None loc state] removes from [state] all inferred properties
+ that depend on the memory location [loc].
+ If the first argument is not None, it contains the logical clause being
+ interpreted and the pre-state in which the terms of the clause are
+ evaluated. The clause can be an \assign, \allocated or \free clause.
+ [loc] is then the memory location concerned by the clause. *)
+ val logic_assign: (logic_assign * state) option -> location -> state -> state
(** Evaluates a [predicate] to a logical status in the current [state].
The [logic_environment] contains the states at some labels and the
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index c9fd86075f1fcccffea2d705ed1df8241cddd739..c21820f2b2dfa19d7132a2b9f646c38321d72881 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -673,7 +673,7 @@ module Make (Man : Input) = struct
let show_expr _valuation _state _fmt _expr = ()
- let logic_assign _assigns location ~pre:_ state = kill_bases location state
+ let logic_assign _assigns location state = kill_bases location state
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index b5a165f31890864f6d0491dc2c653587f132a9d3..5257e966b8729ffd4b3223a17080b80706964655 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -308,15 +308,19 @@ module State = struct
Printer.pp_from assign pp_eval_error e;
Cvalue.V.top
- let logic_assign logic_assign location ~pre:(pre_state, _) (state, sclob) =
+ let logic_assign logic_assign location (state, sclob) =
match logic_assign with
- | Assigns assign ->
+ | None ->
+ let location = Precise_locs.imprecise_location location
+ and value = Cvalue.V.top in
+ Cvalue.Model.add_binding ~exact:false state location value, sclob
+ | Some (Assigns assign, (pre_state, _)) ->
let location = Precise_locs.imprecise_location location in
let env = Eval_terms.env_assigns pre_state in
let value = evaluate_from_clause env assign in
Locals_scoping.remember_if_locals_in_value sclob location value;
Cvalue.Model.add_binding ~exact:false state location value, sclob
- | Frees _ | Allocates _ -> state, sclob
+ | Some ((Frees _ | Allocates _), _) -> state, sclob
(* ------------------------------------------------------------------------ *)
(* Initialization *)
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 4be9203e8c2f4c0ff6e351757aec427445f57334..a574d3a3c4a82d66b9c5c5844dfada3d02dab530 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -102,7 +102,7 @@ module Make_Minimal
let lval = Cil.var varinfo in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
- let logic_assign _assigns _location ~pre:_ _state = top
+ let logic_assign _assigns _location _state = top
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ t _ _ = `Value t
@@ -239,7 +239,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
let lval = Cil.var varinfo in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
- let logic_assign _assigns _location ~pre:_ _state = top
+ let logic_assign _assigns _location _state = top
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ t _ _ = `Value t
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index 0e8d958ef1dd6fe0dbb2bbc9526d6252af663df3..46331911138dce10ab88edc059e32d695b44c0ac 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -123,8 +123,8 @@ module Make
let show_expr valuation = Domain.show_expr (lift_valuation valuation)
- let logic_assign assigns location ~pre state =
- Domain.logic_assign assigns (Convert.restrict_loc location) ~pre state
+ let logic_assign assigns location state =
+ Domain.logic_assign assigns (Convert.restrict_loc location) state
let evaluate_predicate = Domain.evaluate_predicate
let reduce_by_predicate = Domain.reduce_by_predicate
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index e9894fa2f069890427ec9d54768eecf47e04d85a..06574e327e6fed7fb945168a33b07b20372d9f98 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -227,9 +227,14 @@ module Make
print_one_side fmt right_log Right.name Right.pretty right)
- let logic_assign assign location ~pre:(left_pre, right_pre) (left, right) =
- Left.logic_assign assign location ~pre:left_pre left,
- Right.logic_assign assign location ~pre:right_pre right
+ let logic_assign assign location (left, right) =
+ let left_assign, right_assign =
+ match assign with
+ | None -> None, None
+ | Some (assign, (left, right)) -> Some (assign, left), Some (assign, right)
+ in
+ Left.logic_assign left_assign location left,
+ Right.logic_assign right_assign location right
let lift_logic_env f logic_env =
Abstract_domain.{ states = (fun label -> f (logic_env.states label));
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index f78930c6d92601bcfd31e60239dc47ceac7565a4..b04cd0ffa19955c80a0e67c183af5193509399ff 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -503,7 +503,7 @@ module Make
| Some equality -> Equality.Equality.pretty fmt equality
| None -> ()
- let logic_assign _assigns location ~pre:_ state =
+ let logic_assign _assigns location state =
let loc = Precise_locs.imprecise_location location in
let zone = Locations.(enumerate_valid_bits Write loc) in
kill Hcexprs.Modified zone state
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 3b60576b8157c6a06a7c9df8f92de01e185e1b5e..4c8dec87e1ecf236a920ef4eb38a1134f3a6ceb7 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1296,7 +1296,7 @@ module D_Impl : Abstract_domain.S
let initialize_variable _ _ ~initialized:_ _ state = state
(* Logic *)
- let logic_assign _assigns location ~pre:_ state = kill location state
+ let logic_assign _assigns location state = kill location state
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index da068efc2f9b332de553c61e6d909d1fcc5d7381..5bbf25ba1ff5dc18b3f392d07d6d25b5d35c4fcf 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -261,7 +261,7 @@ module Internal
let initialize_variable_using_type _ _ state = state
(* TODO *)
- let logic_assign _assign _location ~pre:_ _state = top
+ let logic_assign _assign _location _state = top
(* Logic *)
let evaluate_predicate _ _ _ = Alarmset.Unknown
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 853183f0d398055d4a1e6d57a4bfaa00a49c49b5..b1faca4b4d688ab17f84382b814b3b23c4206a6b 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1235,7 +1235,7 @@ module Domain = struct
let show_expr _valuation _state _fmt _expr = ()
- let logic_assign _logic_assign location ~pre:_ state =
+ let logic_assign _logic_assign location state =
let loc = Precise_locs.imprecise_location location in
let zone = Locations.(enumerate_valid_bits Write loc) in
let state = kill zone state in
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 4d8a15d53eba5c6c7ace3746c759011de0f1d28b..cb7c583d9e8aa74a6008cbd9a746de1f3223d8ad 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -216,7 +216,7 @@ module Internal : Domain_builder.InputDomain
let initialize_variable _ _ ~initialized:_ _ state = state
(* Logic *)
- let logic_assign _assign location ~pre:_ state =
+ let logic_assign _assign location state =
let loc = Precise_locs.imprecise_location location in
kill loc state
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 20f91dc4a9992519580c145c2293034678f98bb5..f2e84f2c345451919a483d69b896082546acb526 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -300,7 +300,7 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
let incr_loop_counter _ state = state
let leave_loop _ state = state
- let logic_assign _assign location ~pre:_ state = remove location state
+ let logic_assign _assign location state = remove location state
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 91b53803645608e876c6e66d40a581d37dff92ba..9464308a6e2d57bed2ad1a649186983298815d56 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -631,7 +631,7 @@ module Internal : Domain_builder.InputDomain
let initialize_variable _ _ ~initialized:_ _ state = state
(* Logic *)
- let logic_assign _assigns location ~pre:_ state =
+ let logic_assign _assigns location state =
let loc = Precise_locs.imprecise_location location in
Memory.kill loc state
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 4c533c30c2c260dfbd0c9d383599576a17be9d32..de5887617b6b296e62609fe8fbe67d6ae974e4fb 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -931,7 +931,7 @@ module Internal = struct
Traces.add_trans state (Msg msg)
(* TODO *)
- let logic_assign _assign _location ~pre:_ state =
+ let logic_assign _assign _location state =
Traces.add_trans state (Msg "logic assign")
(* Logic *)
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 5d1a55942186ade66365ccbc5164f1c5bbf3e958..c12cdfc9f3cfa03bc6b7b3ac6ef2001b96513110 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -67,7 +67,7 @@ module Make
let finalize_call _ _ ~pre:_ ~post:_ = `Value ()
let show_expr _ _ _ _ = ()
- let logic_assign _ _ ~pre:_ _ = ()
+ let logic_assign _ _ _ = ()
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ _ _ _ = `Value ()
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index d84a01a562d01814e83e121f2c0deb60109e5a05..4521648ffbbe9efce1e5e6a20a06226aba7309fb 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -267,7 +267,7 @@ module Make
let env = make_env state in
let assigns_with_locations = evaluate_locations env retres_loc assigns in
let transfer state (logic_assign, location) =
- Domain.logic_assign logic_assign location ~pre state
+ Domain.logic_assign (Some (logic_assign, pre)) location state
in
List.fold_left transfer state assigns_with_locations