Frama-C API - Cfloat
Floating Arithmetic Model
val ft32 : Lang.adt Lang.externval ft64 : Lang.adt Lang.externval f32 : Lang.F.tau Lang.externval f64 : Lang.F.tau Lang.externval fq32 : Lang.lfun Lang.externval fq64 : Lang.lfun Lang.externval configure : model -> WpContext.rollbackval ftau : Ctypes.c_float -> Lang.F.taumodel independent
val tau_of_float : Ctypes.c_float -> Lang.F.tauwith respect to model
val find : Lang.lfun -> op * Ctypes.c_floatval code_lit : Ctypes.c_float -> float -> string option -> Lang.F.termval acsl_lit : Frama_c_kernel.Cil_types.logic_real -> Lang.F.termval float_lit : Ctypes.c_float -> Q.t -> stringReturns 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.unopval float_of_real : Ctypes.c_float -> Lang.F.unopval real_of_float : Ctypes.c_float -> Lang.F.unopval fopp : Ctypes.c_float -> Lang.F.unopval fadd : Ctypes.c_float -> Lang.F.binopval fsub : Ctypes.c_float -> Lang.F.binopval fmul : Ctypes.c_float -> Lang.F.binopval fdiv : Ctypes.c_float -> Lang.F.binopval flt : Ctypes.c_float -> Lang.F.cmpval fle : Ctypes.c_float -> Lang.F.cmpval feq : Ctypes.c_float -> Lang.F.cmpval fneq : Ctypes.c_float -> Lang.F.cmpval f_model : Ctypes.c_float -> Lang.lfun Lang.externval f_delta : Ctypes.c_float -> Lang.lfun Lang.externval f_epsilon : Ctypes.c_float -> Lang.lfun Lang.externval flt_of_real : Ctypes.c_float -> Lang.lfun Lang.externval real_of_flt : Ctypes.c_float -> Lang.lfun Lang.externval flt_add : Ctypes.c_float -> Lang.lfun Lang.externval flt_mul : Ctypes.c_float -> Lang.lfun Lang.externval flt_div : Ctypes.c_float -> Lang.lfun Lang.externval flt_neg : Ctypes.c_float -> Lang.lfun Lang.extern