|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include "libm.h"Functions | |
| static float | erfc1 (float x) |
| static float | erfc2 (uint32_t ix, float x) |
| float | erff (float x) |
| float | erfcf (float x) |
Variables | |
| static const float | erx = 8.4506291151e-01 |
| static const float | efx8 = 1.0270333290e+00 |
| static const float | pp0 = 1.2837916613e-01 |
| static const float | pp1 = -3.2504209876e-01 |
| static const float | pp2 = -2.8481749818e-02 |
| static const float | pp3 = -5.7702702470e-03 |
| static const float | pp4 = -2.3763017452e-05 |
| static const float | qq1 = 3.9791721106e-01 |
| static const float | qq2 = 6.5022252500e-02 |
| static const float | qq3 = 5.0813062117e-03 |
| static const float | qq4 = 1.3249473704e-04 |
| static const float | qq5 = -3.9602282413e-06 |
| static const float | pa0 = -2.3621185683e-03 |
| static const float | pa1 = 4.1485610604e-01 |
| static const float | pa2 = -3.7220788002e-01 |
| static const float | pa3 = 3.1834661961e-01 |
| static const float | pa4 = -1.1089469492e-01 |
| static const float | pa5 = 3.5478305072e-02 |
| static const float | pa6 = -2.1663755178e-03 |
| static const float | qa1 = 1.0642088205e-01 |
| static const float | qa2 = 5.4039794207e-01 |
| static const float | qa3 = 7.1828655899e-02 |
| static const float | qa4 = 1.2617121637e-01 |
| static const float | qa5 = 1.3637083583e-02 |
| static const float | qa6 = 1.1984500103e-02 |
| static const float | ra0 = -9.8649440333e-03 |
| static const float | ra1 = -6.9385856390e-01 |
| static const float | ra2 = -1.0558626175e+01 |
| static const float | ra3 = -6.2375331879e+01 |
| static const float | ra4 = -1.6239666748e+02 |
| static const float | ra5 = -1.8460508728e+02 |
| static const float | ra6 = -8.1287437439e+01 |
| static const float | ra7 = -9.8143291473e+00 |
| static const float | sa1 = 1.9651271820e+01 |
| static const float | sa2 = 1.3765776062e+02 |
| static const float | sa3 = 4.3456588745e+02 |
| static const float | sa4 = 6.4538726807e+02 |
| static const float | sa5 = 4.2900814819e+02 |
| static const float | sa6 = 1.0863500214e+02 |
| static const float | sa7 = 6.5702495575e+00 |
| static const float | sa8 = -6.0424413532e-02 |
| static const float | rb0 = -9.8649431020e-03 |
| static const float | rb1 = -7.9928326607e-01 |
| static const float | rb2 = -1.7757955551e+01 |
| static const float | rb3 = -1.6063638306e+02 |
| static const float | rb4 = -6.3756646729e+02 |
| static const float | rb5 = -1.0250950928e+03 |
| static const float | rb6 = -4.8351919556e+02 |
| static const float | sb1 = 3.0338060379e+01 |
| static const float | sb2 = 3.2579251099e+02 |
| static const float | sb3 = 1.5367296143e+03 |
| static const float | sb4 = 3.1998581543e+03 |
| static const float | sb5 = 2.5530502930e+03 |
| static const float | sb6 = 4.7452853394e+02 |
| static const float | sb7 = -2.2440952301e+01 |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |