diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 9d3603ad580f66c8cd71d8077719f12e614061e2..dcd64ed822256755b0a1ccbd1517ca56cc11a8b4 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -412,7 +412,8 @@ module type S = sig
(** Interprets an ACSL extension.
Defined by {!Domain_builder.Complete} as the identity. *)
- val interpret_acsl_extension: acsl_extension -> state -> state
+ val interpret_acsl_extension:
+ acsl_extension -> state logic_environment -> state -> state
(** {3 Scoping and initialization } *)
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 22f0af53515c2639505ceccc9ef7b1e67b1a8a46..3bc961572d72b56d63387af68454bccf5321e833 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -316,7 +316,7 @@ module State = struct
then `Value (state, clob)
else `Bottom
- let interpret_acsl_extension _extension state = state
+ let interpret_acsl_extension _extension _env state = state
let evaluate_from_clause state deps =
(* Evaluates the contents of one element of the from clause, topify them,
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 7c05474f1b52aa6ac83897e36d153974b4b33554..d5b24f78bd2119db70670d9f3344fb9b03660559 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -39,7 +39,8 @@ module type LeafDomain = sig
t Abstract_domain.logic_environment -> t -> predicate -> Alarmset.status
val reduce_by_predicate:
t Abstract_domain.logic_environment -> t -> predicate -> bool -> t or_bottom
- val interpret_acsl_extension: acsl_extension -> t -> t
+ val interpret_acsl_extension:
+ acsl_extension -> t Abstract_domain.logic_environment -> t -> t
val enter_loop: stmt -> t -> t
val incr_loop_counter: stmt -> t -> t
@@ -65,7 +66,7 @@ module Complete (Domain: InputDomain) = struct
let evaluate_predicate _env _state _predicate = Alarmset.Unknown
let reduce_by_predicate _env state _predicate _positive = `Value state
- let interpret_acsl_extension _extension state = state
+ let interpret_acsl_extension _extension _env state = state
let enter_loop _stmt state = state
let incr_loop_counter _stmt state = state
@@ -546,8 +547,8 @@ module Restrict
then Some (f state, mode)
else x
- let interpret_acsl_extension extension =
- lift (Domain.interpret_acsl_extension extension)
+ let interpret_acsl_extension extension env =
+ lift (Domain.interpret_acsl_extension extension (lift_env env))
let enter_scope kind varinfos = lift (Domain.enter_scope kind varinfos)
let leave_scope kf varinfos = lift (Domain.leave_scope kf varinfos)
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index 4c38846e01f0dda328316b9b50f7e51afc662cda..3fd93d211841312e9a2942d363f4f6d00453c304 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -45,7 +45,8 @@ module type LeafDomain = sig
t Abstract_domain.logic_environment -> t -> predicate -> Alarmset.status
val reduce_by_predicate:
t Abstract_domain.logic_environment -> t -> predicate -> bool -> t or_bottom
- val interpret_acsl_extension: acsl_extension -> t -> t
+ val interpret_acsl_extension:
+ acsl_extension -> t Abstract_domain.logic_environment -> t -> t
val enter_loop: stmt -> t -> t
val incr_loop_counter: stmt -> t -> t
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index ceda6361b5f85d06c53ae5f74d12ff7c34babfe5..3adc09a45327fa56e9b929c6e6e79404de03b14a 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -263,9 +263,10 @@ module Make
Right.reduce_by_predicate right_env right pred positive >>-: fun right ->
left, right
- let interpret_acsl_extension extension (left, right) =
- Left.interpret_acsl_extension extension left,
- Right.interpret_acsl_extension extension right
+ let interpret_acsl_extension extension env (left, right) =
+ let left_env, right_env = split_logic_env env in
+ Left.interpret_acsl_extension extension left_env left,
+ Right.interpret_acsl_extension extension right_env right
let enter_scope kind vars (left, right) =
Left.enter_scope kind vars left, Right.enter_scope kind vars right
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 60a72b4b7daf48aebb3fd7a223d676fe7ec76857..d0ef3151485039fa5568cb2655acd903539846d1 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -512,7 +512,7 @@ let interpret_taint_logic (module Abstract: Abstractions.S) : (module Abstractio
in
`Value (Abstract.Dom.set key taint state)
- let interpret_acsl_extension extension state =
+ let interpret_acsl_extension extension _env state =
if String.equal extension.ext_name "taint"
|| String.equal extension.ext_name "taints"
then
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 367c0c0e8e717ebc427a0fa15f1e961d0f06ef74..95f0220637e68f331ec05c47d4f26b7a1ddaf603 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -304,7 +304,8 @@ module type LogicDomain = sig
t Abstract_domain.logic_environment -> t -> predicate -> Alarmset.status
val reduce_by_predicate:
t Abstract_domain.logic_environment -> t -> predicate -> bool -> t or_bottom
- val interpret_acsl_extension: acsl_extension -> t -> t
+ val interpret_acsl_extension:
+ acsl_extension -> t Abstract_domain.logic_environment -> t -> t
end
module Make
@@ -505,8 +506,11 @@ module Make
let states =
eval_and_reduce kf b active k posts states build_prop build_env
in
+ let interpret_extension extension state =
+ Domain.interpret_acsl_extension extension (build_env state) state
+ in
List.fold_left
- (fun acc e -> States.map (Domain.interpret_acsl_extension e) acc)
+ (fun acc e -> States.map (interpret_extension e) acc)
states b.b_extended
in
List.fold_left check_one_behavior post_states behaviors
@@ -711,7 +715,11 @@ module Make
| AVariant _ | AAssigns _ | AAllocation _
| AStmtSpec _ (*TODO*) -> states
| AExtended (_, _, extension) ->
- States.map (Domain.interpret_acsl_extension extension) states
+ let interpret_extension extension state =
+ let env = here_env ~pre:initial_state ~here:state in
+ Domain.interpret_acsl_extension extension env state
+ in
+ States.map (interpret_extension extension) states
end
diff --git a/src/plugins/value/engine/transfer_logic.mli b/src/plugins/value/engine/transfer_logic.mli
index 11ab601df138f23143443caf2af970cb77dbf694..99b9b94b2c6ed12630174866622f5b5e295eb31e 100644
--- a/src/plugins/value/engine/transfer_logic.mli
+++ b/src/plugins/value/engine/transfer_logic.mli
@@ -73,7 +73,8 @@ module type LogicDomain = sig
t Abstract_domain.logic_environment -> t -> predicate -> Alarmset.status
val reduce_by_predicate:
t Abstract_domain.logic_environment -> t -> predicate -> bool -> t or_bottom
- val interpret_acsl_extension: acsl_extension -> t -> t
+ val interpret_acsl_extension:
+ acsl_extension -> t Abstract_domain.logic_environment -> t -> t
end
module Make