Module Framac_ival.Floating_pointSource

Floating-point operations.

Sourcetype c_rounding_mode =
  1. | FE_ToNearest
  2. | FE_Upward
  3. | FE_Downward
  4. | FE_TowardZero

Rounding modes defined in the C99 standard.

Sourceval string_of_c_rounding_mode : c_rounding_mode -> string
Sourceval set_round_downward : unit -> unit
Sourceval set_round_upward : unit -> unit
Sourceval set_round_nearest_even : unit -> unit
Sourceval set_round_toward_zero : unit -> unit
Sourceval get_rounding_mode : unit -> c_rounding_mode
Sourceval set_rounding_mode : c_rounding_mode -> unit
Sourceval round_to_single_precision_float : float -> float
Sourceval max_single_precision_float : float
Sourceval most_negative_single_precision_float : float
Sourceval min_denormal : float
Sourceval neg_min_denormal : float
Sourceval min_single_precision_denormal : float
Sourceval neg_min_single_precision_denormal : float
Sourceval sys_single_precision_of_string : string -> float
Sourcetype parsed_float = {
  1. f_nearest : float;
  2. f_lower : float;
  3. f_upper : float;
}

If s is parsed as (n, l, u), then n is the nearest approximation of s with the desired precision. Moreover, l and u are the most precise float such that l <= s <= u, again with this precision.

Consistent with logic_real definition in Cil_types.

parse s parses s and returns the parsed float and its kind (single, double or long double precision) according to its suffix, if any. Strings with no suffix are parsed as double.

Sourceval pretty_normal : use_hex:bool -> Format.formatter -> float -> unit
Sourceval pretty : Format.formatter -> float -> unit
Sourcetype sign =
  1. | Neg
  2. | Pos
Sourceexception Float_Non_representable_as_Int64 of sign
Sourceval truncate_to_integer : float -> Z.t

Raises Float_Non_representable_as_Int64 if the float value cannot be represented as an Int64 or as an unsigned Int64.

Sourceval bits_of_max_double : Z.t

binary representation of -DBL_MAX and DBL_MAX as 64 bits signed integers

Sourceval bits_of_most_negative_double : Z.t
Sourceval bits_of_max_float : Z.t

binary representation of -FLT_MAX and FLT_MAX as 32 bits signed integers

Sourceval bits_of_most_negative_float : Z.t
Sourceval fround : float -> float

Rounds to nearest integer, away from zero (like round() in C).

Sourceval trunc : float -> float

Rounds to integer, toward zero (like trunc() in C).

Single-precision (32-bit) floating-point wrappers

Sourceval expf : float -> float
Sourceval logf : float -> float
Sourceval log10f : float -> float
Sourceval powf : float -> float -> float
Sourceval sqrtf : float -> float
Sourceval fmodf : float -> float -> float
Sourceval cosf : float -> float
Sourceval sinf : float -> float
Sourceval atan2f : float -> float -> float

Auxiliary functions similar to the ones in the C math library

Sourceval isnan : float -> bool
Sourceval isfinite : float -> bool
Sourceval nextafter : float -> float -> float
Sourceval nextafterf : float -> float -> float