package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install 

dune-project
 Dependency

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

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. A
    Anne Pacalet
  36. V
    Valentin Perrelle
  37. G
    Guillaume Petiot
  38. D
    Dario Pinto
  39. V
    Virgile Prevosto
  40. A
    Armand Puccetti
  41. F
    Félix Ridoux
  42. V
    Virgile Robles
  43. M
    Muriel Roger
  44. J
    Julien Signoles
  45. N
    Nicolas Stouls
  46. K
    Kostyantyn Vorobyov
  47. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz
sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

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

Module Frama_c_kernel.Floating_point

Floating-point operations.

type c_rounding_mode =
  1. | FE_ToNearest
  2. | FE_Upward
  3. | FE_Downward
  4. | 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 = {
  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.

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 =
  1. | Neg
  2. | 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