diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index a667687b8c603e5f9a1c51a5c2d30d39fde832ba..472f056cf79882aaaa355c67383a1df2da886053 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -260,7 +260,7 @@ module type Transfer = sig
       - [valuation] is a cache for all values and locations computed during
         the evaluation of the function and its arguments. *)
   val start_call:
-    stmt -> (location, value) call ->
+    stmt -> (location, value) call -> recursion option ->
     (value, location, origin) valuation -> state -> state or_bottom
 
   (** [finalize_call stmt call ~pre ~post] computes the state after a function
@@ -271,7 +271,8 @@ module type Transfer = sig
       - [pre] and [post] are the states before and at the end of the call
         respectively. *)
   val finalize_call:
-    stmt -> (location, value) call -> pre:state -> post:state -> state or_bottom
+    stmt -> (location, value) call -> recursion option ->
+    pre:state -> post:state -> state or_bottom
 
   (** Called on the Frama_C_show_each directives. Prints the internal properties
       inferred by the domain in the [state] about the expression [exp]. Can use
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 9c2d3e85184dd5ab65a9e17762df7bb46f081255..9bfd7edafd34c312d3b529bd2ec54e7ce0b3c197 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -634,7 +634,11 @@ module Make (Man : Input) = struct
     with
     | Out_of_Scope _ -> `Value state
 
-  let start_call _stmt call valuation state =
+  let start_call _stmt call recursion valuation state =
+    if recursion <> None
+    then
+      Value_parameters.abort ~current:true
+        "The binding to APRON domains does not support recursive calls.";
     update valuation state >>- fun state ->
     let eval = make_eval state in
     let oracle = make_oracle valuation in
@@ -669,7 +673,7 @@ module Make (Man : Input) = struct
     then `Bottom
     else `Value state
 
-  let finalize_call _stmt _call ~pre:_ ~post = `Value post
+  let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
 
   let show_expr _valuation _state _fmt _expr = ()
 
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 661b972b1ad7cc1f53fefcd7a1541b11d16f2aa4..c7e2889e3df0501e8308c4b128f0b6d4f2570c11 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -230,15 +230,33 @@ module State = struct
     Cvalue_transfer.assume stmt expr positive valuation s >>-: fun s ->
     s, clob
 
-  let start_call stmt call valuation (s, _clob) =
-    Cvalue_transfer.start_call stmt call valuation s >>-: fun state ->
-    state, Locals_scoping.bottom ()
-
-  let finalize_call stmt call ~pre ~post =
-    let (post_state, post_clob) = post
-    and pre_state, clob = pre in
+  let start_recursive_call recursion (state, clob) =
+    let state = Model.remove_variables recursion.withdrawal state in
+    let state = Model.replace_base recursion.base_substitution state in
+    Locals_scoping.substitute recursion.base_substitution clob state
+
+  let start_call stmt call recursion valuation (state, clob) =
+    let state =
+      match recursion with
+      | None -> state
+      | Some recursion -> start_recursive_call recursion (state, clob)
+    in
+    Cvalue_transfer.start_call stmt call recursion valuation state
+    >>-: fun state -> state, Locals_scoping.bottom ()
+
+  let finalize_recursive_call ~pre recursion (state, clob) =
+    let shape = Base.Hptset.shape recursion.base_withdrawal in
+    let inter = Cvalue.Model.filter_by_shape shape pre in
+    let state = Cvalue.Model.merge ~into:state inter in
+    let state = Model.replace_base recursion.base_substitution state in
+    Locals_scoping.substitute recursion.base_substitution clob state, clob
+
+  let finalize_call stmt call recursion ~pre ~post =
+    let pre, clob = pre in
+    let post = Extlib.opt_fold (finalize_recursive_call ~pre) recursion post in
+    let (post, post_clob) = post in
     Locals_scoping.(remember_bases_with_locals clob post_clob.clob);
-    Cvalue_transfer.finalize_call stmt call ~pre:pre_state ~post:post_state
+    Cvalue_transfer.finalize_call stmt call recursion  ~pre ~post
     >>-: fun state ->
     state, clob
 
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 1f2c66726233a8357c3b4bb193f38263caafd06b..1e7bedefe0b5a6de16ade918a054f434eefd50ad 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -204,14 +204,14 @@ let actualize_formals state arguments =
   in
   List.fold_left treat_one_formal state arguments
 
-let start_call _stmt call valuation state =
+let start_call _stmt call _recursion valuation state =
   let state = update valuation state in
   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);
   `Value with_formals
 
-let finalize_call stmt call ~pre:_ ~post:state =
+let finalize_call stmt call _recursion ~pre:_ ~post:state =
   (* Deallocate memory allocated via alloca().
      To minimize computations, only do it for function definitions. *)
   let state' =
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index f19b48efa1217c95f8d54bc13b5930e2a7e4e2f0..62f4e168dc79228f58b3c8650cec68a6b6f12a1a 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -82,10 +82,16 @@ module Make_Minimal
   let assume stmt expr positive _valuation state =
     Domain.assume stmt expr positive state
 
-  let start_call stmt call _valuation state =
-    `Value (Domain.start_call stmt (simplify_call call) state)
-
-  let finalize_call stmt call ~pre ~post =
+  let start_call stmt call recursion _valuation state =
+    match recursion with
+    | None -> `Value (Domain.start_call stmt (simplify_call call) state)
+    | Some _ ->
+      (* TODO *)
+      Value_parameters.abort
+        "The domain %s does not support recursive call." Domain.name
+
+  let finalize_call stmt call recursion ~pre ~post =
+    assert (recursion = None);
     Domain.finalize_call stmt (simplify_call call) ~pre ~post
 
   let show_expr _valuation = Domain.show_expr
@@ -218,9 +224,18 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
       Domain.assign kinstr lv expr value (record valuation) state
     let assume stmt expr positive valuation state =
       Domain.assume stmt expr positive (record valuation) state
-    let start_call stmt call valuation state =
-      `Value (Domain.start_call stmt call (record valuation) state)
-    let finalize_call = Domain.finalize_call
+
+    let start_call stmt call recursion valuation state =
+      match recursion with
+      | None -> `Value (Domain.start_call stmt call (record valuation) state)
+      | Some _ ->
+        (* TODO *)
+        Value_parameters.abort
+          "The domain %s does not support recursive call." Domain.name
+
+    let finalize_call stmt call recursion =
+      assert (recursion = None);
+      Domain.finalize_call stmt call
 
     let show_expr _valuation = Domain.show_expr
 
@@ -436,7 +451,7 @@ module Restrict
      - otherwise, only propagate the state from the call site to kill the
        properties that depend on locations written in the called functions. *)
 
-  let start_call stmt call valuation state =
+  let start_call stmt call recursion valuation state =
     (* Starts the call with mode [new_mode]. [previous_mode] is the current mode
        of the caller. *)
     let start_call_with_mode ?previous_mode ~new_mode state =
@@ -444,7 +459,7 @@ module Restrict
       then
         match previous_mode with
         | Some mode when mode.current.write ->
-          Domain.start_call stmt call valuation state >>-: fun state ->
+          Domain.start_call stmt call recursion valuation state >>-: fun state ->
           Some (state, new_mode)
         | _ ->
           `Value (Some (start_analysis call state, new_mode))
