diff --git a/src/plugins/value/values/abstract_value.mli b/src/plugins/value/values/abstract_value.mli
index 05e465434ffa50ad28ba262aeceb2c599fd111bc..ac8ddecc5dc658026dd08264ee725b7abcd05342 100644
--- a/src/plugins/value/values/abstract_value.mli
+++ b/src/plugins/value/values/abstract_value.mli
@@ -182,12 +182,15 @@ module type S = sig
     dst_val: t ->
     t option or_bottom
 
+  (** {3 Misc } *)
+
   val resolve_functions : t -> Kernel_function.t list or_top * bool
   (** [resolve_functions v] returns the list of functions that may be pointed to
       by the abstract value [v] (representing a function pointer). The returned
       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]. *)
 
+  val replace_base: Base.substitution -> t -> t
 end
 
 type 'v key = 'v Structure.Key_Value.key
diff --git a/src/plugins/value/values/main_values.ml b/src/plugins/value/values/main_values.ml
index b21f868739e43063cf196d40e5aa1ebea5b3b811..b38d4fcaf3a3eb938642682fc965784ee137b0f2 100644
--- a/src/plugins/value/values/main_values.ml
+++ b/src/plugins/value/values/main_values.ml
@@ -132,6 +132,8 @@ module CVal = struct
       let kfs, alarm = Locations.Location_Bytes.fold_topset_ok aux v init in
       `Value kfs, alarm
     with Abstract_interp.Error_Top -> `Top, true
+
+  let replace_base substitution t = snd (Cvalue.V.replace_base substitution t)
 end
 
 module Interval = struct
@@ -175,6 +177,7 @@ module Interval = struct
   let forward_cast ~src_type:_ ~dst_type:_ _ = `Value top
 
   let resolve_functions _ = `Top, true
+  let replace_base _substitution t = t
 
   let rewrap_integer range value =
     match value with
diff --git a/src/plugins/value/values/numerors/numerors_value.ml b/src/plugins/value/values/numerors/numerors_value.ml
index 2832d06cb3586316b5fe2fa311b2cb2f05e7a3ce..5381969a55fc736414ca52827754b99f6b22cd00 100644
--- a/src/plugins/value/values/numerors/numerors_value.ml
+++ b/src/plugins/value/values/numerors/numerors_value.ml
@@ -318,6 +318,7 @@ let assume_comparable _cmp v1 v2 = `Unknown (v1, v2)
 let rewrap_integer _ _ = top
 let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
 let resolve_functions _ = `Top, true
+let replace_base _substitution t = t
 
 
 (*-----------------------------------------------------------------------------
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index b46b11002e82269573247c93bebfb48e5e102bb7..f6fd8d3fd663c0c763a80f814b1d343015a6cabe 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -434,6 +434,11 @@ module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
     else Top
 
   let resolve_functions _ = `Top, true (* TODO: extract value *)
+  let replace_base substitution = function
+    | Top -> Top
+    | O offsm ->
+      let f v = snd (Cvalue.V_Or_Uninitialized.replace_base substitution v) in
+      O (Cvalue.V_Offsetmap.map_on_values f offsm)
 
   let forward_unop _typ op o =
     let o' = match o, op with
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index b9f59f90e277c5ef875801640ea6f98d3987a801..08334941537bb65fd0931def46400ca033e12a12 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -107,6 +107,8 @@ let constant _ = function
    precisely *)
 let resolve_functions _ = `Top, true
 
+let replace_base _substitution t = t
+
 (** {2 Alarms} *)
 
 let assume_non_zero v =
diff --git a/src/plugins/value/values/value_product.ml b/src/plugins/value/values/value_product.ml
index 7e89f1fc751c739bdd1e262ae99ab1b6871f2136..03ec02d71f2b735936b3e84186198d8da1bf5cd9 100644
--- a/src/plugins/value/values/value_product.ml
+++ b/src/plugins/value/values/value_product.ml
@@ -125,6 +125,10 @@ module Make
     in
     list, b1 && b2
 
+  let replace_base substitution (left, right) =
+    Left.replace_base substitution left,
+    Right.replace_base substitution right
+
   let reduce (orig_left, orig_right) left right = match left, right with
     | None, None            -> None
     | Some left, None       -> Some (left, orig_right)