Module Ival.Float_abstract

module Float_abstract: sig .. end

type t 
exception Nan_or_infinite
Nan_or_infinite means that the operation may not be a finite float. (It does not mean that it is not a finite float).
exception Bottom
type rounding_mode = 
| Any
| Nearest_Even
type float_kind = 
| Float32 (*
32 bits float (a.k.a 'float' C type)
*)
| Float64 (*
64 bits float (a.k.a 'double' C type)
*)
val inject : Ival.F.t -> Ival.F.t -> t
inject creates an abstract float interval. Does not handle infinites or NaN. Does not enlarge subnormals to handle flush-to-zero modes
val inject_r : Ival.F.t -> Ival.F.t -> bool * t
inject_r creates an abstract float interval. It handles infinites and flush-to-zero, but not NaN. The returned boolean is true if a bound was infinite. May raise Ival.Float_abstract.Bottom when no part of the result would be finite.
val inject_singleton : Ival.F.t -> t
val min_and_max_float : t -> Ival.F.t * Ival.F.t
val top : t
val add : rounding_mode ->
t ->
t -> bool * t
val sub : rounding_mode ->
t ->
t -> bool * t
val mul : rounding_mode ->
t ->
t -> bool * t
val div : rounding_mode ->
t ->
t -> bool * t
val contains_zero : t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val hash : t -> int
val zero : t
val is_zero : t -> bool
val is_included : t -> t -> bool
val join : t -> t -> t
val meet : t -> t -> t
val contains_a_zero : t -> bool
val is_singleton : t -> bool
val minus_one_one : t
val neg : t -> t
val cos : t -> t
val cos_precise : t -> t
val sin : t -> t
val sin_precise : t -> t
val sqrt : rounding_mode ->
t -> bool * t

Discussion regarding -all-rounding-modes and the functions below.

Support for fesetround(FE_UPWARD) and fesetround(FE_DOWNWARD) seems to be especially poor, including in not-so-old versions of Glibc (https://sourceware.org/bugzilla/show_bug.cgi?id=3976). The code for Ival.Float_abstract.exp, Ival.Float_abstract.log and Ival.Float_abstract.log10 is correct wrt. -all-rounding-modes ONLY if the C implementation of these functions is correct in directed rounding modes. Otherwise, anything could happen, including crashes. For now, unless the Libc is known to be reliable, these functions should be called with rounding_mode=Nearest_Even only

val exp : rounding_mode ->
t -> bool * t
val log : rounding_mode ->
t -> bool * t
val log10 : rounding_mode ->
t -> bool * t
All three functions may raise Ival.Float_abstract.Bottom. Can only be called to approximate a computation on double (float64).
val widen : t -> t -> t
val equal_float_ieee : t -> t -> bool * bool
val maybe_le_ieee_float : t -> t -> bool
val maybe_lt_ieee_float : t -> t -> bool
val diff : t -> t -> t
val filter_le_ge_lt_gt : Cil_types.binop ->
bool ->
float_kind ->
t -> t -> t
filter_le_ge_lt_gt op allroundingmodes fkind f1 f2 attemps to reduce f1 into f1' so that the relation f1' op f2 holds. fkind is the type of f1 and f1' (not necessarily of f2). If allroundingmodes is set, all possible rounding modes are taken into acount. op must be Le, Ge, Lt or Gt