@@ -465,13 +480,13 @@ module Restrict
     | None, None ->
       `Value None
 
-  let finalize_call stmt call ~pre ~post =
+  let finalize_call stmt call recursion ~pre ~post =
     match pre, post with
     | None, _ | _, None -> `Value None
     | Some (pre, pre_mode), Some (post, post_mode) ->
       if post_mode.current.write
       then
-        Domain.finalize_call stmt call ~pre ~post >>-: fun state ->
+        Domain.finalize_call stmt call recursion ~pre ~post >>-: fun state ->
         Some (state, pre_mode)
       else
         `Value (Some (post, pre_mode))
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index 0ff4608c1cdc1bead64778c44b3c8d7d4fe61646..63fe0d3bdf20aea816374463d3a0df398431fafc 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -116,11 +116,12 @@ module Make
   let assume stmt expr positive valuation state =
     Domain.assume stmt expr positive (lift_valuation valuation) state
 
-  let start_call stmt call valuation state =
-    Domain.start_call stmt (lift_call call) (lift_valuation valuation) state
+  let start_call stmt call recursion valuation state =
+    Domain.start_call
+      stmt (lift_call call) recursion (lift_valuation valuation) state
 
-  let finalize_call stmt call ~pre ~post =
-    Domain.finalize_call stmt (lift_call call) ~pre ~post
+  let finalize_call stmt call recursion ~pre ~post =
+    Domain.finalize_call stmt (lift_call call) recursion ~pre ~post
 
   let show_expr valuation = Domain.show_expr (lift_valuation valuation)
 
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 683892ef2dcc07bd5da22c1a3834d06a3437447a..4ea88b8b41f51be54b2ec089efb36e4f948599ed 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -155,18 +155,20 @@ module Make
     Right.assume stmt expr positive (right_val valuation) right >>-: fun right ->
     left, right
 
-  let finalize_call stmt call ~pre ~post =
+  let finalize_call stmt call recursion ~pre ~post =
     let pre_left, pre_right = pre
     and left_state, right_state = post in
-    Left.finalize_call stmt call ~pre:pre_left ~post:left_state
+    Left.finalize_call stmt call recursion ~pre:pre_left ~post:left_state
     >>- fun left ->
-    Right.finalize_call stmt call ~pre:pre_right ~post:right_state
+    Right.finalize_call stmt call recursion ~pre:pre_right ~post:right_state
     >>-: fun right ->
     left, right
 
-  let start_call stmt call valuation (left, right) =
-    Left.start_call stmt call (left_val valuation) left >>- fun left ->
-    Right.start_call stmt call (right_val valuation) right >>-: fun right ->
+  let start_call stmt call recursion valuation (left, right) =
+    Left.start_call stmt call recursion (left_val valuation) left
+    >>- fun left ->
+    Right.start_call stmt call recursion (right_val valuation) right
+    >>-: fun right ->
     left, right
 
   let show_expr =
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 2849ec1f6f3181dc30a8be6536f26c0df68c57c9..4bc2213fcca50717d73ea1232bf22b3791f81830 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -473,16 +473,21 @@ module Make
       end
     | _ -> `Value state
 
