ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
libm.h File Reference
#include <stdint.h>
#include <float.h>
#include <math.h>
#include "endian.h"
Include dependency graph for libm.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define WANT_ROUNDING   1
#define WANT_SNAN   0
#define issignalingf_inline(x)
#define issignaling_inline(x)
#define TOINT_INTRINSICS   0
#define predict_true(x)
#define predict_false(x)
#define fp_barrierf   fp_barrierf
#define fp_barrier   fp_barrier
#define fp_barrierl   fp_barrierl
#define _UNUSED(expr)
#define fp_force_evalf   fp_force_evalf
#define fp_force_eval   fp_force_eval
#define fp_force_evall   fp_force_evall
#define FORCE_EVAL(x)
#define asuint(f)
#define asfloat(i)
#define asuint64(f)
#define asdouble(i)
#define EXTRACT_WORDS(hi, lo, d)
#define GET_HIGH_WORD(hi, d)
#define GET_LOW_WORD(lo, d)
#define INSERT_WORDS(d, hi, lo)
#define SET_HIGH_WORD(d, hi)
#define SET_LOW_WORD(d, lo)
#define GET_FLOAT_WORD(w, d)
#define SET_FLOAT_WORD(d, w)

Functions

static float eval_as_float (float x)
static double eval_as_double (double x)
static float fp_barrierf (float x)
static double fp_barrier (double x)
static long double fp_barrierl (long double x)
static void fp_force_evalf (float x)
static void fp_force_eval (double x)
static void fp_force_evall (long double x)
int __rem_pio2_large (double *, double *, int, int, int)
int __rem_pio2 (double, double *)
double __k_sin (double, double, int)
double __k_cos (double, double)
double __k_tan (double, double, int)
double __expo2 (double, double)
int __rem_pio2f (float, double *)
float __k_sindf (double)
float __k_cosdf (double)
float __k_tandf (double, int)
float __expo2f (float, float)
int __rem_pio2l (long double, long double *)
long double __k_sinl (long double, long double, int)
long double __k_cosl (long double, long double)
long double __k_tanl (long double, long double, int)
long double __polevll (long double, const long double *, int)
long double __p1evll (long double, const long double *, int)
double __lgamma_r (double, int *)
float __lgammaf_r (float, int *)
float __math_xflowf (uint32_t, float)
float __math_uflowf (uint32_t)
float __math_oflowf (uint32_t)
float __math_divzerof (uint32_t)
float __math_invalidf (float)
double __math_xflow (uint32_t, double)
double __math_uflow (uint32_t)
double __math_oflow (uint32_t)
double __math_divzero (uint32_t)
double __math_invalid (double)
double j0 (double x)
double j1 (double x)
double y0 (double x)
double y1 (double x)
float j0f (float x)
float y0f (float x)
float j1f (float x)
float y1f (float x)

Variables

int __signgam

Macro Definition Documentation

◆ _UNUSED

#define _UNUSED ( expr)
Value:
do { (void)(expr); } while (0)

◆ asdouble

#define asdouble ( i)
Value:
((union{uint64_t _i; double _f;}){i})._f

◆ asfloat

#define asfloat ( i)
Value:
((union{uint32_t _i; float _f;}){i})._f

◆ asuint

#define asuint ( f)
Value:
((union{float _f; uint32_t _i;}){f})._i

◆ asuint64

#define asuint64 ( f)
Value:
((union{double _f; uint64_t _i;}){f})._i

◆ EXTRACT_WORDS

#define EXTRACT_WORDS ( hi,
lo,
d )
Value:
do { \
uint64_t __u = asuint64(d); \
(hi) = __u >> 32; \
(lo) = (uint32_t)__u; \
} while (0)
#define asuint64(f)

◆ FORCE_EVAL

#define FORCE_EVAL ( x)
Value:
do { \
if (sizeof(x) == sizeof(float)) { \
fp_force_evalf(x); \
} else if (sizeof(x) == sizeof(double)) { \
fp_force_eval(x); \
} else { \
fp_force_evall(x); \
} \
} while(0)

◆ fp_barrier

#define fp_barrier   fp_barrier

◆ fp_barrierf

#define fp_barrierf   fp_barrierf

◆ fp_barrierl

#define fp_barrierl   fp_barrierl

◆ fp_force_eval

#define fp_force_eval   fp_force_eval

◆ fp_force_evalf

#define fp_force_evalf   fp_force_evalf

◆ fp_force_evall

#define fp_force_evall   fp_force_evall

◆ GET_FLOAT_WORD

#define GET_FLOAT_WORD ( w,
d )
Value:
do { \
(w) = asuint(d); \
} while (0)
#define asuint(f)

◆ GET_HIGH_WORD

#define GET_HIGH_WORD ( hi,
d )
Value:
do { \
(hi) = asuint64(d) >> 32; \
} while (0)

