CBMC
Loading...
Searching...
No Matches
math.c File Reference
#include <math.h>
#include <limits.h>
#include <fenv.h>
#include <stdint.h>
#include <errno.h>
#include <float.h>
+ Include dependency graph for math.c:

Go to the source code of this file.

Classes

union  mixf
 
union  mixd
 
union  mixl
 

Macros

#define __CPROVER_MATH_H_INCLUDED
 
#define __CPROVER_LIMITS_H_INCLUDED
 
#define __CPROVER_FENV_H_INCLUDED
 
#define __CPROVER_STDINT_H_INCLUDED
 
#define __CPROVER_ERRNO_H_INCLUDED
 
#define __CPROVER_FLOAT_H_INCLUDED
 

Functions

double fabs (double d)
 
long double fabsl (long double d)
 
float fabsf (float f)
 
double __builtin_fabs (double d)
 
long double __builtin_fabsl (long double d)
 
float __builtin_fabsf (float f)
 
int __CPROVER_isgreaterf (float f, float g)
 
int __CPROVER_isgreaterd (double f, double g)
 
int __CPROVER_isgreaterequalf (float f, float g)
 
int __CPROVER_isgreaterequald (double f, double g)
 
int __CPROVER_islessf (float f, float g)
 
int __CPROVER_islessd (double f, double g)
 
int __CPROVER_islessequalf (float f, float g)
 
int __CPROVER_islessequald (double f, double g)
 
int __CPROVER_islessgreaterf (float f, float g)
 
int __CPROVER_islessgreaterd (double f, double g)
 
int __CPROVER_isunorderedf (float f, float g)
 
int __CPROVER_isunorderedd (double f, double g)
 
int isfinite (double d)
 
int __finite (double d)
 
int __finitef (float f)
 
int __finitel (long double ld)
 
int isinf (double d)
 
int __isinf (double d)
 
int isinff (float f)
 
int __isinff (float f)
 
int isinfl (long double ld)
 
int __isinfl (long double ld)
 
int isnan (double d)
 
int __isnan (double d)
 
int __isnanf (float f)
 
int isnanf (float f)
 
int isnanl (long double ld)
 
int __isnanl (long double ld)
 
int isnormal (double d)
 
int __isnormalf (float f)
 
int __builtin_isinf (double d)
 
int __builtin_isinff (float f)
 
int __builtin_isinfl (long double ld)
 
int __builtin_isnan (double d)
 
int __builtin_isnanf (float f)
 
float __builtin_huge_valf (void)
 
double __builtin_huge_val (void)
 
long double __builtin_huge_vall (void)
 
int _dsign (double d)
 
int _ldsign (long double ld)
 
int _fdsign (float f)
 
int signbit (double d)
 
int __signbitd (double d)
 
int __signbitf (float f)
 
int __signbit (double ld)
 
short _dclass (double d)
 
short _ldclass (long double ld)
 
short _fdclass (float f)
 
int __fpclassifyd (double d)
 
int __fpclassifyf (float f)
 
int __fpclassifyl (long double f)
 
int __fpclassify (double d)
 
double __VERIFIER_nondet_double (void)
 
double sin (double x)
 
long double __VERIFIER_nondet_long_double (void)
 
long double sinl (long double x)
 
float __VERIFIER_nondet_float (void)
 
float sinf (float x)
 
double cos (double x)
 
long double cosl (long double x)
 
float cosf (float x)
 
double __builtin_nan (const char *str)
 
float __builtin_nanf (const char *str)
 
double nan (const char *str)
 
float nanf (const char *str)
 
long double nanl (const char *str)
 
float nextUpf (float f)
 
double nextUp (double d)
 
long double nextUpl (long double d)
 
float sqrtf (float f)
 
double sqrt (double d)
 
long double sqrtl (long double d)
 
double fmax (double f, double g)
 
float fmaxf (float f, float g)
 
long double fmaxl (long double f, long double g)
 
double fmin (double f, double g)
 
float fminf (float f, float g)
 
long double fminl (long double f, long double g)
 
double fdim (double f, double g)
 