-  let start_call _stmt call valuation state =
+  let start_recursive_call recursion state =
+    let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+    unscope state vars
+
+  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
     in
+    let state = Extlib.opt_fold start_recursive_call recursion state in
     `Value state
 
-  let finalize_call _stmt call ~pre ~post =
+  let finalize_call _stmt call _recursion ~pre ~post =
     if call_init_state call.kf = ISCaller then
       `Value post (* [pre] was the state inferred in the caller, and it
                      has been updated during the analysis of [kf] into
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 00641adb100e2b346ca8c8de13da269f824c713e..8b45d1c11ff3d93957311bea2aebefb4a161b7ec 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1208,7 +1208,7 @@ module D_Impl : Abstract_domain.S
     try `Value (G.assign to_loc to_val lv.lval e state)
     with Unassignable -> `Value (kill lv.lloc state)
 
-  let finalize_call _stmt _call ~pre ~post =
+  let finalize_call _stmt _call _recursion ~pre ~post =
     let state =
       match function_calls_handling with
       | FullInterprocedural -> post
@@ -1217,10 +1217,16 @@ module D_Impl : Abstract_domain.S
     in
     `Value state
 
-  let start_call _stmt call valuation state =
+  let start_recursive_call recursion state =
+    let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+    remove_variables vars state
+
+  let start_call _stmt call recursion valuation state =
     let state =
       match function_calls_handling with
-      | FullInterprocedural -> update valuation state
+      | FullInterprocedural ->
+        let state = Extlib.opt_fold start_recursive_call recursion state in
+        update valuation state
       | IntraproceduralAll
       | IntraproceduralNonReferenced -> `Value G.empty
     in
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index a51098e16eb63723b7d82f5449f5e835ad5cf58f..bda7c81868aa9913ca0e5b03ba9d9f802203c482 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -241,9 +241,10 @@ module Internal
     let effects = Transfer.effects_assume to_z e in
     `Value (Transfer.catenate state effects)
 
-  let start_call _stmt _call _valuation _state = `Value LatticeInout.empty
+  let start_call _stmt _call _recursion _valuation _state =
+    `Value LatticeInout.empty
 
-  let finalize_call _stmt _call ~pre ~post =
+  let finalize_call _stmt _call _recursion ~pre ~post =
     `Value (Transfer.catenate pre post)
 
   let update _valuation state = `Value state
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 2be0ff0dfa9e97bd2e36809c8ff2c47a932fa51b..b63cce8fc729d45187ac9f79c61de50ef6b5ca4f 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1216,17 +1216,22 @@ module Domain = struct
 
   let assume _stmt _exp _bool = update
 
-  let start_call _stmt call valuation state =
+  let start_recursive_call recursion state =
+    let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+    List.fold_left State.remove state vars
+
+  let start_call _stmt call recursion valuation state =
     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
 
-  let finalize_call _stmt _call ~pre ~post =
+  let finalize_call _stmt _call _recursion ~pre ~post =
     if intraprocedural ()
     then `Value (kill post.modified pre)
     else
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index a2d8355c3e27b361b452e9898deb331a9b9d2d0c..07872c80f08088ae3a979608cbee6894342a5196 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -157,9 +157,15 @@ module Internal  : Domain_builder.InputDomain
 
   let assume _ _ _ _ state = `Value state
 
-  let finalize_call _stmt _call ~pre:_ ~post = `Value post
+  let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
 
-  let start_call _stmt _call valuation state = update valuation state
+  let start_recursive_call recursion state =
+    let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+    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
 
   let show_expr _valuation _state _fmt _expr = ()
 
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 94a2f4c5f6ce72aa1a962f391fe0a76ef151b060..1c5d96355def4af667ac8f5292c4af4e85c0dd9a 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -52,11 +52,17 @@ module Make_Memory (Value: Value) = struct
   module Initial_Values = struct let v = [] end
   module Deps = struct let l = [Ast.self] end
 
-  include Hptmap.Make (Base) (Value)(Hptmap.Comp_unused) (Initial_Values) (Deps)
+  include Hptmap.Make
+      (Base.Base) (Value)(Hptmap.Comp_unused) (Initial_Values) (Deps)
 
   let cache_name s =
     Hptmap_sig.PersistentCache ("Value." ^ Value.name ^ "." ^ s)
 
+  let disjoint_union =
+    let cache = cache_name "union" in
+    let decide _key _v1 _v2 = assert false in
+    join ~cache ~symmetric:true ~idempotent:true ~decide
+
   let narrow =
     let module E = struct exception Bottom end in
     let cache = cache_name "narrow" in
@@ -259,7 +265,14 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
      abstraction of the domain itself. *)
   let assume _stmt _expr _pos = update
 
