From 4c486b4d4bbb64996fac9e9d90cd89b1138e0308 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 13 Oct 2022 14:55:35 +0200
Subject: [PATCH] [Eva] Slightly improves the documentation of [to_seq]
functions.
---
src/kernel_services/abstract_interp/int_val.mli | 5 +++--
src/kernel_services/abstract_interp/ival.mli | 7 ++++---
src/kernel_services/abstract_interp/locations.mli | 2 ++
src/libraries/utils/hptmap_sig.ml | 6 +++---
4 files changed, 12 insertions(+), 8 deletions(-)
diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli
index e750ceec9d0..f3b00895f3b 100644
--- a/src/kernel_services/abstract_interp/int_val.mli
+++ b/src/kernel_services/abstract_interp/int_val.mli
@@ -191,7 +191,8 @@ val complement_under: size:int -> signed:bool -> t -> t or_bottom
val fold_int: ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
(** Builds a sequence of all integers represented by an abstraction, in
- increasing order (resp. decreasing order if [increasing is set to false])
+ increasing order (resp. decreasing order if [increasing] is set to false).
+ The sequence might be infinite.
@raise Abstract_interp.Error_Top if the abstraction has no lower bound
- (resp. no upper bound) *)
+ (or no upper bound in decreasing order). *)
val to_seq: ?increasing:bool -> t -> Integer.t Seq.t
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index edec2e8cecc..ea1f30416e1 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -216,9 +216,10 @@ val fold_int_bounds: (t -> 'a -> 'a) -> t -> 'a -> 'a
in the corresponding direction(s). *)
val to_int_seq: t -> Integer.t Seq.t
-(** Builds a sequence of integer values of the ival in increasing order. The
- Raise {!Abstract_interp.Error_Top} if the argument is a float or a
- potentially infinite integer. *)
+(** Builds a sequence of integer values of the ival in increasing order.
+ The resulting sequence might be infinite.
+ @raise {!Abstract_interp.Error_Top} if the argument is a floating-point
+ interval or an infinite integer interval. *)
(** Subdivisions into two intervals *)
val subdivide: size:Integer.t -> t -> t * t
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index bcb7f17f367..e8b3a29018d 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -146,6 +146,8 @@ module Location_Bytes : sig
one offset cannot be enumerated. *)
val to_seq_i : t -> (Base.t * Ival.t) Seq.t
+ (** Builds a sequence of all bases (with their offsets) of the location.
+ @raise Error_Top in the cases [Top _]. *)
val cached_fold:
cache_name:string ->
diff --git a/src/libraries/utils/hptmap_sig.ml b/src/libraries/utils/hptmap_sig.ml
index b75c35b4be6..1579855eb92 100644
--- a/src/libraries/utils/hptmap_sig.ml
+++ b/src/libraries/utils/hptmap_sig.ml
@@ -113,9 +113,9 @@ module type Shape = sig
to [f] in the opposite order. *)
val to_seq : 'v map -> (key * 'v) Seq.t
- (** [to_seq m] builds a sequence of each pair of key and datume in the
- map [m]. Keys are presented in the sequence in increasing order according
- to the map's ordering. *)
+ (** [to_seq m] builds a sequence of each pair (key, datum) in the map [m].
+ Keys are presented in the sequence in increasing order according to
+ the map's ordering. *)
val cached_fold :
cache_name:string ->
--
GitLab