package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Floating Arithmetic Model

val f32 : Lang.adt
val f64 : Lang.adt
val t32 : Lang.F.tau
val t64 : Lang.F.tau
val fq32 : Lang.lfun
val fq64 : Lang.lfun
type model =
  1. | Real
  2. | Float
val configure : model -> WpContext.rollback

model independant

val tau_of_float : Ctypes.c_float -> Lang.F.tau

with respect to model

type op =
  1. | LT
  2. | EQ
  3. | LE
  4. | NE
  5. | NEG
  6. | ADD
  7. | SUB
  8. | MUL
  9. | DIV
  10. | REAL
  11. | ROUND
  12. | EXACT
    (*

    same as round, but argument is exact representation

    *)
val find : Lang.lfun -> op * Ctypes.c_float
val code_lit : Ctypes.c_float -> float -> string option -> Lang.F.term
val float_lit : Ctypes.c_float -> Q.t -> string

Returns a string literal in decimal notation (without suffix) that reparses to the same value (when added suffix).

val float_of_int : Ctypes.c_float -> Lang.F.unop
val float_of_real : Ctypes.c_float -> Lang.F.unop
val real_of_float : Ctypes.c_float -> Lang.F.unop
val f_model : Ctypes.c_float -> Lang.lfun
val f_delta : Ctypes.c_float -> Lang.lfun
val f_epsilon : Ctypes.c_float -> Lang.lfun
val flt_of_real : Ctypes.c_float -> Lang.lfun
val real_of_flt : Ctypes.c_float -> Lang.lfun
val flt_add : Ctypes.c_float -> Lang.lfun
val flt_mul : Ctypes.c_float -> Lang.lfun
val flt_div : Ctypes.c_float -> Lang.lfun
val flt_neg : Ctypes.c_float -> Lang.lfun
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct