Frama-C:
Plug-ins:
Libraries:

Frama-C API - Cfloat

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