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
val inject : Ival.F.t -> Ival.F.t -> t
inject creates an abstract float interval. Does not handle infinites. 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. the returned boolean is true if there was reduction
val inject_singleton : Ival.F.t -> t
val min_and_max_float : t -> Ival.F.t * Ival.F.t
val top : t
val add_float : rounding_mode ->
t ->
t -> bool * t
val sub_float : rounding_mode ->
t ->
t -> bool * t
val mult_float : rounding_mode ->
t ->
t -> bool * t
val div_float : 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 neg_float : t -> t
val sqrt_float : rounding_mode ->
t -> bool * t
val minus_one_one : t
val cos_float : t -> t
val cos_float_precise : t -> t
val sin_float : t -> t
val sin_float_precise : t -> t
val exp_float : t -> t
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 : bool ->
typ_loc:Cil_types.typ ->
t -> t -> t
val filter_ge : bool ->
typ_loc:Cil_types.typ ->
t -> t -> t
val filter_lt : bool ->
typ_loc:Cil_types.typ ->
t -> t -> t
val filter_gt : bool ->
typ_loc:Cil_types.typ ->
t -> t -> t