◆ GET_LOW_WORD

#define GET_LOW_WORD ( lo,
d )
Value:
do { \
(lo) = (uint32_t)asuint64(d); \
} while (0)

◆ INSERT_WORDS

#define INSERT_WORDS ( d,
hi,
lo )
Value:
do { \
(d) = asdouble(((uint64_t)(hi)<<32) | (uint32_t)(lo)); \
} while (0)
#define asdouble(i)

◆ issignaling_inline

#define issignaling_inline ( x)
Value:
0

◆ issignalingf_inline

#define issignalingf_inline ( x)
Value:
0

◆ predict_false

#define predict_false ( x)
Value:
(x)

◆ predict_true

#define predict_true ( x)
Value:
(x)

◆ SET_FLOAT_WORD

#define SET_FLOAT_WORD ( d,
w )
Value:
do { \
(d) = asfloat(w); \
} while (0)
#define asfloat(i)

◆ SET_HIGH_WORD

#define SET_HIGH_WORD ( d,
hi )
Value:
INSERT_WORDS(d, hi, (uint32_t)asuint64(d))
#define INSERT_WORDS(d, hi, lo)

◆ SET_LOW_WORD

#define SET_LOW_WORD ( d,
lo )
Value:
INSERT_WORDS(d, asuint64(d)>>32, lo)

◆ TOINT_INTRINSICS

#define TOINT_INTRINSICS   0

◆ WANT_ROUNDING

#define WANT_ROUNDING   1

◆ WANT_SNAN

#define WANT_SNAN   0

Function Documentation

◆ __expo2()

double __expo2 ( double ,
double  )

◆ __expo2f()

float __expo2f ( float ,
float  )

◆ __k_cos()

double __k_cos ( double ,
double  )

◆ __k_cosdf()

float __k_cosdf ( double x)

◆ __k_cosl()

long double __k_cosl ( long double ,
long double  )

◆ __k_sin()

double __k_sin ( double ,
double ,
int  )

◆ __k_sindf()

float __k_sindf ( double x)

◆ __k_sinl()

long double __k_sinl ( long double ,
long double ,
int  )

◆ __k_tan()

double __k_tan ( double ,
double ,
int  )

◆ __k_tandf()

float __k_tandf ( double ,
int  )

◆ __k_tanl()

long double __k_tanl ( long double ,
long double ,
int  )

◆ __lgamma_r()

double __lgamma_r ( double ,
int *  )

◆ __lgammaf_r()

float __lgammaf_r ( float ,
int *  )

◆ __math_divzero()

double __math_divzero ( uint32_t sign)

◆ __math_divzerof()

float __math_divzerof ( uint32_t sign)

◆ __math_invalid()

double __math_invalid ( double x)

◆ __math_invalidf()

float __math_invalidf ( float x)

◆ __math_oflow()

double __math_oflow ( uint32_t sign)

◆ __math_oflowf()

float __math_oflowf ( uint32_t sign)

◆ __math_uflow()

double __math_uflow ( uint32_t sign)

◆ __math_uflowf()

float __math_uflowf ( uint32_t sign)

◆ __math_xflow()

double __math_xflow ( uint32_t sign,
double y )

◆ __math_xflowf()

float __math_xflowf ( uint32_t sign,
float y )

◆ __p1evll()

long double __p1evll ( long double ,
const long double * ,
int  )

◆ __polevll()

long double __polevll ( long double ,
const long double * ,
int  )

◆ __rem_pio2()

int __rem_pio2 ( double ,
double *  )

◆ __rem_pio2_large()

int __rem_pio2_large ( double * x,
double * y,
int e0,
int nx,
int prec )

◆ __rem_pio2f()

int __rem_pio2f ( float x,
double * y )

◆ __rem_pio2l()

int __rem_pio2l ( long double ,
long double *  )

◆ eval_as_double()

double eval_as_double ( double x)
inlinestatic

◆ eval_as_float()

float eval_as_float ( float x)
inlinestatic

◆ fp_barrier()

double fp_barrier ( double x)
inlinestatic

◆ fp_barrierf()

float fp_barrierf ( float x)
inlinestatic

◆ fp_barrierl()

long double fp_barrierl ( long double x)
inlinestatic

◆ fp_force_eval()

void fp_force_eval ( double x)
inlinestatic

◆ fp_force_evalf()

void fp_force_evalf ( float x)
inlinestatic

◆ fp_force_evall()

void fp_force_evall ( long double x)
inlinestatic

◆ j0()

double j0 ( double x)

◆ j0f()

float j0f ( float x)

◆ j1()

double j1 ( double x)

◆ j1f()

float j1f ( float x)

◆ y0()

double y0 ( double x)

◆ y0f()

float y0f ( float x)

◆ y1()

double y1 ( double x)

◆ y1f()

float y1f ( float x)

Variable Documentation

◆ __signgam

int __signgam
extern