float fdimf (float f, float g)
 
long double fdiml (long double f, long double g)
 
double ceil (double x)
 
float ceilf (float x)
 
long double ceill (long double x)
 
double floor (double x)
 
float floorf (float x)
 
long double floorl (long double x)
 
double trunc (double x)
 
float truncf (float x)
 
long double truncl (long double x)
 
double round (double x)
 
float roundf (float x)
 
long double roundl (long double x)
 
double nearbyint (double x)
 
float nearbyintf (float x)
 
long double nearbyintl (long double x)
 
double rint (double x)
 
float rintf (float x)
 
long double rintl (long double x)
 
long int lrint (double x)
 
long int lrintf (float x)
 
long int lrintl (long double x)
 
long long int llrint (double x)
 
long long int llrintf (float x)
 
long long int llrintl (long double x)
 
long int lround (double x)
 
long int lroundf (float x)
 
long int lroundl (long double x)
 
long long int llround (double x)
 
long long int llroundf (float x)
 
long long int llroundl (long double x)
 
double modf (double x, double *iptr)
 
float modff (float x, float *iptr)
 
long double modfl (long double x, long double *iptr)
 
double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y)
 
float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y)
 
long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y)
 
double fmod (double x, double y)
 
float fmodf (float x, float y)
 
long double fmodl (long double x, long double y)
 
double remainder (double x, double y)
 
float remainderf (float x, float y)
 
long double remainderl (long double x, long double y)
 
double copysign (double x, double y)
 
float copysignf (float x, float y)
 
long double copysignl (long double x, long double y)
 
double exp2 (double x)
 
float exp2f (float x)
 
long double exp2l (long double x)
 
int32_t __VERIFIER_nondet_int32_t (void)
 
double exp (double x)
 
float expf (float x)
 
long double expl (long double x)
 
double log (double x)
 
float logf (float x)
 
long double logl (long double x)
 
double log2 (double x)
 
float log2f (float x)
 
long double log2l (long double x)
 
double log10 (double x)
 
float log10f (float x)
 
long double log10l (long double x)
 
double __builtin_inf (void)
 
double pow (double x, double y)
 
float __builtin_inff (void)
 
float powf (float x, float y)
 
long double __builtin_infl (void)
 
long double powl (long double x, long double y)
 
double fma (double x, double y, double z)
 
float fmaf (float x, float y, float z)
 
long double fmal (long double x, long double y, long double z)
 
double __builtin_powi (double x, int y)
 
float __builtin_powif (float x, int y)
 
long double __builtin_powil (long double x, int y)
 

Variables

int __CPROVER_rounding_mode
 

Macro Definition Documentation

◆ __CPROVER_ERRNO_H_INCLUDED

#define __CPROVER_ERRNO_H_INCLUDED

Definition at line 2181 of file math.c.

◆ __CPROVER_FENV_H_INCLUDED

#define __CPROVER_FENV_H_INCLUDED

Definition at line 846 of file math.c.

◆ __CPROVER_FLOAT_H_INCLUDED

#define __CPROVER_FLOAT_H_INCLUDED

Definition at line 2323 of file math.c.

◆ __CPROVER_LIMITS_H_INCLUDED

#define __CPROVER_LIMITS_H_INCLUDED

Definition at line 664 of file math.c.

◆ __CPROVER_MATH_H_INCLUDED

#define __CPROVER_MATH_H_INCLUDED

Definition at line 342 of file math.c.

◆ __CPROVER_STDINT_H_INCLUDED

#define __CPROVER_STDINT_H_INCLUDED

Definition at line 2176 of file math.c.

Function Documentation

◆ __builtin_fabs()

double __builtin_fabs ( double  d)

Definition at line 24 of file math.c.

◆ __builtin_fabsf()

float __builtin_fabsf ( float  f)

Definition at line 38 of file math.c.

◆ __builtin_fabsl()

long double __builtin_fabsl ( long double  d)

Definition at line 31 of file math.c.

◆ __builtin_huge_val()

double __builtin_huge_val ( void  )

Definition at line 267 of file math.c.

◆ __builtin_huge_valf()

