module Fval:sig
..end
module F:sig
..end
type
t
val packed_descr : Structural_descr.pack
exception Non_finite
Non_finite
is produced when the result of a computation is
entirely not-finite, such as +oo,+oo
(results in Bottom
).type
rounding_mode =
| |
Any |
| |
Nearest_Even |
val top_single_precision_float : t
val round_to_single_precision_float : rounding_mode:rounding_mode -> t -> bool * t
val bits_of_float64 : signed:bool -> t -> Abstract_interp.Int.t * Abstract_interp.Int.t
val bits_of_float32 : signed:bool -> t -> Abstract_interp.Int.t * Abstract_interp.Int.t
val has_finite : t -> bool
has_finite f
returns true iff f
contains at least one finite
element.type
builtin_alarm =
| |
APosInf |
| |
ANegInf |
| |
ANaN of |
| |
AAssume of |
APosInf
when the result may contain +oo;ANegInf
when the result may contain -oo;ANaN msg
when the result is NaN; an explanation of why the argument
is invalid is given.AAssume msg
is a variant of ANaN for debugging purposes, mostly for
internal use. Ignored when printing alarms.
Builtins may sometimes raise Non_finite
when no part of the result
is finite.module Builtin_alarms:Set.S
with type elt = builtin_alarm
typebuiltin_res =
Builtin_alarms.t * t Bottom.or_bottom
type
float_kind =
| |
Float32 |
(* |
32 bits float (a.k.a 'float' C type)
| *) |
| |
Float64 |
(* |
64 bits float (a.k.a 'double' C type)
| *) |
val next_after : float_kind -> F.t -> F.t -> F.t
nextafter/nextafterf
functions in C.val inject : F.t -> F.t -> t
inject
creates an abstract float interval.
Does not handle infinities or NaN.
Does not enlarge subnormals to handle flush-to-zero modesval inject_r_f : float_kind -> F.t -> F.t -> bool * bool * t
inject_r_f
creates an abstract float interval. It handles infinities and
flush-to-zero (rounding subnormals if needed), but not NaN.
The returned booleans are true if the lower/upper bound may be infinite.
May raise Fval.Non_finite
when no part of the result would be finite.
Inputs must be compatible with float_kind
.val inject_r : F.t -> F.t -> bool * t
inject_r_f Float64
.val inject_f : float_kind -> F.t -> F.t -> t
inject_r_f
, but ignores the boolean not_finite
.
The caller must emit appropriate warnings in the presence of
non-finite values.val inject_singleton : F.t -> t
val compare_min : t -> t -> int
val compare_max : t -> t -> int
val min_and_max : t -> F.t * 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 is_a_zero : t -> bool
is_a_zero f
returns true iff f ⊆ -0.0,+0.0
val fold_split : int -> (t -> 'a -> 'a) -> t -> 'a -> 'a
val contains_zero : t -> bool
val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val pretty_overflow : Format.formatter -> t -> unit
--.
is used.val hash : t -> int
val zero : t
val minus_zero : t
val zeros : t
val is_zero : t -> bool
val is_included : t -> t -> bool
val join : t -> t -> t
val meet : t -> t -> t Bottom.or_bottom
val narrow : t -> t -> t Bottom.or_bottom
val contains_a_zero : t -> bool
val is_singleton : t -> bool
exception Not_Singleton_Float
val project_float : t -> F.t
Not_Singleton_Float
when the interval is not a single float.val minus_one_one : t
val subdiv_float_interval : size:int -> t -> t * t
val neg : t -> t
val cos : t -> t
val sin : t -> t
val atan2 : t -> t -> builtin_res
val pow : t -> t -> builtin_res
val powf : t -> t -> builtin_res
val fmod : t -> t -> builtin_res
Builtin_invalid_domain
if there is certainly a division by zero.val sqrt : rounding_mode -> t -> builtin_res
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
Fval.exp
, Fval.log
and Fval.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.
Also note that there the Glibc does not guarantee that
f(FE_DOWNWARD) <= f(FE_TONEAREST) <= f(FE_UPWARD), which implies that
using different rounding modes to bound the final result does not ensure
correct bounds. Here's an example where it does not hold (glibc 2.21):
log10f(3, FE_TONEAREST) < log10f(3, FE_DOWNWARD).
val exp : rounding_mode -> t -> Builtin_alarms.t * t
val log : rounding_mode -> t -> builtin_res
val log10 : rounding_mode -> t -> builtin_res
Fval.Non_finite
.
Can only be called to approximate a computation on double (float64).val floor : rounding_mode -> t -> Builtin_alarms.t * t
val ceil : rounding_mode -> t -> Builtin_alarms.t * t
val trunc : rounding_mode -> t -> Builtin_alarms.t * t
val fround : rounding_mode -> t -> Builtin_alarms.t * t
val expf : rounding_mode -> t -> Builtin_alarms.t * t
val logf : rounding_mode -> t -> builtin_res
val log10f : rounding_mode -> t -> builtin_res
val sqrtf : rounding_mode -> t -> builtin_res
val floorf : rounding_mode -> t -> Builtin_alarms.t * t
val ceilf : rounding_mode -> t -> Builtin_alarms.t * t
val truncf : rounding_mode -> t -> Builtin_alarms.t * t
val froundf : rounding_mode -> t -> Builtin_alarms.t * t
val widen : t -> t -> t
val forward_comp : Abstract_interp.Comp.t -> t -> t -> Abstract_interp.Comp.result
val diff : t -> t -> t Bottom.or_bottom
val backward_comp_left : Abstract_interp.Comp.t ->
bool -> float_kind -> t -> t -> t Bottom.or_bottom
backward_comp op allroundingmodes fkind f1 f2
attempts 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
account. op
must be Eq
, Ne
, Le
, Ge
, Lt
or Gt
val cast_float_to_double_inverse : t -> t
cast_float_to_double_inverse d
return all possible float32 f
such that
(double)f = d
. The double of d
that have no float32 equivalent are
discarded.val enlarge_1ulp : float_kind -> t -> t
Non_finite
if the result is not fully finite.