Frama-C:
Plug-ins:
Libraries:

Frama-C API - Numerors_float

type t
val pretty : Stdlib.Format.formatter -> t -> unit

Returns a t element representing a positive infinite value

Returns a t element representing a negative infinite value

val pos_zero : Numerors_utils.Precisions.t -> t

Returns a t element representing a positive zero value

val neg_zero : Numerors_utils.Precisions.t -> t

Returns a t element representing a negative zero value

This function returns a float of precision ?prec containing the machine epsilon divided by two for the mandatory precision parameter. We divide it by two because we are only interested in the rounding to nearest mode.

This function returns a float of precision ?prec containing the machine delta of the mandatory precision parameter also divided by two for the same reason as machine_epsilon.

val maximal_pos_float : prec:Numerors_utils.Precisions.t -> t

Maximal positive float in the precision

val maximal_neg_float : prec:Numerors_utils.Precisions.t -> t

Maximal negative float in the precision

val of_int : ?rnd:Numerors_utils.Rounding.t -> ?prec:Numerors_utils.Precisions.t -> int -> t

The functions of_<typ> ~rnd ~prec x return a float of precision <prec> containing the value of x (of type <typ>) rounding to <rnd>. The default values are prec=Precisions.Real and rnd=Rounding.Near

val of_float : ?rnd:Numerors_utils.Rounding.t -> ?prec:Numerors_utils.Precisions.t -> float -> t
val of_string : ?rnd:Numerors_utils.Rounding.t -> ?prec:Numerors_utils.Precisions.t -> string -> t
val change_prec : rnd:Numerors_utils.Rounding.t -> prec:Numerors_utils.Precisions.t -> t -> t

Change the precision

val compare : t -> t -> int

Comparison functions

val eq : t -> t -> bool
val le : t -> t -> bool
val lt : t -> t -> bool
val ge : t -> t -> bool
val gt : t -> t -> bool
val min : t -> t -> t
val max : t -> t -> t
val is_nan : t -> bool

Check if its input is a NaN

val is_inf : t -> bool

Check if its input is an infinite value

val is_pos : t -> bool

Check if its input is positive (is_pos NaN = true)

val is_neg : t -> bool

Check if its input is negative (is_neg NaN = false)

val is_a_zero : t -> bool

Check if its input is a zero (positive or negative)

val is_pos_zero : t -> bool

Check if its input is a positive zero

val is_neg_zero : t -> bool

Check if its input is a negative zero

val is_strictly_pos : t -> bool

Check if its input is strictly positive (non zero)

val is_strictly_neg : t -> bool

Check if its input is strictly negative (non zero)

val sign : t -> Numerors_utils.Sign.t

Returns the sign of its input. The sign of a NaN is Positive

Returns the precision of its input

val exponent : t -> int

Returns the exponent of its input

val significand : t -> t

Returns the significand of its input.

val apply_sign : src:t -> dst:t -> t

Returns a element containing the same value as <dst> but with the sign of <src>

val prev_float : t -> t

Returns the previous floating point number of the same precision

val next_float : t -> t

Returns the following floating point number of the same precision

val neg : t -> t

Negation

val abs : t -> t

Absolute value

val add : ?rnd:Numerors_utils.Rounding.t -> ?prec:Numerors_utils.Precisions.t -> t -> t -> t

The following functions perform floating-point arithmetic operations at the precision <prec> and using the rounding mode <rnd>. Their default values are prec=Precisions.Real and rnd=Rounding.Near. The inputs are "casted" to the asked precision if necessary before computing the operation

val sub : ?rnd:Numerors_utils.Rounding.t -> ?prec:Numerors_utils.Precisions.t -> t -> t -> t
val mul : ?rnd:Numerors_utils.Rounding.t -> ?prec:Numerors_utils.Precisions.t -> t -> t -> t
val div : ?rnd:Numerors_utils.Rounding.t -> ?prec:Numerors_utils.Precisions.t -> t -> t -> t
val pow : ?rnd:Numerors_utils.Rounding.t -> ?prec:Numerors_utils.Precisions.t -> t -> t -> t
val pow_int : ?rnd:Numerors_utils.Rounding.t -> ?prec:Numerors_utils.Precisions.t -> t -> int -> t
val square : ?rnd:Numerors_utils.Rounding.t -> ?prec:Numerors_utils.Precisions.t -> t -> t