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 modesval 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
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
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