From a7b9ef95d06de45559155850abdff5937f14e0e2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 12 Apr 2021 10:42:13 +0200
Subject: [PATCH] [Eva] Clarifies the documentation of [replace_base] in lmap
and locations.
---
src/kernel_services/abstract_interp/lmap_sig.mli | 3 ++-
src/kernel_services/abstract_interp/locations.mli | 3 ++-
2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli b/src/kernel_services/abstract_interp/lmap_sig.mli
index fe238921431..f9c31abc77d 100644
--- a/src/kernel_services/abstract_interp/lmap_sig.mli
+++ b/src/kernel_services/abstract_interp/lmap_sig.mli
@@ -151,7 +151,8 @@ val filter_by_shape: 'a Hptmap.Shape(Base.Base).t -> t -> t
val remove_base : Base.t -> t -> t
(** [replace_bases substitition map] replaces some bases in [map]
- according to [substitution]. *)
+ according to [substitution]. If [substitution] conflates different bases,
+ the offsetmaps bound to these bases are joined. *)
val replace_base: Base.substitution -> t -> t
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index 5157be7d4ed..4bea9a7b4e2 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -80,7 +80,8 @@ module Location_Bytes : sig
val replace_base: Base.substitution -> t -> bool * t
(** [replace_base subst loc] changes the location [loc] by substituting the
- pointed bases according to [subst]. *)
+ pointed bases according to [subst]. If [substitution] conflates different
+ bases, the offsets bound to these bases are joined. *)
val diff : t -> t -> t
(** Over-approximation of difference. [arg2] needs to be exact or an
--
GitLab