package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/Floating_point/index.html

Module `Frama_c_kernel.Floating_point`

Floating-point operations.

type c_rounding_mode =

| FE_ToNearest
| FE_Upward
| FE_Downward
| FE_TowardZero

Rounding modes defined in the C99 standard.

val string_of_c_rounding_mode : c_rounding_mode -> string

val set_round_downward : unit -> unit

val set_round_upward : unit -> unit

val set_round_nearest_even : unit -> unit

val set_round_toward_zero : unit -> unit

val get_rounding_mode : unit -> c_rounding_mode

val set_rounding_mode : c_rounding_mode -> unit

val round_to_single_precision_float : float -> float

val max_single_precision_float : float

val most_negative_single_precision_float : float

val min_denormal : float

val neg_min_denormal : float

val min_single_precision_denormal : float

val neg_min_single_precision_denormal : float

val sys_single_precision_of_string : string -> float

type parsed_float = {

f_nearest : float;
f_lower : float;
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.

val parse : string -> Cil_types.fkind * parsed_float

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.

val has_suffix : Cil_types.fkind -> string -> bool

Checks if the (uppercased) string ends with an explicit F|D|L suffix corresponding to the given float kind.

val pretty_normal : use_hex:bool -> Format.formatter -> float -> unit

val pretty : Format.formatter -> float -> unit

type sign =

| Neg
| Pos

exception Float_Non_representable_as_Int64 of sign

val truncate_to_integer : float -> Integer.t

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

val bits_of_max_double : Integer.t

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

val bits_of_most_negative_double : Integer.t

val bits_of_max_float : Integer.t

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

val bits_of_most_negative_float : Integer.t

val fround : float -> float

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

val trunc : float -> float

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

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

val expf : float -> float

val logf : float -> float

val log10f : float -> float

val powf : float -> float -> float

val sqrtf : float -> float

val fmodf : float -> float -> float

val cosf : float -> float

val sinf : float -> float

val acosf : float -> float

val asinf : float -> float

val atanf : float -> float

val atan2f : float -> float -> float

Auxiliary functions similar to the ones in the C math library

val isnan : float -> bool

val isfinite : float -> bool

val nextafter : float -> float -> float

val nextafterf : float -> float -> float