From d5c3a5447458e54fcfea363b64a8c3ac8e4a079a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 11 Oct 2021 16:41:29 +0200
Subject: [PATCH] [libc] Updates test oracles.
The preconditions generated in place of behaviors leading to NaN or infinite
floating-point values are now named.
---
tests/libc/oracle/fc_libc.1.res.oracle | 8 +-
tests/libc/oracle/math_h.1.res.oracle | 457 +++++++++++++++----------
tests/libc/oracle/math_h.2.res.oracle | 234 +++++--------
3 files changed, 375 insertions(+), 324 deletions(-)
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index cb12a8c02f4..1cf9de7928f 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3758,8 +3758,8 @@ extern float sinf(float x);
*/
extern long double sinl(long double x);
-/*@ requires ¬(infinite_arg: \is_infinite(x));
- requires ¬(nan_arg: \is_NaN(x));
+/*@ requires not_infinity: ¬(infinite_arg: \is_infinite(x));
+ requires not_nan: ¬(nan_arg: \is_NaN(x));
assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
@@ -3782,8 +3782,8 @@ extern long double sinl(long double x);
*/
extern double tan(double x);
-/*@ requires ¬(infinite_arg: \is_infinite(x));
- requires ¬(nan_arg: \is_NaN(x));
+/*@ requires not_infinity: ¬(infinite_arg: \is_infinite(x));
+ requires not_nan: ¬(nan_arg: \is_NaN(x));
assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
diff --git a/tests/libc/oracle/math_h.1.res.oracle b/tests/libc/oracle/math_h.1.res.oracle
index 39d3fa1f6cc..a2d2aea1a03 100644
--- a/tests/libc/oracle/math_h.1.res.oracle
+++ b/tests/libc/oracle/math_h.1.res.oracle
@@ -161,275 +161,308 @@
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
[eva] using specification for function fabs
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva:alarm] tests/libc/math_h.c:87: Warning:
NaN double value. assert ¬\is_NaN(top);
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
[eva] using specification for function fabsf
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva:alarm] tests/libc/math_h.c:87: Warning:
NaN float value. assert ¬\is_NaN(f_top);
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
[eva] using specification for function fabsl
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva:alarm] tests/libc/math_h.c:87: Warning:
NaN long double value. assert ¬\is_NaN(ld_top);
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
[eva] Done for function fabs
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:87.
-[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
[eva] Done for function fabsl
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] using specification for function tan
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva:alarm] tests/libc/math_h.c:88: Warning:
NaN double value. assert ¬\is_NaN(top);
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva:alarm] tests/libc/math_h.c:88: Warning:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status unknown.
+ function tan: precondition 'not_infinity' got status unknown.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] using specification for function tanf
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva:alarm] tests/libc/math_h.c:88: Warning:
NaN float value. assert ¬\is_NaN(f_top);
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva:alarm] tests/libc/math_h.c:88: Warning:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status unknown.
+ function tanf: precondition 'not_infinity' got status unknown.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanl <- main.
Called from tests/libc/math_h.c:88.
@@ -464,30 +497,30 @@
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva:alarm] tests/libc/math_h.c:88: Warning:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status invalid.
+ function tan: precondition 'not_infinity' got status invalid.
[eva] tests/libc/math_h.c:88:
- function tan: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: no state left, precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva:alarm] tests/libc/math_h.c:88: Warning:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status invalid.
+ function tan: precondition 'not_infinity' got status invalid.
[eva] tests/libc/math_h.c:88:
- function tan: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: no state left, precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva:alarm] tests/libc/math_h.c:88: Warning:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status invalid.
+ function tanf: precondition 'not_infinity' got status invalid.
[eva] tests/libc/math_h.c:88:
- function tanf: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: no state left, precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva:alarm] tests/libc/math_h.c:88: Warning:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status invalid.
+ function tanf: precondition 'not_infinity' got status invalid.
[eva] tests/libc/math_h.c:88:
- function tanf: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: no state left, precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanl <- main.
Called from tests/libc/math_h.c:88.
@@ -501,14 +534,14 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -518,7 +551,7 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -528,7 +561,7 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -538,7 +571,7 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -548,7 +581,7 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -558,7 +591,7 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -568,7 +601,7 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -580,7 +613,7 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -591,56 +624,56 @@
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva:alarm] tests/libc/math_h.c:91: Warning:
NaN float value. assert ¬\is_NaN(f_top);
@@ -649,7 +682,7 @@
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
@@ -657,56 +690,56 @@
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva:alarm] tests/libc/math_h.c:92: Warning:
NaN long double value. assert ¬\is_NaN(ld_top);
@@ -715,313 +748,385 @@
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:93.
[eva] using specification for function ldexp
-[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:93.
-[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:93.
-[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:93.
-[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:93.
-[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:93.
-[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:93.
-[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:93.
-[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva:alarm] tests/libc/math_h.c:93: Warning:
NaN double value. assert ¬\is_NaN(top);
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:93.
-[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:94.
[eva] using specification for function ldexpf
-[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:94.
-[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:94.
-[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:94.
-[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:94.
-[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:94.
-[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:94.
-[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:94.
-[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva:alarm] tests/libc/math_h.c:94: Warning:
NaN float value. assert ¬\is_NaN(f_top);
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:94.
-[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:96.
-[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:96.
-[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:96.
-[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:96.
-[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:96.
-[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:96.
-[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:96.
-[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:96.
-[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva:alarm] tests/libc/math_h.c:96: Warning:
NaN double value. assert ¬\is_NaN(top);
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:96.
-[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:97.
-[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:97.
-[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:97.
-[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:97.
-[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:97.
-[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:97.
-[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:97.
-[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:97.
-[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva:alarm] tests/libc/math_h.c:97: Warning:
NaN float value. assert ¬\is_NaN(f_top);
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:97.
-[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:99.
-[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:99.
-[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:99.
-[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:99.
-[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:99.
-[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:99.
-[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:99.
-[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:99.
-[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva:alarm] tests/libc/math_h.c:99: Warning:
NaN double value. assert ¬\is_NaN(top);
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:99.
-[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:100.
-[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:100.
-[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:100.
-[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:100.
-[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:100.
-[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:100.
-[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:100.
-[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:100.
-[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva:alarm] tests/libc/math_h.c:100: Warning:
NaN float value. assert ¬\is_NaN(f_top);
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:100.
-[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:102.
-[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:102.
-[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:102.
-[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:102.
-[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:102.
-[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:102.
-[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:102.
-[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:102.
-[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva:alarm] tests/libc/math_h.c:102: Warning:
NaN double value. assert ¬\is_NaN(top);
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:102.
-[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
[eva] Done for function ldexp
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:103.
-[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:103.
-[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:103.
-[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:103.
-[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:103.
-[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:103.
-[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:103.
-[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:103.
-[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva:alarm] tests/libc/math_h.c:103: Warning:
NaN float value. assert ¬\is_NaN(f_top);
[eva] computing for function ldexpf <- main.
Called from tests/libc/math_h.c:103.
-[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
[eva] Done for function ldexpf
[eva] computing for function __finite <- main.
Called from tests/libc/math_h.c:108.
diff --git a/tests/libc/oracle/math_h.2.res.oracle b/tests/libc/oracle/math_h.2.res.oracle
index 886f7eb4b11..2caf779ac2d 100644
--- a/tests/libc/oracle/math_h.2.res.oracle
+++ b/tests/libc/oracle/math_h.2.res.oracle
@@ -277,133 +277,133 @@
Called from tests/libc/math_h.c:88.
[eva] using specification for function tan
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva:alarm] tests/libc/math_h.c:88: Warning:
non-finite double value. assert \is_finite(top);
[eva] computing for function tan <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tan: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tan: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tan: precondition 'not_nan' got status valid.
[eva] Done for function tan
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] using specification for function tanf
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva:alarm] tests/libc/math_h.c:88: Warning:
non-finite float value. assert \is_finite(f_top);
[eva] computing for function tanf <- main.
Called from tests/libc/math_h.c:88.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+ function tanf: precondition 'not_infinity' got status valid.
[eva] tests/libc/math_h.c:88:
- function tanf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function tanf: precondition 'not_nan' got status valid.
[eva] Done for function tanf
[eva] computing for function tanl <- main.
Called from tests/libc/math_h.c:88.
@@ -441,22 +441,18 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexp: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexp: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -466,11 +462,9 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexp: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -480,11 +474,9 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexp: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -494,11 +486,9 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexp: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -508,11 +498,9 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexp: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -522,11 +510,9 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexp: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -536,11 +522,9 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexp: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -552,11 +536,9 @@
[eva] tests/libc/math_h.c:90:
function frexp: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexp: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:90:
- function frexp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexp: precondition 'not_nan' got status valid.
[eva] Done for function frexp
[eva] computing for function frexp <- main.
Called from tests/libc/math_h.c:90.
@@ -567,88 +549,72 @@
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpf: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpf: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpf: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpf: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpf: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpf: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpf: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpf <- main.
Called from tests/libc/math_h.c:91.
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpf: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva:alarm] tests/libc/math_h.c:91: Warning:
non-finite float value. assert \is_finite(f_top);
@@ -657,11 +623,9 @@
[eva] tests/libc/math_h.c:91:
function frexpf: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpf: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:91:
- function frexpf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpf: precondition 'not_nan' got status valid.
[eva] Done for function frexpf
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
@@ -669,88 +633,72 @@
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpl: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpl: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpl: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpl: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpl: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpl: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpl: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function frexpl <- main.
Called from tests/libc/math_h.c:92.
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status valid.
+ function frexpl: precondition 'not_infinite' got status valid.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva:alarm] tests/libc/math_h.c:92: Warning:
non-finite long double value. assert \is_finite(ld_top);
@@ -759,11 +707,9 @@
[eva] tests/libc/math_h.c:92:
function frexpl: precondition 'valid_exp' got status valid.
[eva:alarm] tests/libc/math_h.c:92: Warning:
- function frexpl: precondition ¬(infinite_arg:
- \is_plus_infinity(x) ∨
- \is_minus_infinity(x)) got status unknown.
+ function frexpl: precondition 'not_infinite' got status unknown.
[eva] tests/libc/math_h.c:92:
- function frexpl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function frexpl: precondition 'not_nan' got status valid.
[eva] Done for function frexpl
[eva] computing for function ldexp <- main.
Called from tests/libc/math_h.c:93.
--
GitLab