CBMC
Loading...
Searching...
No Matches
Classes | Macros | Functions | Variables
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

 
 
 
 
 
 

Functions

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
double  nan (const char *str)
 
float  nanf (const char *str)
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Variables

 

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 charstr )

Definition at line 586 of file math.c.

◆  __builtin_nanf()

float __builtin_nanf ( const charstr )

Definition at line 599 of file math.c.

◆  __builtin_powi()

double __builtin_powi ( double  x,
int  y 
)

Definition at line 3583 of file math.c.

◆  __builtin_powif()

float __builtin_powif ( float  x,
int  y 
)

Definition at line 3702 of file math.c.

◆  __builtin_powil()

long double __builtin_powil ( long double  x,
int  y 
)

Definition at line 3818 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 3489 of file math.c.

◆  fmaf()

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

Definition at line 3518 of file math.c.

◆  fmal()

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

Definition at line 3546 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,
doubleiptr 
)

Definition at line 1857 of file math.c.

◆  modff()

float modff ( float  x,
floatiptr 
)

Definition at line 1875 of file math.c.

◆  modfl()

long double modfl ( long double  x,
long doubleiptr 
)

Definition at line 1894 of file math.c.

◆  nan()

double nan ( const charstr )

Definition at line 626 of file math.c.

◆  nanf()

float nanf ( const charstr )

Definition at line 638 of file math.c.

◆  nanl()

long double nanl ( const charstr )

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.

AltStyle によって変換されたページ (->オリジナル) /