diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli index e750ceec9d0d719da7dbc60d45e8d46f15888c95..f3b00895f3b1d89b010d1ef53ad04f80d3598647 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 edec2e8cecc71049687bcd9e47ce5493a260251d..ea1f30416e131f7ffa3c9356a781457f4ccf3588 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 bcb7f17f367e4e2e0d641384b6a210ed5ca37401..e8b3a29018d7817f2d373b403a3c9b210ad25f53 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 b75c35b4be657ae35d58a2a021f5f399e61ef0f7..1579855eb92d871a42a69ea461bd1e3ab23664e7 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 ->