-  let start_call _stmt call _valuation state =
+  let start_recusive_call recursion state =
+    let state = remove_variables recursion.withdrawal state in
+    (* No collision should occur in the substitution. *)
+    let decide _key _v1 _v2 = assert false in
+    snd (replace_key ~decide recursion.base_substitution state)
+
+  let start_call _stmt call recursion _valuation state =
+    let state = Extlib.opt_fold start_recusive_call recursion state in
     let bind_argument state argument =
       let typ = argument.formal.vtype in
       let loc = Main_locations.PLoc.eval_varinfo argument.formal in
@@ -269,8 +282,17 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
     let state = List.fold_left bind_argument state call.arguments in
     `Value state
 
-  let finalize_call _stmt call ~pre:_ ~post =
+  let finalize_recursive_call ~pre recursion state =
+    let shape = Base.Hptset.shape recursion.base_withdrawal in
+    let inter = inter_with_shape shape pre in
+    let state = disjoint_union state inter in
+    (* No collision should occur in the substitution. *)
+    let decide _key _v1 _v2 = assert false in
+    snd (replace_key ~decide recursion.base_substitution state)
+
+  let finalize_call _stmt call recursion ~pre ~post =
     let kf_name = Kernel_function.get_name call.kf in
+    let post = Extlib.opt_fold (finalize_recursive_call ~pre) recursion post in
     match find_builtin kf_name, call.return with
     | None, _ | _, None   -> `Value post
     | Some f, Some return ->
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 2c2f51d88a24600c8c1640d4496547dc9926f048..03f5bb739613e085951385362ff3b686f4964a2c 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -563,9 +563,15 @@ module Internal : Domain_builder.InputDomain
 
   let assume _stmt _exp _pos valuation state = update valuation state
 
-  let start_call _stmt _call valuation state = update valuation state
+  let start_recursive_call recursion state =
+    let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+    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
 
-  let finalize_call _stmt _call ~pre:_ ~post = `Value post
+  let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
 
   let show_expr _valuation _state _fmt _expr = ()
 
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 408114d15682d5121126bb154111f216bf67c8f6..5f566f15944666fa24003a90c4c87db494064deb 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -865,7 +865,7 @@ module Internal = struct
     let trans = Assume (stmt, e, pos) in
     `Value (Traces.add_trans state trans)
 
-  let start_call stmt call _valuation state =
+  let start_call stmt call _recursion _valuation state =
     let kf = call.Eval.kf in
     if Kernel_function.is_definition kf then
       let msg = Format.asprintf "start_call: %s (%b)" (Kernel_function.get_name call.Eval.kf)
