sig
type t
exception Nan_or_infinite
exception Bottom
type rounding_mode = Any | Nearest_Even
type float_kind = Float32 | Float64
val inject : Ival.F.t -> Ival.F.t -> Ival.Float_abstract.t
val inject_r : Ival.F.t -> Ival.F.t -> bool * Ival.Float_abstract.t
val inject_singleton : Ival.F.t -> Ival.Float_abstract.t
val min_and_max_float : Ival.Float_abstract.t -> Ival.F.t * Ival.F.t
val top : Ival.Float_abstract.t
val add :
Ival.Float_abstract.rounding_mode ->
Ival.Float_abstract.t ->
Ival.Float_abstract.t -> bool * Ival.Float_abstract.t
val sub :
Ival.Float_abstract.rounding_mode ->
Ival.Float_abstract.t ->
Ival.Float_abstract.t -> bool * Ival.Float_abstract.t
val mul :
Ival.Float_abstract.rounding_mode ->
Ival.Float_abstract.t ->
Ival.Float_abstract.t -> bool * Ival.Float_abstract.t
val div :
Ival.Float_abstract.rounding_mode ->
Ival.Float_abstract.t ->
Ival.Float_abstract.t -> bool * Ival.Float_abstract.t
val contains_zero : Ival.Float_abstract.t -> bool
val compare : Ival.Float_abstract.t -> Ival.Float_abstract.t -> int
val pretty : Format.formatter -> Ival.Float_abstract.t -> unit
val hash : Ival.Float_abstract.t -> int
val zero : Ival.Float_abstract.t
val is_zero : Ival.Float_abstract.t -> bool
val is_included : Ival.Float_abstract.t -> Ival.Float_abstract.t -> bool
val join :
Ival.Float_abstract.t -> Ival.Float_abstract.t -> Ival.Float_abstract.t
val meet :
Ival.Float_abstract.t -> Ival.Float_abstract.t -> Ival.Float_abstract.t
val contains_a_zero : Ival.Float_abstract.t -> bool
val is_singleton : Ival.Float_abstract.t -> bool
val minus_one_one : Ival.Float_abstract.t
val neg : Ival.Float_abstract.t -> Ival.Float_abstract.t
val cos : Ival.Float_abstract.t -> Ival.Float_abstract.t
val cos_precise : Ival.Float_abstract.t -> Ival.Float_abstract.t
val sin : Ival.Float_abstract.t -> Ival.Float_abstract.t
val sin_precise : Ival.Float_abstract.t -> Ival.Float_abstract.t
val sqrt :
Ival.Float_abstract.rounding_mode ->
Ival.Float_abstract.t -> bool * Ival.Float_abstract.t
val exp :
Ival.Float_abstract.rounding_mode ->
Ival.Float_abstract.t -> bool * Ival.Float_abstract.t
val log :
Ival.Float_abstract.rounding_mode ->
Ival.Float_abstract.t -> bool * Ival.Float_abstract.t
val log10 :
Ival.Float_abstract.rounding_mode ->
Ival.Float_abstract.t -> bool * Ival.Float_abstract.t
val widen :
Ival.Float_abstract.t -> Ival.Float_abstract.t -> Ival.Float_abstract.t
val equal_float_ieee :
Ival.Float_abstract.t -> Ival.Float_abstract.t -> bool * bool
val maybe_le_ieee_float :
Ival.Float_abstract.t -> Ival.Float_abstract.t -> bool
val maybe_lt_ieee_float :
Ival.Float_abstract.t -> Ival.Float_abstract.t -> bool
val diff :
Ival.Float_abstract.t -> Ival.Float_abstract.t -> Ival.Float_abstract.t
val filter_le_ge_lt_gt :
Cil_types.binop ->
bool ->
Ival.Float_abstract.float_kind ->
Ival.Float_abstract.t -> Ival.Float_abstract.t -> Ival.Float_abstract.t
end