Skip to content
Snippets Groups Projects
Commit 8c1a50fa authored by Andre Maroneze's avatar Andre Maroneze Committed by David Bühler
Browse files

[Libc] add minimal specs for frexp and ldexp

parent ba6b0900
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
share/libc/math.h
+ 28
− 0
View file @ 8c1a50fa
......@@ -653,16 +653,44 @@ extern double expm1(double x);
extern float expm1f(float x);
extern long double expm1l(long double x);
/*@
requires valid_exp: \valid(exp);
assigns \result, *exp \from value;
ensures initialization:exp:\initialized(exp);
*/
extern double frexp(double value, int *exp);
/*@
requires valid_exp: \valid(exp);
assigns \result, *exp \from value;
ensures initialization:exp:\initialized(exp);
*/
extern float frexpf(float value, int *exp);
/*@
requires valid_exp: \valid(exp);
assigns \result, *exp \from value;
ensures initialization:exp:\initialized(exp);
*/
extern long double frexpl(long double value, int *exp);
extern int ilogb(double x);
extern int ilogbf(float x);
extern int ilogbl(long double x);
/*@
assigns \result \from x, exp;
*/
extern double ldexp(double x, int exp);
/*@
assigns \result \from x, exp;
*/
extern float ldexpf(float x, int exp);
/*@
assigns \result \from x, exp;
*/
extern long double ldexpl(long double x, int exp);
/*@
......
src/plugins/report/tests/report/oracle/csv.csv
+ 1
− 1
View file @ 8c1a50fa
directory file line function property kind status property
FRAMAC_SHARE/libc math.h 1032 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
FRAMAC_SHARE/libc math.h 1060 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
tests/report csv.c 11 main1 signed_overflow Unknown -2147483648 ≤ x * x
tests/report csv.c 11 main1 signed_overflow Unknown x * x ≤ 2147483647
tests/report csv.c 12 main1 index_bound Unknown 0 ≤ x
......
tests/idct/oracle/ieee_1180_1990.res.oracle
+ 147
− 45
View file @ 8c1a50fa
......@@ -2961,6 +2961,108 @@
behavior underflow
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'frexp'
--------------------------------------------------------------------------------
[ Extern ] Post-condition 'initialization,exp'
ensures initialization: exp: \initialized(\old(exp))
Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/math.h, line 658)
assigns \result, *exp;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 658)
assigns \result \from value;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 658)
assigns *exp \from value;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'frexpf'
--------------------------------------------------------------------------------
[ Extern ] Post-condition 'initialization,exp'
ensures initialization: exp: \initialized(\old(exp))
Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/math.h, line 665)
assigns \result, *exp;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 665)
assigns \result \from value;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 665)
assigns *exp \from value;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'frexpl'
--------------------------------------------------------------------------------
[ Extern ] Post-condition 'initialization,exp'
ensures initialization: exp: \initialized(\old(exp))
Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/math.h, line 672)
assigns \result, *exp;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 672)
assigns \result \from value;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 672)
assigns *exp \from value;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'ldexp'
--------------------------------------------------------------------------------
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 682)
assigns \result \from x, exp;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'ldexpf'
--------------------------------------------------------------------------------
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 687)
assigns \result \from x, exp;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'ldexpl'
--------------------------------------------------------------------------------
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 692)
assigns \result \from x, exp;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'log'
--------------------------------------------------------------------------------
......@@ -2974,7 +3076,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 673)
[ Extern ] Froms (file share/libc/math.h, line 701)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -2994,7 +3096,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 704)
[ Extern ] Froms (file share/libc/math.h, line 732)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3014,7 +3116,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 735)
[ Extern ] Froms (file share/libc/math.h, line 763)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3034,7 +3136,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 766)
[ Extern ] Froms (file share/libc/math.h, line 794)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3054,7 +3156,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 797)
[ Extern ] Froms (file share/libc/math.h, line 825)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3074,7 +3176,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 828)
[ Extern ] Froms (file share/libc/math.h, line 856)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3094,7 +3196,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 863)
[ Extern ] Froms (file share/libc/math.h, line 891)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3114,7 +3216,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 894)
[ Extern ] Froms (file share/libc/math.h, line 922)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3134,7 +3236,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 925)
[ Extern ] Froms (file share/libc/math.h, line 953)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3159,7 +3261,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 972)
[ Extern ] Froms (file share/libc/math.h, line 1000)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3184,7 +3286,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 990)
[ Extern ] Froms (file share/libc/math.h, line 1018)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3209,7 +3311,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1008)
[ Extern ] Froms (file share/libc/math.h, line 1036)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3227,13 +3329,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/math.h, line 1030)
[ Extern ] Assigns (file share/libc/math.h, line 1058)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1030)
[ Extern ] Froms (file share/libc/math.h, line 1058)
assigns __fc_errno \from x, y;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1030)
[ Extern ] Froms (file share/libc/math.h, line 1058)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3251,13 +3353,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/math.h, line 1045)
[ Extern ] Assigns (file share/libc/math.h, line 1073)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1045)
[ Extern ] Froms (file share/libc/math.h, line 1073)
assigns __fc_errno \from x, y;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1045)
[ Extern ] Froms (file share/libc/math.h, line 1073)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3289,7 +3391,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1066)
[ Extern ] Froms (file share/libc/math.h, line 1094)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3315,7 +3417,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1095)
[ Extern ] Froms (file share/libc/math.h, line 1123)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3338,7 +3440,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1124)
[ Extern ] Froms (file share/libc/math.h, line 1152)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3355,7 +3457,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1164)
[ Extern ] Froms (file share/libc/math.h, line 1192)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3372,7 +3474,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1181)
[ Extern ] Froms (file share/libc/math.h, line 1209)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3389,7 +3491,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1198)
[ Extern ] Froms (file share/libc/math.h, line 1226)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3406,7 +3508,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1215)
[ Extern ] Froms (file share/libc/math.h, line 1243)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3423,7 +3525,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1232)
[ Extern ] Froms (file share/libc/math.h, line 1260)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3440,7 +3542,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1249)
[ Extern ] Froms (file share/libc/math.h, line 1277)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3457,7 +3559,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1282)
[ Extern ] Froms (file share/libc/math.h, line 1310)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3474,7 +3576,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1299)
[ Extern ] Froms (file share/libc/math.h, line 1327)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3491,7 +3593,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1316)
[ Extern ] Froms (file share/libc/math.h, line 1344)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3508,7 +3610,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1341)
[ Extern ] Froms (file share/libc/math.h, line 1369)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3525,7 +3627,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1358)
[ Extern ] Froms (file share/libc/math.h, line 1386)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3542,7 +3644,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1375)
[ Extern ] Froms (file share/libc/math.h, line 1403)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3562,7 +3664,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1395)
[ Extern ] Froms (file share/libc/math.h, line 1423)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3582,7 +3684,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1416)
[ Extern ] Froms (file share/libc/math.h, line 1444)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3599,7 +3701,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1449)
[ Extern ] Froms (file share/libc/math.h, line 1477)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3616,7 +3718,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1456)
[ Extern ] Froms (file share/libc/math.h, line 1484)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3633,7 +3735,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1463)
[ Extern ] Froms (file share/libc/math.h, line 1491)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3653,7 +3755,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1493)
[ Extern ] Froms (file share/libc/math.h, line 1521)
assigns \result \from f;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3679,7 +3781,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1506)
[ Extern ] Froms (file share/libc/math.h, line 1534)
assigns \result \from d;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3702,7 +3804,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1533)
[ Extern ] Froms (file share/libc/math.h, line 1561)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -3719,7 +3821,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 1539)
[ Extern ] Froms (file share/libc/math.h, line 1567)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
......@@ -4081,9 +4183,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
173 Completely validated
179 Completely validated
16 Locally validated
488 Considered valid
506 Considered valid
56 To be validated
733 Total
757 Total
--------------------------------------------------------------------------------
tests/libc/math_h.c
+ 35
− 17
View file @ 8c1a50fa
......@@ -28,26 +28,28 @@ const long double huge_vall = HUGE_VALL;
const float infinity = INFINITY;
const double fp_ilogb0 = FP_ILOGB0;
const double fp_ilogbnan = FP_ILOGBNAN;
volatile int int_top;
#define TEST_VAL(type,f,c) type f##_##c = f(c)
#define TEST_FUN(type,f,prefix) \
TEST_VAL(type,f,prefix##pi); \
TEST_VAL(type,f,prefix##half_pi); \
TEST_VAL(type,f,prefix##e); \
TEST_VAL(type,f,zero); \
TEST_VAL(type,f,minus_zero); \
TEST_VAL(type,f,one); \
TEST_VAL(type,f,minus_one); \
TEST_VAL(type,f,large); \
TEST_VAL(type,f,prefix##top)
#define TEST_VAL_CONST(type,f,cst) type f##_##cst = f(cst)
#define TEST_FUN_CONSTS(type,f,prefix) \
TEST_VAL_CONST(type,f,prefix##pi); \
TEST_VAL_CONST(type,f,prefix##half_pi); \
TEST_VAL_CONST(type,f,prefix##e); \
TEST_VAL_CONST(type,f,zero); \
TEST_VAL_CONST(type,f,minus_zero); \
TEST_VAL_CONST(type,f,one); \
TEST_VAL_CONST(type,f,minus_one); \
TEST_VAL_CONST(type,f,large); \
TEST_VAL_CONST(type,f,prefix##top)
void test_simple_specs(void);
int main() {
TEST_FUN(double,atan,);
TEST_FUN(float,atanf,f_);
TEST_FUN(long double,atanl,ld_);
TEST_FUN(double,fabs,);
TEST_FUN(float,fabsf,f_);
TEST_FUN(long double,fabsl,ld_);
TEST_FUN_CONSTS(double,atan,);
TEST_FUN_CONSTS(float,atanf,f_);
TEST_FUN_CONSTS(long double,atanl,ld_);
TEST_FUN_CONSTS(double,fabs,);
TEST_FUN_CONSTS(float,fabsf,f_);
TEST_FUN_CONSTS(long double,fabsl,ld_);
#ifdef NONFINITE
int r;
......@@ -64,4 +66,20 @@ int main() {
r = isfinite(NAN);
//@ assert !r;
#endif
test_simple_specs();
}
#define TEST_VAL_VAR(type,fn,...) type res_##fn = fn(__VA_ARGS__)
#define TEST_FUN_VAR(fn,...) \
TEST_VAL_VAR(double,fn,__VA_ARGS__); \
TEST_VAL_VAR(float,fn##f,__VA_ARGS__); \
TEST_VAL_VAR(long double,fn##l,__VA_ARGS__);
void test_simple_specs() {
int exponent;
TEST_FUN_VAR(frexp, ld_top, &exponent);
TEST_FUN_VAR(ldexp, ld_top, int_top);
//@ assert \initialized(&exponent);
}
tests/libc/oracle/fc_libc.0.res.oracle
+ 18
− 16
View file @ 8c1a50fa
......@@ -41,7 +41,7 @@
wcscpy (0 call); wcsdup (0 call); wcslen (3 calls); wcsncat (0 call);
wcsncpy (0 call); wmemcpy (1 call); wmemset (0 call);
Specified-only functions (416)
Specified-only functions (422)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
......@@ -95,8 +95,9 @@
flockfile (0 call); floor (0 call); floorf (0 call); floorl (0 call);
fmod (0 call); fmodf (0 call); fopen (0 call); fork (0 call);
fputc (0 call); fputs (0 call); fread (0 call); free (1 call);
freeaddrinfo (0 call); freopen (0 call); fseek (0 call); fseeko (0 call);
fsetpos (0 call); ftell (0 call); ftello (0 call); ftrylockfile (0 call);
freeaddrinfo (0 call); freopen (0 call); frexp (0 call); frexpf (0 call);
frexpl (0 call); fseek (0 call); fseeko (0 call); fsetpos (0 call);
ftell (0 call); ftello (0 call); ftrylockfile (0 call);
funlockfile (0 call); fwrite (0 call); gai_strerror (0 call); getc (0 call);
getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
......@@ -111,18 +112,19 @@
iconv_open (0 call); inet_addr (2 calls); inet_ntoa (0 call);
inet_ntop (0 call); inet_pton (0 call); isascii (0 call); isatty (0 call);
jrand48 (0 call); kill (0 call); killpg (0 call); labs (0 call);
lcong48 (0 call); ldiv (0 call); listen (0 call); llabs (0 call);
lldiv (0 call); localtime (0 call); log (0 call); log10 (0 call);
log10f (0 call); log10l (0 call); log2 (0 call); log2f (0 call);
log2l (0 call); logf (0 call); logl (0 call); longjmp (0 call);
lrand48 (0 call); lseek (0 call); lstat (0 call); makedev (0 call);
malloc (10 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
mkdir (0 call); mkfifo (0 call); mknod (0 call); mkstemp (0 call);
mktime (0 call); mrand48 (0 call); nan (0 call); nanf (0 call);
nanl (0 call); nanosleep (0 call); nrand48 (0 call); ntohl (0 call);
ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
openlog (0 call); pathconf (0 call); pclose (0 call); perror (0 call);
pipe (0 call); poll (0 call); popen (0 call); pow (0 call); powf (0 call);
lcong48 (0 call); ldexp (0 call); ldexpf (0 call); ldexpl (0 call);
ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
lseek (0 call); lstat (0 call); makedev (0 call); malloc (10 calls);
mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call);
mkfifo (0 call); mknod (0 call); mkstemp (0 call); mktime (0 call);
mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
poll (0 call); popen (0 call); pow (0 call); powf (0 call);
pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
pthread_cond_init (0 call); pthread_cond_wait (0 call);
pthread_create (0 call); pthread_join (0 call);
......@@ -194,7 +196,7 @@
Goto = 99
Assignment = 466
Exit point = 84
Function = 501
Function = 507
Function call = 98
Pointer dereferencing = 161
Cyclomatic complexity = 299
......
tests/libc/oracle/fc_libc.1.res.oracle
+ 36
− 0
View file @ 8c1a50fa
......@@ -3081,6 +3081,42 @@ extern double exp(double x);
*/
extern float expf(float x);
/*@ requires valid_exp: \valid(exp);
ensures initialization: exp: \initialized(\old(exp));
assigns \result, *exp;
assigns \result \from value;
assigns *exp \from value;
*/
extern double frexp(double value, int *exp);
/*@ requires valid_exp: \valid(exp);
ensures initialization: exp: \initialized(\old(exp));
assigns \result, *exp;
assigns \result \from value;
assigns *exp \from value;
*/
extern float frexpf(float value, int *exp);
/*@ requires valid_exp: \valid(exp);
ensures initialization: exp: \initialized(\old(exp));
assigns \result, *exp;
assigns \result \from value;
assigns *exp \from value;
*/
extern long double frexpl(long double value, int *exp);
/*@ assigns \result;
assigns \result \from x, exp; */
extern double ldexp(double x, int exp);
/*@ assigns \result;
assigns \result \from x, exp; */
extern float ldexpf(float x, int exp);
/*@ assigns \result;
assigns \result \from x, exp; */
extern long double ldexpl(long double x, int exp);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
......
tests/libc/oracle/math_h.res.oracle
+ 139
− 95
View file @ 8c1a50fa
......@@ -29,255 +29,299 @@
infinity ∈ {inf}
fp_ilogb0 ∈ {-2147483648.}
fp_ilogbnan ∈ {-2147483648.}
[eva] tests/libc/math_h.c:45: Call to builtin atan
[eva] tests/libc/math_h.c:45: Call to builtin atan
[eva] tests/libc/math_h.c:45: Call to builtin atan
[eva] tests/libc/math_h.c:45: Call to builtin atan
[eva] tests/libc/math_h.c:45: Call to builtin atan
[eva] tests/libc/math_h.c:45: Call to builtin atan
[eva] tests/libc/math_h.c:45: Call to builtin atan
[eva] tests/libc/math_h.c:45: Call to builtin atan
[eva] tests/libc/math_h.c:45: Call to builtin atan
[eva] tests/libc/math_h.c:46: Call to builtin atanf
[eva] tests/libc/math_h.c:46: Call to builtin atanf
[eva] tests/libc/math_h.c:46: Call to builtin atanf
[eva] tests/libc/math_h.c:46: Call to builtin atanf
[eva] tests/libc/math_h.c:46: Call to builtin atanf
[eva] tests/libc/math_h.c:46: Call to builtin atanf
[eva] tests/libc/math_h.c:46: Call to builtin atanf
[eva] tests/libc/math_h.c:46: Call to builtin atanf
[eva] tests/libc/math_h.c:46: Call to builtin atanf
int_top ∈ [--..--]
[eva] tests/libc/math_h.c:47: Call to builtin atan
[eva] tests/libc/math_h.c:47: Call to builtin atan
[eva] tests/libc/math_h.c:47: Call to builtin atan
[eva] tests/libc/math_h.c:47: Call to builtin atan
[eva] tests/libc/math_h.c:47: Call to builtin atan
[eva] tests/libc/math_h.c:47: Call to builtin atan
[eva] tests/libc/math_h.c:47: Call to builtin atan
[eva] tests/libc/math_h.c:47: Call to builtin atan
[eva] tests/libc/math_h.c:47: Call to builtin atan
[eva] tests/libc/math_h.c:48: Call to builtin atanf
[eva] tests/libc/math_h.c:48: Call to builtin atanf
[eva] tests/libc/math_h.c:48: Call to builtin atanf
[eva] tests/libc/math_h.c:48: Call to builtin atanf
[eva] tests/libc/math_h.c:48: Call to builtin atanf
[eva] tests/libc/math_h.c:48: Call to builtin atanf
[eva] tests/libc/math_h.c:48: Call to builtin atanf
[eva] tests/libc/math_h.c:48: Call to builtin atanf
[eva] tests/libc/math_h.c:48: Call to builtin atanf
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
Called from tests/libc/math_h.c:49.
[eva] using specification for function atanl
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] using specification for function fabs
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
Called from tests/libc/math_h.c:51.
[eva] using specification for function fabsf
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] using specification for function fabsl
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function __finite <- main.
Called from tests/libc/math_h.c:54.
Called from tests/libc/math_h.c:56.
[eva] using specification for function __finite
[eva] Done for function __finite
[eva] tests/libc/math_h.c:55: assertion got status valid.
[eva] tests/libc/math_h.c:57: assertion got status valid.
[eva] computing for function __finite <- main.
Called from tests/libc/math_h.c:56.
Called from tests/libc/math_h.c:58.
[eva] Done for function __finite
[eva] computing for function __finite <- main.
Called from tests/libc/math_h.c:56.
Called from tests/libc/math_h.c:58.
[eva] Done for function __finite
[eva] tests/libc/math_h.c:57: assertion got status valid.
[eva] tests/libc/math_h.c:59: assertion got status valid.
[eva] computing for function __finitef <- main.
Called from tests/libc/math_h.c:58.
Called from tests/libc/math_h.c:60.
[eva] using specification for function __finitef
[eva] Done for function __finitef
[eva] computing for function __finitef <- main.
Called from tests/libc/math_h.c:58.
Called from tests/libc/math_h.c:60.
[eva] Done for function __finitef
[eva] tests/libc/math_h.c:59: assertion got status valid.
[eva] tests/libc/math_h.c:61: assertion got status valid.
[eva] computing for function __finite <- main.
Called from tests/libc/math_h.c:60.
Called from tests/libc/math_h.c:62.
[eva] Done for function __finite
[eva] computing for function __finite <- main.
Called from tests/libc/math_h.c:60.
[eva] Done for function __finite
[eva] tests/libc/math_h.c:61: assertion got status valid.
[eva] computing for function __finitef <- main.
Called from tests/libc/math_h.c:62.
[eva] Done for function __finitef
[eva] Done for function __finite
[eva] tests/libc/math_h.c:63: assertion got status valid.
[eva] computing for function __finitef <- main.
Called from tests/libc/math_h.c:64.
[eva] Done for function __finitef
[eva] tests/libc/math_h.c:65: assertion got status valid.
[eva] computing for function __finitef <- main.
Called from tests/libc/math_h.c:66.
[eva] Done for function __finitef
[eva] tests/libc/math_h.c:67: assertion got status valid.
[eva] computing for function test_simple_specs <- main.
Called from tests/libc/math_h.c:70.
[eva] computing for function frexp <- test_simple_specs <- main.
Called from tests/libc/math_h.c:82.
[eva] using specification for function frexp
[eva] tests/libc/math_h.c:82:
function frexp: precondition 'valid_exp' got status valid.
[eva] Done for function frexp
[eva] computing for function frexpf <- test_simple_specs <- main.
Called from tests/libc/math_h.c:82.
[eva] using specification for function frexpf
[eva] tests/libc/math_h.c:82:
function frexpf: precondition 'valid_exp' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpl <- test_simple_specs <- main.
Called from tests/libc/math_h.c:82.
[eva] using specification for function frexpl
[eva] tests/libc/math_h.c:82:
function frexpl: precondition 'valid_exp' got status valid.
[eva] Done for function frexpl
[eva] computing for function ldexp <- test_simple_specs <- main.
Called from tests/libc/math_h.c:83.
[eva] using specification for function ldexp
[eva] Done for function ldexp
[eva] computing for function ldexpf <- test_simple_specs <- main.
Called from tests/libc/math_h.c:83.
[eva] using specification for function ldexpf
[eva] Done for function ldexpf
[eva] computing for function ldexpl <- test_simple_specs <- main.
Called from tests/libc/math_h.c:83.
[eva] using specification for function ldexpl
[eva] Done for function ldexpl
[eva] tests/libc/math_h.c:84: assertion got status valid.
[eva] Recording results for test_simple_specs
[eva] Done for function test_simple_specs
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function test_simple_specs:
exponent ∈ [--..--]
res_frexp ∈ [-inf .. inf] ∪ {NaN}
res_frexpf ∈ [-inf .. inf] ∪ {NaN}
res_frexpl ∈ [-inf .. inf] ∪ {NaN}
res_ldexp ∈ [-inf .. inf] ∪ {NaN}
res_ldexpf ∈ [-inf .. inf] ∪ {NaN}
res_ldexpl ∈ [-inf .. inf] ∪ {NaN}
[eva:final-states] Values at end of function main:
atan_pi ∈ {1.26262725568}
atan_half_pi ∈ {1.00388482185}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment