diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 318a78d9638e6accdd2b77bcd46ab3863dba8699..7c5861aa9420ac2df98b4be9602488d1d5e27355 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -260,7 +260,16 @@ module type Transfer = sig
It is None if the call is not recursive.
- [state] is the abstract state at the call site, before the call;
- [valuation] is a cache for all values and locations computed during
- the evaluation of the function and its arguments. *)
+ the evaluation of the function and its arguments.
+
+ On recursive calls, [recursion] contains some substitution of variables
+ to be applied on the domain state to prevent mixing up local variables
+ and formal parameters of different recursive calls.
+ See {!Eval.recursion} for more details.
+ This substitution has been applied on values and expressions in [call],
+ but not in the [valuation] given as argument. If the domain uses some
+ information from the [valuation] on a recursive call, it must apply the
+ substitution on it. *)
val start_call:
stmt -> (location, value) call -> recursion option ->
(value, location, origin) valuation -> state -> state or_bottom
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index e31a140be372267d31bb1b442596d2b15a44064a..80f885d59365f5a7cc965285394b602cf60d6a7e 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -245,6 +245,9 @@ module State = struct
Model.replace_base substitution state
let start_call stmt call recursion valuation (state, clob) =
+ (* Uses the [valuation] to update the [state] before the substitution
+ for recursive calls. *)
+ Cvalue_transfer.update valuation state >>- fun state ->
let state =
match recursion with
| None -> state
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 1e7bedefe0b5a6de16ade918a054f434eefd50ad..26518aa8d7c76a6a249d3c082b9131c453b4bbda 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -204,8 +204,7 @@ let actualize_formals state arguments =
in
List.fold_left treat_one_formal state arguments
-let start_call _stmt call _recursion valuation state =
- let state = update valuation state in
+let start_call _stmt call _recursion _valuation state =
let with_formals = actualize_formals state call.arguments in
let stack_with_call = Value_util.call_stack () in
Db.Value.Call_Value_Callbacks.apply (with_formals, stack_with_call);
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 4bc2213fcca50717d73ea1232bf22b3791f81830..74925890fdce72eaba7ab228afc9f19b2cfe097f 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -479,12 +479,19 @@ module Make
let start_call _stmt call recursion valuation state =
let state =
- match call_init_state call.kf with
- | ISCaller -> assign_formals valuation call state
- | ISFormals -> assign_formals valuation call empty
- | ISEmpty -> empty
+ match recursion with
+ | Some recursion ->
+ (* No relation inferred from the assignment of formal parameters
+ for recursive calls, because the valuation cannot be used safely
+ as the substitution of local and formals variables has not been
+ applied to it. *)
+ start_recursive_call recursion state
+ | None ->
+ match call_init_state call.kf with
+ | ISCaller -> assign_formals valuation call state
+ | ISFormals -> assign_formals valuation call empty
+ | ISEmpty -> empty
in
- let state = Extlib.opt_fold start_recursive_call recursion state in
`Value state
let finalize_call _stmt call _recursion ~pre ~post =
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 8b45d1c11ff3d93957311bea2aebefb4a161b7ec..23cef9f01a25a84154166592159a41ad9281d01c 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1225,8 +1225,8 @@ module D_Impl : Abstract_domain.S
let state =
match function_calls_handling with
| FullInterprocedural ->
- let state = Extlib.opt_fold start_recursive_call recursion state in
- update valuation state
+ update valuation state >>-: fun state ->
+ Extlib.opt_fold start_recursive_call recursion state
| IntraproceduralAll
| IntraproceduralNonReferenced -> `Value G.empty
in
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index b63cce8fc729d45187ac9f79c61de50ef6b5ca4f..e45b1c875de6bb8e1421c9064e1366382cf1982f 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1224,12 +1224,19 @@ module Domain = struct
if intraprocedural ()
then `Value (empty ())
else
- let state = Extlib.opt_fold start_recursive_call recursion state in
let state = { state with modified = Locations.Zone.bottom } in
- let assign_formal state { formal; concrete; avalue } =
- state >>- assign_variable formal concrete avalue valuation
- in
- List.fold_left assign_formal (`Value state) call.arguments
+ match recursion with
+ | Some recursion ->
+ (* No relation inferred from the assignment of formal parameters
+ for recursive calls, because the valuation cannot be used safely
+ as the substitution of local and formals variables has not been
+ applied to it. *)
+ `Value (start_recursive_call recursion state)
+ | None ->
+ let assign_formal state { formal; concrete; avalue } =
+ state >>- assign_variable formal concrete avalue valuation
+ in
+ List.fold_left assign_formal (`Value state) call.arguments
let finalize_call _stmt _call _recursion ~pre ~post =
if intraprocedural ()
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 07872c80f08088ae3a979608cbee6894342a5196..70f2f43cccafd606c62e5c4484da7feb9601dc4d 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -164,8 +164,8 @@ module Internal : Domain_builder.InputDomain
Memory.remove_variables vars state
let start_call _stmt _call recursion valuation state =
- let state = Extlib.opt_fold start_recursive_call recursion state in
- update valuation state
+ update valuation state >>-: fun state ->
+ Extlib.opt_fold start_recursive_call recursion state
let show_expr _valuation _state _fmt _expr = ()
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 03f5bb739613e085951385362ff3b686f4964a2c..bd2fab8b55a914f5c6639aef3a8a5c494a2fc54d 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -568,8 +568,8 @@ module Internal : Domain_builder.InputDomain
Memory.remove_variables vars state
let start_call _stmt _call recursion valuation state =
- let state = Extlib.opt_fold start_recursive_call recursion state in
- update valuation state
+ update valuation state >>-: fun state ->
+ Extlib.opt_fold start_recursive_call recursion state
let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post