float __builtin_huge_valf ( void  )

Definition at line 256 of file math.c.

◆ __builtin_huge_vall()

long double __builtin_huge_vall ( void  )

Definition at line 278 of file math.c.

◆ __builtin_inf()

double __builtin_inf ( void  )

◆ __builtin_inff()

float __builtin_inff ( void  )

◆ __builtin_infl()

long double __builtin_infl ( void  )

◆ __builtin_isinf()

int __builtin_isinf ( double  d)

Definition at line 221 of file math.c.

◆ __builtin_isinff()

int __builtin_isinff ( float  f)

Definition at line 228 of file math.c.

◆ __builtin_isinfl()

int __builtin_isinfl ( long double  ld)

Definition at line 235 of file math.c.

◆ __builtin_isnan()

int __builtin_isnan ( double  d)

Definition at line 242 of file math.c.

◆ __builtin_isnanf()

int __builtin_isnanf ( float  f)

Definition at line 249 of file math.c.

◆ __builtin_nan()

double __builtin_nan ( const char str)

Definition at line 586 of file math.c.

◆ __builtin_nanf()

float __builtin_nanf ( const char str)

Definition at line 599 of file math.c.

◆ __builtin_powi()

double __builtin_powi ( double  x,
int  y 
)

Definition at line 3663 of file math.c.

◆ __builtin_powif()

float __builtin_powif ( float  x,
int  y 
)

Definition at line 3782 of file math.c.

◆ __builtin_powil()

long double __builtin_powil ( long double  x,
int  y 
)

Definition at line 3898 of file math.c.

◆ __CPROVER_isgreaterd()

int __CPROVER_isgreaterd ( double  f,
double  g 
)

Definition at line 49 of file math.c.

◆ __CPROVER_isgreaterequald()

int __CPROVER_isgreaterequald ( double  f,
double  g 
)

Definition at line 57 of file math.c.

◆ __CPROVER_isgreaterequalf()

int __CPROVER_isgreaterequalf ( float  f,
float  g 
)

Definition at line 53 of file math.c.

◆ __CPROVER_isgreaterf()

int __CPROVER_isgreaterf ( float  f,
float  g 
)

Definition at line 45 of file math.c.

◆ __CPROVER_islessd()

int __CPROVER_islessd ( double  f,
double  g 
)

Definition at line 65 of file math.c.

◆ __CPROVER_islessequald()

int __CPROVER_islessequald ( double  f,
double  g 
)

Definition at line 73 of file math.c.

◆ __CPROVER_islessequalf()

int __CPROVER_islessequalf ( float  f,
float  g 
)

Definition at line 69 of file math.c.

◆ __CPROVER_islessf()

int __CPROVER_islessf ( float  f,
float  g 
)

Definition at line 61 of file math.c.

◆ __CPROVER_islessgreaterd()

int __CPROVER_islessgreaterd ( double  f,
double  g 
)

Definition at line 81 of file math.c.

◆ __CPROVER_islessgreaterf()

int __CPROVER_islessgreaterf ( float  f,
float  g 
)

Definition at line 77 of file math.c.

◆ __CPROVER_isunorderedd()

int __CPROVER_isunorderedd ( double  f,
double  g 
)

Definition at line 92 of file math.c.

◆ __CPROVER_isunorderedf()

int __CPROVER_isunorderedf ( float  f,
float  g 
)

Definition at line 85 of file math.c.

◆ __finite()

int __finite ( double  d)

Definition at line 105 of file math.c.

◆ __finitef()

int __finitef ( float  f)

Definition at line 109 of file math.c.

◆ __finitel()

int __finitel ( long double  ld)

Definition at line 113 of file math.c.

◆ __fpclassify()

int __fpclassify ( double  d)

Definition at line 449 of file math.c.

◆ __fpclassifyd()

int __fpclassifyd ( double  d)

Definition at line 396 of file math.c.

◆ __fpclassifyf()

int __fpclassifyf ( float  f)

Definition at line 410 of file math.c.

◆ __fpclassifyl()

int __fpclassifyl ( long double  f)

