diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 0bfde596c3a5a58f79426bb00d5e24df90604f56..0c7e3ba7eeca445689d0faa9b82e4ac3955e2788 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -452,6 +452,7 @@ module Base = struct
         let varname = Datatype.undefined
       end)
   let id = id
+  let pretty_debug = pretty
 end
 
 include Base
@@ -549,6 +550,17 @@ let of_string_exp e =
 
 module SetLattice = Make_Hashconsed_Lattice_Set(Base)(Hptset)
 
+module BMap =
+  Hptmap.Make (Base) (Base) (Hptmap.Comp_unused)
+    (struct let v = [ [] ] end)
+    (struct let l = [ Ast.self ] end)
+
+type substitution = base Hptmap.Shape(Base).t
+
+let substitution_from_list list =
+  let add map (key, elt) = BMap.add key elt map in
+  let bmap = List.fold_left add BMap.empty list in
+  BMap.shape bmap
 
 (*
 Local Variables:
diff --git a/src/kernel_services/abstract_interp/base.mli b/src/kernel_services/abstract_interp/base.mli
index 708c79c5579a7cd21c2b3a44e64001e47d2cbef7..ccebf749bbff8ad2ad9617a9fe071c31691b818c 100644
--- a/src/kernel_services/abstract_interp/base.mli
+++ b/src/kernel_services/abstract_interp/base.mli
@@ -225,6 +225,12 @@ 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. *)
 
+type substitution = base Hptmap.Shape(Base).t
+(** Type used for the substitution between bases. *)
+
+val substitution_from_list: (base * base) list -> substitution
+(** Creates a substitution from an association list. *)
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 46906585f7665013e9e5de09741e9e87a4b31377..b2223cda94798f4fd226b56f777c6bb8dfa9e94e 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -638,6 +638,14 @@ struct
     | Top -> Top
     | Map m -> Map (M.remove b m)
 
+  let replace_base shape = function
+    | Bottom -> Bottom
+    | Top -> Top
+    | Map map as t ->
+      let decide _key = Offsetmap.join in
+      let modified, map = M.replace_key ~decide shape map in
+      if modified then Map map else t
+
   let is_reachable = function
     | Bottom -> false
     | Top | Map _ -> true
diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli b/src/kernel_services/abstract_interp/lmap_sig.mli
index 9a7ac8d40b99f7cf4072d0a67e24a5509661db74..b9070fa559c4e22b574e0f16407d3dfab8080337 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
 
+val replace_base: Base.substitution -> t -> t
+
 
 (** {2 Iterators} *)
 
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index f5c126c7119a38108bfa9d98a3f9b0c2bec5ce0d..442b8d59bc652f8e903e810104b36a7dd8f74640 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -358,6 +358,19 @@ module Location_Bytes = struct
        | Map _ -> false);
        true
 
+ let replace_base substitution v =
+   let substitute replace make acc =
+     let modified, set' = replace substitution acc in
+     modified, if modified then make set' else v
+   in
+   match v with
+   | Top (Base.SetLattice.Top, _) -> false, v
+   | Top (Base.SetLattice.Set set, origin) ->
+     substitute Base.Hptset.replace (inject_top_origin_internal origin) set
+   | Map map ->
+     let decide _key  = Ival.join in
+     substitute (M.replace_key ~decide) (fun m -> Map m) map
+
  let overlaps ~partial ~size mm1 mm2 =
    match mm1, mm2 with
    | Top _, _ | _, Top _ -> intersects mm1 mm2
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index 760e1b93fa61909cf5a2fe0326db8f63f205c7bc..5157be7d4edb642bed311dbe52cd716202317830 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -78,6 +78,10 @@ module Location_Bytes : sig
   (** [add b i loc] binds [b] to [i] in [loc] when [i] is not {!Ival.bottom},
       and returns {!bottom} otherwise. *)
 
+  val replace_base: Base.substitution -> t -> bool * t
+  (** [replace_base subst loc] changes the location [loc] by substituting the
+      pointed bases according to [subst]. *)
+
   val diff : t -> t -> t
     (** Over-approximation of difference. [arg2] needs to be exact or an
         under_approximation. *)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index a545314edfe9d57bca80a5b37ab7d504a507f032..0fdd5f2fea59bd6a63b227433c8c022e8b681597 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -909,6 +909,10 @@ module V_Or_Uninitialized = struct
     in
     removed, t'
 
+  let replace_base substitution t =
+    let modified, v = V.replace_base substitution (get_v t) in
+    modified, if modified then create (get_flags t) v else t
+
   let reduce_by_initializedness pos v =
     if pos then
       meet v (C_init_esc V.top)
diff --git a/src/plugins/value_types/cvalue.mli b/src/plugins/value_types/cvalue.mli
index a5c93243c0b2de1d3eeea18c3f4882e641652a3c..717c387372fd1c049d6809987a8ced77534c0271 100644
--- a/src/plugins/value_types/cvalue.mli
+++ b/src/plugins/value_types/cvalue.mli
@@ -226,6 +226,8 @@ module V_Or_Uninitialized : sig
   val unspecify_escaping_locals :
     exact:bool -> (V.M.key -> bool) -> t -> bool * t
 
+  val replace_base: Base.substitution -> t -> bool * t
+
   val map: (V.t -> V.t) -> t -> t
   val map2: (V.t -> V.t -> V.t) -> t -> t -> t
   (** initialized/escaping information is the join of the information