package frama-c

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Wp.CfloatSource

Floating Arithmetic Model

Sourceval f32 : Lang.adt
Sourceval f64 : Lang.adt
Sourceval fq32 : Lang.lfun
Sourceval fq64 : Lang.lfun
Sourcetype model =
  1. | Real
  2. | Float
Sourceval configure : model -> WpContext.rollback

model independant

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

with respect to model

Sourcetype 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

    *)
Sourceval code_lit : Ctypes.c_float -> float -> string option -> Lang.F.term
Sourceval 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).

Sourceval float_of_int : Ctypes.c_float -> Lang.F.unop
Sourceval float_of_real : Ctypes.c_float -> Lang.F.unop
Sourceval real_of_float : Ctypes.c_float -> Lang.F.unop
Sourceval f_epsilon : Ctypes.c_float -> Lang.lfun
Sourceval flt_of_real : Ctypes.c_float -> Lang.lfun
Sourceval real_of_flt : Ctypes.c_float -> Lang.lfun
OCaml

Innovation. Community. Security.