diff --git a/src/kernel_services/abstract_interp/base.mli b/src/kernel_services/abstract_interp/base.mli
index ccebf749bbff8ad2ad9617a9fe071c31691b818c..adbbcbc800ddffd87125846e4e7241daf601803f 100644
--- a/src/kernel_services/abstract_interp/base.mli
+++ b/src/kernel_services/abstract_interp/base.mli
@@ -225,6 +225,11 @@ val register_memory_var : Cil_types.varinfo -> validity -> t
     They are created only to fill the contents of another variable.
     Their field [vsource] is set to false. *)
 
+
+(** {2 Substituting bases}
+    This is used to efficiently replace some bases by others in locations or
+    in memory states, for instance in {!Locations} or {!Lmap_sig}. *)
+
 type substitution = base Hptmap.Shape(Base).t
 (** Type used for the substitution between bases. *)
 
diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli b/src/kernel_services/abstract_interp/lmap_sig.mli
index b9070fa559c4e22b574e0f16407d3dfab8080337..fe238921431058ec58b0ee8f8deda27fbe675672 100644
--- a/src/kernel_services/abstract_interp/lmap_sig.mli
+++ b/src/kernel_services/abstract_interp/lmap_sig.mli
@@ -150,6 +150,8 @@ val filter_by_shape: 'a Hptmap.Shape(Base.Base).t -> t -> t
 (** Removes the base if it is present. Does nothing otherwise. *)
 val remove_base : Base.t -> t -> t
 
+(** [replace_bases substitition map] replaces some bases in [map]
+    according to [substitution]. *)
 val replace_base: Base.substitution -> t -> t
 
 
diff --git a/src/libraries/utils/hptset.mli b/src/libraries/utils/hptset.mli
index cd4781d5726394fac1204192a5efe5498864642a..1da170653c0006277b2111ae767e974ab6a48d41 100644
--- a/src/libraries/utils/hptset.mli
+++ b/src/libraries/utils/hptset.mli
@@ -89,6 +89,9 @@ module type S = sig
     (** Build a set from another [elt]-indexed map or set. *)
 
     val partition_with_shape: 'a shape -> t -> t * t
+    (** [partition_with_shape shape set] returns two sets [inter, diff] that are
+        respectively the intersection and the difference between [set] and
+        [shape]. *)
 
     val fold2_join_heterogeneous:
       cache:Hptmap_sig.cache_type ->
@@ -101,6 +104,9 @@ module type S = sig
       'b
 
     val replace: elt shape -> t -> bool * t