Definition at line 424 of file math.c.

◆ __isinf()

int __isinf ( double  d)

Definition at line 126 of file math.c.

◆ __isinff()

int __isinff ( float  f)

Definition at line 140 of file math.c.

◆ __isinfl()

int __isinfl ( long double  ld)

Definition at line 154 of file math.c.

◆ __isnan()

int __isnan ( double  d)

Definition at line 170 of file math.c.

◆ __isnanf()

int __isnanf ( float  f)

Definition at line 177 of file math.c.

◆ __isnanl()

int __isnanl ( long double  ld)

Definition at line 198 of file math.c.

◆ __isnormalf()

int __isnormalf ( float  f)

Definition at line 214 of file math.c.

◆ __signbit()

int __signbit ( double  ld)

Definition at line 333 of file math.c.

◆ __signbitd()

int __signbitd ( double  d)

Definition at line 319 of file math.c.

◆ __signbitf()

int __signbitf ( float  f)

Definition at line 326 of file math.c.

◆ __sort_of_CPROVER_remainder()

double __sort_of_CPROVER_remainder ( int  rounding_mode,
double  x,
double  y 
)

Definition at line 1905 of file math.c.

◆ __sort_of_CPROVER_remainderf()

float __sort_of_CPROVER_remainderf ( int  rounding_mode,
float  x,
float  y 
)

Definition at line 1920 of file math.c.

◆ __sort_of_CPROVER_remainderl()

long double __sort_of_CPROVER_remainderl ( int  rounding_mode,
long double  x,
long double  y 
)

Definition at line 1935 of file math.c.

◆ __VERIFIER_nondet_double()

double __VERIFIER_nondet_double ( void  )

◆ __VERIFIER_nondet_float()

float __VERIFIER_nondet_float ( void  )

◆ __VERIFIER_nondet_int32_t()

int32_t __VERIFIER_nondet_int32_t ( void  )

◆ __VERIFIER_nondet_long_double()

long double __VERIFIER_nondet_long_double ( void  )

◆ _dclass()

short _dclass ( double  d)

Definition at line 345 of file math.c.

◆ _dsign()

int _dsign ( double  d)

Definition at line 289 of file math.c.

◆ _fdclass()

short _fdclass ( float  f)

Definition at line 379 of file math.c.

◆ _fdsign()

int _fdsign ( float  f)

Definition at line 303 of file math.c.

◆ _ldclass()

short _ldclass ( long double  ld)

Definition at line 362 of file math.c.

◆ _ldsign()

int _ldsign ( long double  ld)

Definition at line 296 of file math.c.

◆ ceil()

double ceil ( double  x)

Definition at line 1232 of file math.c.

◆ ceilf()

float ceilf ( float  x)

Definition at line 1249 of file math.c.

◆ ceill()

long double ceill ( long double  x)

Definition at line 1267 of file math.c.

◆ copysign()

double copysign ( double  x,
double  y 
)

Definition at line 2092 of file math.c.

◆ copysignf()

float copysignf ( float  x,
float  y 
)

Definition at line 2107 of file math.c.

◆ copysignl()

long double copysignl ( long double  x,
long double  y 
)

Definition at line 2122 of file math.c.

◆ cos()

double cos ( double  x)

Definition at line 524 of file math.c.

◆ cosf()

float cosf ( float  x)

Definition at line 566 of file math.c.

◆ cosl()

long double cosl ( long double  x)

Definition at line 545 of file math.c.

◆ exp()

double exp ( double  x)

Definition at line 2186 of file math.c.

◆ exp2()

double exp2 ( double  x)

Definition at line 2135 of file math.c.

◆ exp2f()

float exp2f ( float  x)

Definition at line 2147 of file math.c.

◆ exp2l()

long double exp2l ( long double  x)

Definition at line 2159 of file math.c.

◆ expf()

float expf ( float  x)

Definition at line 2263 of file math.c.

◆ expl()

long double expl ( long double  x)

Definition at line 2338 of file math.c.

◆ fabs()

double fabs ( double  d)

Definition at line 3 of file math.c.

◆ fabsf()