@@ -890,7 +890,7 @@ module Internal = struct
           (CallDeclared (call.Eval.kf, exps, Option.map Cil.var var))
       in `Value {state with call_declared_function = true}
 
-  let finalize_call _stmt call ~pre:_ ~post =
+  let finalize_call _stmt call _recursion ~pre:_ ~post =
     if post.call_declared_function
     then `Value {post with call_declared_function = false}
     else
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 5633d599dd564bf5884cb63af702ffe887c5eac9..0c90f11a4886e2b4ee61e7489581694a1039e50d 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -63,8 +63,8 @@ module Make
   let update _ _ = `Value ()
   let assign _ _ _ _ _ _ = `Value ()
   let assume _ _ _ _ _ = `Value ()
-  let start_call _ _ _ _ = `Value ()
-  let finalize_call _ _ ~pre:_ ~post:_ = `Value ()
+  let start_call _ _ _ _ _ = `Value ()
+  let finalize_call _ _ _ ~pre:_ ~post:_ = `Value ()
   let show_expr _ _ _ _ = ()
 
   let logic_assign _ _ _ = ()
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 8e574e39a482a0c6a0e822e2873e04af132ade4e..853705200e9832fcaa6a9fef87253f1784be3b08 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -301,7 +301,7 @@ module Make (Abstract: Abstractions.Eva) = struct
 
   (* Returns the result of a call, and a boolean that indicates whether a
      builtin has been used to interpret the call. *)
-  let process_call stmt call valuation state =
+  let process_call stmt call recursion valuation state =
     Value_util.push_call_stack call.kf (Kstmt stmt);
     let cleanup () =
       Value_util.pop_call_stack ();
@@ -312,7 +312,7 @@ module Make (Abstract: Abstractions.Eva) = struct
       let domain_valuation = Eval.to_domain_valuation valuation in
       let res =
         (* Process the call according to the domain decision. *)
-        match Domain.start_call stmt call domain_valuation state with
+        match Domain.start_call stmt call recursion domain_valuation state with
         | `Value state ->
           Domain.Store.register_initial_state (Value_util.call_stack ()) state;
           !compute_call_ref stmt call state
@@ -449,11 +449,11 @@ module Make (Abstract: Abstractions.Eva) = struct
     Kernel_function.get_formals kf @ locals
 
   (* Do the call to one function. *)
-  let do_one_call valuation stmt lv call state =
+  let do_one_call valuation stmt lv call recursion state =
     let kf_callee = call.kf in
     let pre = state in
     (* Process the call according to the domain decision. *)
-    let call_result = process_call stmt call valuation state in
+    let call_result = process_call stmt call recursion valuation state in
     call_result.cacheable,
     call_result.states >>- fun result ->
     let leaving_vars = leaving_vars kf_callee in
@@ -474,7 +474,7 @@ module Make (Abstract: Abstractions.Eva) = struct
       let post = Domain.leave_scope kf_callee leaving_vars state in
       (* Computes the state after the call, from the post state at the end of
          the called function, and the pre state at the call site. *)
-      Domain.finalize_call stmt call ~pre ~post >>- fun state ->
+      Domain.finalize_call stmt call recursion ~pre ~post >>- fun state ->
       (* Backward propagates the [reductions] on the concrete arguments. *)
       reduce_arguments reductions state >>- fun state ->
       treat_return ~kf_callee lv call.return stmt state
@@ -483,7 +483,7 @@ module Make (Abstract: Abstractions.Eva) = struct
          domains. Do not reduce them, and more importantly, do not remove
          them from the scope. (Because the instance from the initial,
          non-recursive, call are still present.) *)
-      Domain.finalize_call stmt call ~pre ~post:state >>- fun state ->
+      Domain.finalize_call stmt call recursion ~pre ~post:state >>- fun state ->
       treat_return ~kf_callee lv call.return stmt state
     in
     let states =
@@ -745,10 +745,17 @@ module Make (Abstract: Abstractions.Eva) = struct
           let eval, alarms = make_call ~subdivnb kf args valuation state in
           Alarmset.emit ki_call alarms;
           eval >>- fun (call, valuation) ->
+          let recursion =
+            if call.recursive
+            then Some (Recursion.make_recursive_call call.kf)
+            else None
+          in
           (* Register the call. *)
           Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
           (* Do the call. *)
-          let c, states = do_one_call valuation stmt lval_option call state in
+          let c, states =
+            do_one_call valuation stmt lval_option call recursion state
+          in
           (* If needed, propagate that callers cannot be cached. *)
           if c = NoCacheCallers then
             cacheable := NoCacheCallers;