+    (** [replace shape set] replaces the elements of [set] according to [shape].
+        The returned boolean indicates whether the set has been modified; it is
+        false when the intersection between [shape] and [set] is empty. *)
 
     (** Clear all the caches used internally by the functions of this module.
         Those caches are not project-aware, so this function must be called
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 472f056cf79882aaaa355c67383a1df2da886053..318a78d9638e6accdd2b77bcd46ab3863dba8699 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -251,11 +251,13 @@ module type Transfer = sig
     stmt -> exp -> bool ->
     (value, location, origin) valuation -> state -> state or_bottom
 
-  (** [start_call stmt call valuation state] returns an initial state
+  (** [start_call stmt call recursion valuation state] returns an initial state
       for the analysis of a called function. In particular, this function
       should introduce the formal parameters in the state, if necessary.
       - [stmt] is the statement of the call site;
       - [call] represents the call: the called function and the arguments;
+      - [recursion] is the information needed to interpret a recursive call.
+        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. *)
@@ -268,6 +270,8 @@ module type Transfer = sig
       end of the called function.
       - [stmt] is the statement of the call site;
       - [call] represents the function call and its arguments.
+      - [recursion] is the information needed to interpret a recursive call.
+        It is None if the call is not recursive.
       - [pre] and [post] are the states before and at the end of the call
         respectively. *)
   val finalize_call:
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 1c5d96355def4af667ac8f5292c4af4e85c0dd9a..339d8edb25a19e8e4eb85906a1fe8c10e9f2ae5b 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -53,7 +53,7 @@ module Make_Memory (Value: Value) = struct
   module Deps = struct let l = [Ast.self] end
 
   include Hptmap.Make
-      (Base.Base) (Value)(Hptmap.Comp_unused) (Initial_Values) (Deps)
+      (Base.Base) (Value) (Hptmap.Comp_unused) (Initial_Values) (Deps)
 
   let cache_name s =
     Hptmap_sig.PersistentCache ("Value." ^ Value.name ^ "." ^ s)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 9c68087ab28753222286bf417de5e3acb997da02..50b0d1084fdf9d1c41f08f15226012efa981c997 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -174,7 +174,7 @@ module Make (Abstract: Abstractions.Eva) = struct
     let use_spec =
       match recursion with
       | Some { depth } when depth >= Value_parameters.RecursiveUnroll.get () ->
-        `Spec (Recursion.recursive_spec call_kinstr kf)
+        `Spec (Recursion.get_spec call_kinstr kf)
       | _ ->
         match kf.fundec with
         | Declaration (_,_,_,_) -> `Spec (Annotations.funspec kf)
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index ba0ab79f7e2e7da0f06fc13cd52ea260e47824ec..ca19131dc65c077a240dd187482bf6b724ba0d4f 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -44,7 +44,7 @@ let mark_unknown_requires kinstr kf funspec =
   in
   List.iter emit_behavior funspec.spec_behavior
 
-let recursive_spec kinstr kf =
+let get_spec kinstr kf =
   let funspec = Annotations.funspec ~populate:false kf in
   if Cil.is_empty_funspec funspec then
     Value_parameters.abort ~current:true
@@ -174,7 +174,7 @@ let make_recursion call depth =
   let base_withdrawal = Base.Hptset.of_list list_withdrawal in
   { depth; substitution; base_substitution; withdrawal; base_withdrawal; }
 
-let get_recursion call =
+let make call =
   let call_stack = Value_util.call_stack () in
   let previous_calls = List.filter (fun (f, _) -> f == call.kf) call_stack in
   let depth = List.length previous_calls in
@@ -182,7 +182,7 @@ let get_recursion call =
   then Some (make_recursion call depth)
   else None
 
-let revert_recursion recursion =
+let revert recursion =
   let revert (v1, v2) = v2, v1 in
   let substitution = List.map revert recursion.substitution in
   let base_of_varinfo (v1, v2) = Base.of_varinfo v1, Base.of_varinfo v2 in
diff --git a/src/plugins/value/engine/recursion.mli b/src/plugins/value/engine/recursion.mli
index 58809e8bca2f49da403bb73e4acf00dd6bc86be1..d4f21920b0e191596613912e99c2c79f0811af2d 100644
--- a/src/plugins/value/engine/recursion.mli
+++ b/src/plugins/value/engine/recursion.mli
@@ -25,9 +25,14 @@
 open Cil_types
 open Eval
 
-val recursive_spec: kinstr -> kernel_function -> funspec
+(* Returns the specification for a recursive call to the given function. Fails
+   if the function has no specification. Marks the preconditions of the call
+   as unknowns. *)
+val get_spec: kinstr -> kernel_function -> funspec
 
-(** TODO *)
-val get_recursion: ('v, 'loc) call -> recursion option
+(** Creates the information about a recursive call. *)
+val make: ('v, 'loc) call -> recursion option
 
-val revert_recursion: recursion -> recursion
+(** Changes the information about a recursive call to be used at the end
+    of the call. *)
+val revert: recursion -> recursion
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 245551d66100d08a31952d66e0c068677ce96bb3..68c94c2fa24d42d1e9c85cd58b5006babcbcafca 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -113,7 +113,7 @@ let substitution_visitor table = object
   method! vvrbl varinfo =
     match VarHashtbl.find_opt table varinfo with
     | None -> Cil.JustCopy
-    | Some lval -> Cil.ChangeTo lval
+    | Some vi -> Cil.ChangeTo vi
 end
 
 module Make (Abstract: Abstractions.Eva) = struct
@@ -483,7 +483,7 @@ module Make (Abstract: Abstractions.Eva) = struct
       >>- fun reductions ->
       (* The formals (and the locals) of the called function leave scope. *)
       let post = Domain.leave_scope kf_callee leaving_vars state in
-      let recursion = Option.map Recursion.revert_recursion recursion in
+      let recursion = Option.map Recursion.revert recursion 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 recursion ~pre ~post >>- fun state ->
@@ -582,7 +582,7 @@ module Make (Abstract: Abstractions.Eva) = struct
     compute_actuals ~subdivnb ~determinate valuation state arguments
     >>=: fun (args, valuation) ->
     let call = create_call kf args in
-    let recursion = Recursion.get_recursion call in
+    let recursion = Recursion.make call in
     let call = Extlib.opt_fold replace_recursive_call recursion call in
     call, recursion, valuation
 
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index c64f692b7bd70ac3b95eee342519317c3e0cb11a..c68cebbd998e47af73b5109c6cb0384dac977530 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -236,13 +236,25 @@ type ('loc, 'value) call = {
 (** Information needed to interpret a recursive call.
     The local variables and formal parameters of different recursive calls
     should not be mixed up. Those of the current call must be temporary withdraw
-    or replaced from the domain states before starting the new recursive call. *)
+    or replaced from the domain states before starting the new recursive call,
+    and the inverse transformation must be made at the end of the call. *)
 type recursion = {
   depth: int;
+  (** Depth of the recursive call, i.e. the number of previous call to the
+      called function in the current callstack. *)
   substitution: (varinfo * varinfo) list;
+  (** List of variables substitutions to be performed by the domains: for each
+      pair, the first variable must be replaced by the second one in the domain
+      state. *)
   base_substitution: Base.substitution;
+  (** Same substitution as the previous field, for bases. *)
   withdrawal: varinfo list;
+  (** List of variables to be temporary removed from the state at the start of a
+      new recursive call (by the function [start_call] of the abstract domains),
+      or to be put back in the state at the end of a recursive call (by the
+      function [finalize_call] of the abstract domains).  *)
   base_withdrawal: Base.Hptset.t;
+  (** Same withdrawal as the previous field, for bases. *)
 }
 
 (** Can the results of a function call be cached with memexec? *)
diff --git a/src/plugins/value/values/abstract_location.mli b/src/plugins/value/values/abstract_location.mli
index 00d64bc5f32993e42c9fe2a0577bed641c1ce5f5..40419bfc573c0b96ea2682ac138d10deeea0386f 100644
--- a/src/plugins/value/values/abstract_location.mli
+++ b/src/plugins/value/values/abstract_location.mli
@@ -44,6 +44,8 @@ module type S = sig
   val to_value : location -> value
   val size : location -> Int_Base.t
 
+  (** [replace_base substitution location] replaces the variables represented
+      by the [location] according to [substitution]. *)
   val replace_base: Base.substitution -> location -> location
 
   (** {3 Alarms } *)
diff --git a/src/plugins/value/values/abstract_value.mli b/src/plugins/value/values/abstract_value.mli
index ac8ddecc5dc658026dd08264ee725b7abcd05342..50fb3525cae4491c7d1ad3800558923cc3c1066f 100644
--- a/src/plugins/value/values/abstract_value.mli
+++ b/src/plugins/value/values/abstract_value.mli
@@ -190,6 +190,9 @@ module type S = sig
       boolean must be [true] if some of the values represented by [v] do not
       correspond to functions. It is always safe to return [`Top, true]. *)
 
+  (** For pointer values, [replace_base substitution value] replaces the bases
+      pointed to by [value] according to [substitution]. For arithmetic values,
+      this function returns the [value] unchanged.  *)
   val replace_base: Base.substitution -> t -> t
 end