float fabsf ( float  f)

Definition at line 17 of file math.c.

◆ fabsl()

long double fabsl ( long double  d)

Definition at line 10 of file math.c.

◆ fdim()

double fdim ( double  f,
double  g 
)

Definition at line 1192 of file math.c.

◆ fdimf()

float fdimf ( float  f,
float  g 
)

Definition at line 1202 of file math.c.

◆ fdiml()

long double fdiml ( long double  f,
long double  g 
)

Definition at line 1212 of file math.c.

◆ floor()

double floor ( double  x)

Definition at line 1290 of file math.c.

◆ floorf()

float floorf ( float  x)

Definition at line 1307 of file math.c.

◆ floorl()

long double floorl ( long double  x)

Definition at line 1325 of file math.c.

◆ fma()

double fma ( double  x,
double  y,
double  z 
)

Definition at line 3491 of file math.c.

◆ fmaf()

float fmaf ( float  x,
float  y,
float  z 
)

Definition at line 3543 of file math.c.

◆ fmal()

long double fmal ( long double  x,
long double  y,
long double  z 
)

Definition at line 3600 of file math.c.

◆ fmax()

double fmax ( double  f,
double  g 
)

Definition at line 1111 of file math.c.

◆ fmaxf()

float fmaxf ( float  f,
float  g 
)

Definition at line 1121 of file math.c.

◆ fmaxl()

long double fmaxl ( long double  f,
long double  g 
)

Definition at line 1131 of file math.c.

◆ fmin()

double fmin ( double  f,
double  g 
)

Definition at line 1154 of file math.c.

◆ fminf()

float fminf ( float  f,
float  g 
)

Definition at line 1164 of file math.c.

◆ fminl()

long double fminl ( long double  f,
long double  g 
)

Definition at line 1174 of file math.c.

◆ fmod()

double fmod ( double  x,
double  y 
)

Definition at line 1970 of file math.c.

◆ fmodf()

float fmodf ( float  x,
float  y 
)

Definition at line 1987 of file math.c.

◆ fmodl()

long double fmodl ( long double  x,
long double  y 
)

Definition at line 2004 of file math.c.

◆ isfinite()

int isfinite ( double  d)

Definition at line 101 of file math.c.

◆ isinf()

int isinf ( double  d)

Definition at line 119 of file math.c.

◆ isinff()

int isinff ( float  f)

Definition at line 133 of file math.c.

◆ isinfl()

int isinfl ( long double  ld)

Definition at line 147 of file math.c.

◆ isnan()

int isnan ( double  d)

Definition at line 163 of file math.c.

◆ isnanf()

int isnanf ( float  f)

Definition at line 184 of file math.c.

◆ isnanl()

int isnanl ( long double  ld)

Definition at line 191 of file math.c.

◆ isnormal()

int isnormal ( double  d)

Definition at line 207 of file math.c.

◆ llrint()

long long int llrint ( double  x)

Definition at line 1668 of file math.c.

◆ llrintf()

long long int llrintf ( float  x)

Definition at line 1688 of file math.c.

◆ llrintl()

long long int llrintl ( long double  x)

Definition at line 1709 of file math.c.

◆ llround()

long long int llround ( double  x)

Definition at line 1793 of file math.c.

◆ llroundf()

long long int llroundf ( float  x)

Definition at line 1811 of file math.c.

◆ llroundl()

long long int llroundl ( long double  x)

Definition at line 1830 of file math.c.

◆ log()

double log ( double  x)

Definition at line 2416 of file math.c.

◆ log10()

double log10 ( double  x)

Definition at line 2836 of file math.c.

◆ log10f()

float log10f ( float  x)

Definition at line 2906 of file math.c.

◆ log10l()

long double log10l ( long double  x)

Definition at line 2976 of file math.c.

◆ log2()

double log2 ( double  x)

Definition at line 2627 of file math.c.

◆ log2f()

float log2f ( float  x)

Definition at line 2694 of file math.c.

◆ log2l()

long double log2l ( long double  x)

Definition at line 2762 of file math.c.

◆ logf()

float logf ( float  x)

