sig
type kind = Float32 | Float64 | Real
val pretty_kind : Format.formatter -> Fval.kind -> unit
module F :
sig
type t
val packed_descr : Structural_descr.pack
val of_float : float -> Fval.F.t
val to_float : Fval.F.t -> float
val compare : Fval.F.t -> Fval.F.t -> int
val equal : Fval.F.t -> Fval.F.t -> bool
val pretty : Format.formatter -> Fval.F.t -> unit
val pretty_normal :
use_hex:bool -> Format.formatter -> Fval.F.t -> unit
val plus_zero : Fval.F.t
val is_finite : Fval.F.t -> bool
val next_float : Fval.kind -> float -> float
val prev_float : Fval.kind -> float -> float
end
type t
val packed_descr : Structural_descr.pack
val top_finite : Fval.kind -> Fval.t
val round_to_single_precision_float : Fval.t -> Fval.t
val bits_of_float64_list :
Fval.t -> (Abstract_interp.Int.t * Abstract_interp.Int.t) list
val bits_of_float32_list :
Fval.t -> (Abstract_interp.Int.t * Abstract_interp.Int.t) list
val inject : ?nan:bool -> Fval.kind -> Fval.F.t -> Fval.F.t -> Fval.t
val nan : Fval.t
val inject_singleton : Fval.F.t -> Fval.t
val has_greater_min_bound : Fval.t -> Fval.t -> int
val has_smaller_max_bound : Fval.t -> Fval.t -> int
val min_and_max : Fval.t -> (Fval.F.t * Fval.F.t) option * bool
val is_negative : Fval.t -> Abstract_interp.Comp.result
val top : Fval.t
val add : Fval.kind -> Fval.t -> Fval.t -> Fval.t
val sub : Fval.kind -> Fval.t -> Fval.t -> Fval.t
val mul : Fval.kind -> Fval.t -> Fval.t -> Fval.t
val div : Fval.kind -> Fval.t -> Fval.t -> Fval.t
val compare : Fval.t -> Fval.t -> int
val equal : Fval.t -> Fval.t -> bool
val pretty : Format.formatter -> Fval.t -> unit
val hash : Fval.t -> int
val plus_zero : Fval.t
val minus_zero : Fval.t
val zeros : Fval.t
val pi : Fval.t
val e : Fval.t
val contains_a_zero : Fval.t -> bool
val contains_plus_zero : Fval.t -> bool
val contains_non_zero : Fval.t -> bool
val is_included : Fval.t -> Fval.t -> bool
val join : Fval.t -> Fval.t -> Fval.t
val meet : Fval.t -> Fval.t -> Fval.t Bottom.or_bottom
val narrow : Fval.t -> Fval.t -> Fval.t Bottom.or_bottom
val is_singleton : Fval.t -> bool
val is_finite : Fval.t -> Abstract_interp.Comp.result
val is_not_nan : Fval.t -> Abstract_interp.Comp.result
val backward_is_finite : Fval.kind -> Fval.t -> Fval.t Bottom.or_bottom
val backward_is_not_nan : Fval.t -> Fval.t Bottom.or_bottom
exception Not_Singleton_Float
val project_float : Fval.t -> Fval.F.t
val subdiv_float_interval : Fval.kind -> Fval.t -> Fval.t * Fval.t
val neg : Fval.t -> Fval.t
val cos : Fval.kind -> Fval.t -> Fval.t
val sin : Fval.kind -> Fval.t -> Fval.t
val atan2 : Fval.kind -> Fval.t -> Fval.t -> Fval.t
val pow : Fval.kind -> Fval.t -> Fval.t -> Fval.t
val fmod : Fval.kind -> Fval.t -> Fval.t -> Fval.t
val sqrt : Fval.kind -> Fval.t -> Fval.t
val exp : Fval.kind -> Fval.t -> Fval.t
val log : Fval.kind -> Fval.t -> Fval.t
val log10 : Fval.kind -> Fval.t -> Fval.t
val floor : Fval.kind -> Fval.t -> Fval.t
val ceil : Fval.kind -> Fval.t -> Fval.t
val trunc : Fval.kind -> Fval.t -> Fval.t
val fround : Fval.kind -> Fval.t -> Fval.t
val widen : Fval.t -> Fval.t -> Fval.t
val forward_comp :
Abstract_interp.Comp.t -> Fval.t -> Fval.t -> Abstract_interp.Comp.result
val backward_comp_left_true :
Abstract_interp.Comp.t ->
Fval.kind -> Fval.t -> Fval.t -> Fval.t Bottom.or_bottom
val backward_comp_left_false :
Abstract_interp.Comp.t ->
Fval.kind -> Fval.t -> Fval.t -> Fval.t Bottom.or_bottom
val backward_cast_float_to_double : Fval.t -> Fval.t Bottom.or_bottom
val backward_cast_double_to_real : Fval.t -> Fval.t
val cast_int_to_float :
Fval.kind ->
Abstract_interp.Int.t option -> Abstract_interp.Int.t option -> Fval.t
val backward_add :
Fval.kind ->
left:Fval.t ->
right:Fval.t -> result:Fval.t -> (Fval.t * Fval.t) Bottom.or_bottom
val backward_sub :
Fval.kind ->
left:Fval.t ->
right:Fval.t -> result:Fval.t -> (Fval.t * Fval.t) Bottom.or_bottom
val kind : Cil_types.fkind -> Fval.kind
end