Definition at line 2484 of file math.c.

◆ logl()

long double logl ( long double  x)

Definition at line 2553 of file math.c.

◆ lrint()

long int lrint ( double  x)

Definition at line 1606 of file math.c.

◆ lrintf()

long int lrintf ( float  x)

Definition at line 1626 of file math.c.

◆ lrintl()

long int lrintl ( long double  x)

Definition at line 1647 of file math.c.

◆ lround()

long int lround ( double  x)

Definition at line 1737 of file math.c.

◆ lroundf()

long int lroundf ( float  x)

Definition at line 1755 of file math.c.

◆ lroundl()

long int lroundl ( long double  x)

Definition at line 1774 of file math.c.

◆ modf()

double modf ( double  x,
double iptr 
)

Definition at line 1857 of file math.c.

◆ modff()

float modff ( float  x,
float iptr 
)

Definition at line 1875 of file math.c.

◆ modfl()

long double modfl ( long double  x,
long double iptr 
)

Definition at line 1894 of file math.c.

◆ nan()

double nan ( const char str)

Definition at line 626 of file math.c.

◆ nanf()

float nanf ( const char str)

Definition at line 638 of file math.c.

◆ nanl()

long double nanl ( const char str)

Definition at line 650 of file math.c.

◆ nearbyint()

double nearbyint ( double  x)

Definition at line 1471 of file math.c.

◆ nearbyintf()

float nearbyintf ( float  x)

Definition at line 1490 of file math.c.

◆ nearbyintl()

long double nearbyintl ( long double  x)

Definition at line 1510 of file math.c.

◆ nextUp()

double nextUp ( double  d)

Definition at line 733 of file math.c.

◆ nextUpf()

float nextUpf ( float  f)

Definition at line 681 of file math.c.

◆ nextUpl()

long double nextUpl ( long double  d)

Definition at line 784 of file math.c.

◆ pow()

double pow ( double  x,
double  y 
)

Definition at line 3049 of file math.c.

◆ powf()

float powf ( float  x,
float  y 
)

Definition at line 3197 of file math.c.

◆ powl()

long double powl ( long double  x,
long double  y 
)

Definition at line 3342 of file math.c.

◆ remainder()

double remainder ( double  x,
double  y 
)

Definition at line 2036 of file math.c.

◆ remainderf()

float remainderf ( float  x,
float  y 
)

Definition at line 2053 of file math.c.

◆ remainderl()

long double remainderl ( long double  x,
long double  y 
)

Definition at line 2070 of file math.c.

◆ rint()

double rint ( double  x)

Definition at line 1538 of file math.c.

◆ rintf()

float rintf ( float  x)

Definition at line 1557 of file math.c.

◆ rintl()

long double rintl ( long double  x)

Definition at line 1576 of file math.c.

◆ round()

double round ( double  x)

Definition at line 1408 of file math.c.

◆ roundf()

float roundf ( float  x)

Definition at line 1425 of file math.c.

◆ roundl()

long double roundl ( long double  x)

Definition at line 1443 of file math.c.

◆ signbit()

int signbit ( double  d)

Definition at line 312 of file math.c.

◆ sin()

double sin ( double  x)

Definition at line 461 of file math.c.

◆ sinf()

float sinf ( float  x)

Definition at line 503 of file math.c.

◆ sinl()

long double sinl ( long double  x)

Definition at line 482 of file math.c.

◆ sqrt()

double sqrt ( double  d)

Definition at line 946 of file math.c.

◆ sqrtf()

float sqrtf ( float  f)

Definition at line 853 of file math.c.

◆ sqrtl()

long double sqrtl ( long double  d)

Definition at line 1023 of file math.c.

◆ trunc()

double trunc ( double  x)

Definition at line 1349 of file math.c.

◆ truncf()

float truncf ( float  x)

Definition at line 1366 of file math.c.

◆ truncl()

long double truncl ( long double  x)

Definition at line 1384 of file math.c.

Variable Documentation

◆ __CPROVER_rounding_mode

int __CPROVER_rounding_mode
extern

Definition at line 1488 of file math.c.