Skip to content
Snippets Groups Projects
Commit 4567784f authored by David Bühler's avatar David Bühler Committed by Loïc Correnson
Browse files

[libc] math.h: adds behaviors for NaN and infinite cases in fmod specifications.

parent 6c372eec
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
− 4
View file @ 4567784f
...@@ -1035,17 +1035,41 @@ extern float truncf(float x); ...@@ -1035,17 +1035,41 @@ extern float truncf(float x);
*/ */
extern long double truncl(long double x); extern long double truncl(long double x);
/*@ requires finite_args: \is_finite(x) && \is_finite(y); /*@
requires finite_logic_result: \is_finite(fmod(x, y)); assigns errno, \result \from x, y;
behavior normal:
assumes in_domain: !\is_NaN(x) && !\is_NaN(y) && y != 0.;
assigns \result \from x, y; assigns \result \from x, y;
ensures finite_result: \is_finite(\result); ensures finite_result: \is_finite(\result);
behavior domain_error:
assumes out_of_domain: \is_infinite(x) || y == 0.;
ensures nan_result: \is_NaN(\result);
ensures errno_set: errno == EDOM;
behavior nan:
assumes nan_args: \is_NaN(x) || \is_NaN(y);
assigns \result \from x, y;
ensures nan_result: \is_NaN(\result);
complete behaviors;
disjoint behaviors;
*/ */
extern double fmod(double x, double y); extern double fmod(double x, double y);
/*@ requires finite_args: \is_finite(x) && \is_finite(y); /*@
requires finite_logic_result: \is_finite(fmodf(x, y)); assigns errno, \result \from x, y;
behavior normal:
assumes in_domain: !\is_NaN(x) && !\is_NaN(y) && y != 0.;
assigns \result \from x, y; assigns \result \from x, y;
ensures finite_result: \is_finite(\result); ensures finite_result: \is_finite(\result);
behavior domain_error:
assumes out_of_domain: \is_infinite(x) || y == 0.;
ensures nan_result: \is_NaN(\result);
ensures errno_set: errno == EDOM;
behavior nan:
assumes nan_args: \is_NaN(x) || \is_NaN(y);
assigns \result \from x, y;
ensures nan_result: \is_NaN(\result);
complete behaviors;
disjoint behaviors;
*/ */
extern float fmodf(float x, float y); extern float fmodf(float x, float y);
......
tests/float/oracle/math_builtins.res.oracle
+ 36
− 108
View file @ 4567784f
...@@ -863,45 +863,31 @@ ...@@ -863,45 +863,31 @@
[eva] tests/float/math_builtins.c:405: [eva] tests/float/math_builtins.c:405:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:405: [eva] tests/float/math_builtins.c:405:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:405:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:406: [eva] tests/float/math_builtins.c:406:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:406: [eva] tests/float/math_builtins.c:406:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:406:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:407: [eva] tests/float/math_builtins.c:407:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:407: [eva] tests/float/math_builtins.c:407:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:407:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:408: [eva] tests/float/math_builtins.c:408:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:408: [eva] tests/float/math_builtins.c:408:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:408:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:409: [eva] tests/float/math_builtins.c:409:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:409: [eva] tests/float/math_builtins.c:409:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:409:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:410: [eva] tests/float/math_builtins.c:410:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:410: [eva] tests/float/math_builtins.c:410:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:410:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:411: [eva] tests/float/math_builtins.c:411:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:411:
function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:411: Warning: [eva:alarm] tests/float/math_builtins.c:411: Warning:
function fmod: precondition 'finite_logic_result' got status invalid. function fmod: precondition 'in_domain' got status invalid.
[eva] Recording results for test_fmod_det [eva] Recording results for test_fmod_det
[eva] Done for function test_fmod_det [eva] Done for function test_fmod_det
[eva] computing for function test_fmod <- main. [eva] computing for function test_fmod <- main.
...@@ -913,27 +899,19 @@ ...@@ -913,27 +899,19 @@
[eva] tests/float/math_builtins.c:417: [eva] tests/float/math_builtins.c:417:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:417: [eva] tests/float/math_builtins.c:417:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:417:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:418: [eva] tests/float/math_builtins.c:418:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:418: [eva] tests/float/math_builtins.c:418:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:418:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:419: [eva] tests/float/math_builtins.c:419:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:419: [eva] tests/float/math_builtins.c:419:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:419:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:420: [eva] tests/float/math_builtins.c:420:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:420: [eva] tests/float/math_builtins.c:420:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:420:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:421. Called from tests/float/math_builtins.c:421.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -941,15 +919,11 @@ ...@@ -941,15 +919,11 @@
[eva] tests/float/math_builtins.c:422: [eva] tests/float/math_builtins.c:422:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:422: [eva] tests/float/math_builtins.c:422:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:422:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:423: [eva] tests/float/math_builtins.c:423:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:423: [eva] tests/float/math_builtins.c:423:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:423:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:424. Called from tests/float/math_builtins.c:424.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -961,9 +935,7 @@ ...@@ -961,9 +935,7 @@
[eva] tests/float/math_builtins.c:426: [eva] tests/float/math_builtins.c:426:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:426: [eva] tests/float/math_builtins.c:426:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:426:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:427. Called from tests/float/math_builtins.c:427.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -975,15 +947,11 @@ ...@@ -975,15 +947,11 @@
[eva] tests/float/math_builtins.c:429: [eva] tests/float/math_builtins.c:429:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:429: [eva] tests/float/math_builtins.c:429:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:429:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] tests/float/math_builtins.c:430: [eva] tests/float/math_builtins.c:430:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:430: [eva] tests/float/math_builtins.c:430:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:430:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:431. Called from tests/float/math_builtins.c:431.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -994,10 +962,8 @@ ...@@ -994,10 +962,8 @@
[eva] Done for function double_interval [eva] Done for function double_interval
[eva] tests/float/math_builtins.c:433: [eva] tests/float/math_builtins.c:433:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:433:
function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:433: Warning: [eva:alarm] tests/float/math_builtins.c:433: Warning:
function fmod: precondition 'finite_logic_result' got status unknown. function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:434. Called from tests/float/math_builtins.c:434.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1008,40 +974,32 @@ ...@@ -1008,40 +974,32 @@
[eva] Done for function double_interval [eva] Done for function double_interval
[eva] tests/float/math_builtins.c:436: [eva] tests/float/math_builtins.c:436:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:436:
function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:436: Warning: [eva:alarm] tests/float/math_builtins.c:436: Warning:
function fmod: precondition 'finite_logic_result' got status unknown. function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:437. Called from tests/float/math_builtins.c:437.
[eva] Recording results for double_interval [eva] Recording results for double_interval
[eva] Done for function double_interval [eva] Done for function double_interval
[eva] tests/float/math_builtins.c:438: [eva] tests/float/math_builtins.c:438:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:438:
function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:438: Warning: [eva:alarm] tests/float/math_builtins.c:438: Warning:
function fmod: precondition 'finite_logic_result' got status invalid. function fmod: precondition 'in_domain' got status invalid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:439. Called from tests/float/math_builtins.c:439.
[eva] Recording results for double_interval [eva] Recording results for double_interval
[eva] Done for function double_interval [eva] Done for function double_interval
[eva] tests/float/math_builtins.c:440: [eva] tests/float/math_builtins.c:440:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:440:
function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:440: Warning: [eva:alarm] tests/float/math_builtins.c:440: Warning:
function fmod: precondition 'finite_logic_result' got status unknown. function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:441. Called from tests/float/math_builtins.c:441.
[eva] Recording results for double_interval [eva] Recording results for double_interval
[eva] Done for function double_interval [eva] Done for function double_interval
[eva] tests/float/math_builtins.c:442: [eva] tests/float/math_builtins.c:442:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:442:
function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:442: Warning: [eva:alarm] tests/float/math_builtins.c:442: Warning:
function fmod: precondition 'finite_logic_result' got status unknown. function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:443. Called from tests/float/math_builtins.c:443.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1049,9 +1007,7 @@ ...@@ -1049,9 +1007,7 @@
[eva] tests/float/math_builtins.c:444: [eva] tests/float/math_builtins.c:444:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:444: [eva] tests/float/math_builtins.c:444:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:444:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:445. Called from tests/float/math_builtins.c:445.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1059,9 +1015,7 @@ ...@@ -1059,9 +1015,7 @@
[eva] tests/float/math_builtins.c:446: [eva] tests/float/math_builtins.c:446:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:446: [eva] tests/float/math_builtins.c:446:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:446:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:447. Called from tests/float/math_builtins.c:447.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1069,9 +1023,7 @@ ...@@ -1069,9 +1023,7 @@
[eva] tests/float/math_builtins.c:448: [eva] tests/float/math_builtins.c:448:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:448: [eva] tests/float/math_builtins.c:448:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:448:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:449. Called from tests/float/math_builtins.c:449.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1079,9 +1031,7 @@ ...@@ -1079,9 +1031,7 @@
[eva] tests/float/math_builtins.c:450: [eva] tests/float/math_builtins.c:450:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:450: [eva] tests/float/math_builtins.c:450:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:450:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:451. Called from tests/float/math_builtins.c:451.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1089,9 +1039,7 @@ ...@@ -1089,9 +1039,7 @@
[eva] tests/float/math_builtins.c:452: [eva] tests/float/math_builtins.c:452:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:452: [eva] tests/float/math_builtins.c:452:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:452:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:453. Called from tests/float/math_builtins.c:453.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1099,9 +1047,7 @@ ...@@ -1099,9 +1047,7 @@
[eva] tests/float/math_builtins.c:454: [eva] tests/float/math_builtins.c:454:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:454: [eva] tests/float/math_builtins.c:454:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:454:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:455. Called from tests/float/math_builtins.c:455.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1109,9 +1055,7 @@ ...@@ -1109,9 +1055,7 @@
[eva] tests/float/math_builtins.c:456: [eva] tests/float/math_builtins.c:456:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:456: [eva] tests/float/math_builtins.c:456:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:456:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:457. Called from tests/float/math_builtins.c:457.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1119,9 +1063,7 @@ ...@@ -1119,9 +1063,7 @@
[eva] tests/float/math_builtins.c:458: [eva] tests/float/math_builtins.c:458:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:458: [eva] tests/float/math_builtins.c:458:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:458:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:459. Called from tests/float/math_builtins.c:459.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1133,9 +1075,7 @@ ...@@ -1133,9 +1075,7 @@
[eva] tests/float/math_builtins.c:461: [eva] tests/float/math_builtins.c:461:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:461: [eva] tests/float/math_builtins.c:461:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:461:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:462. Called from tests/float/math_builtins.c:462.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1143,9 +1083,7 @@ ...@@ -1143,9 +1083,7 @@
[eva] tests/float/math_builtins.c:463: [eva] tests/float/math_builtins.c:463:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:463: [eva] tests/float/math_builtins.c:463:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:463:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:464. Called from tests/float/math_builtins.c:464.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1153,9 +1091,7 @@ ...@@ -1153,9 +1091,7 @@
[eva] tests/float/math_builtins.c:465: [eva] tests/float/math_builtins.c:465:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:465: [eva] tests/float/math_builtins.c:465:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:465:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:466. Called from tests/float/math_builtins.c:466.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1163,9 +1099,7 @@ ...@@ -1163,9 +1099,7 @@
[eva] tests/float/math_builtins.c:467: [eva] tests/float/math_builtins.c:467:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:467: [eva] tests/float/math_builtins.c:467:
function fmod: precondition 'finite_args' got status valid. function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:467:
function fmod: precondition 'finite_logic_result' got status valid.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:468. Called from tests/float/math_builtins.c:468.
[eva] Recording results for double_interval [eva] Recording results for double_interval
...@@ -1176,30 +1110,24 @@ ...@@ -1176,30 +1110,24 @@
[eva] Done for function double_interval [eva] Done for function double_interval
[eva] tests/float/math_builtins.c:470: [eva] tests/float/math_builtins.c:470:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:470:
function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:470: Warning: [eva:alarm] tests/float/math_builtins.c:470: Warning:
function fmod: precondition 'finite_logic_result' got status unknown. function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:471. Called from tests/float/math_builtins.c:471.
[eva] Recording results for double_interval [eva] Recording results for double_interval
[eva] Done for function double_interval [eva] Done for function double_interval
[eva] tests/float/math_builtins.c:472: [eva] tests/float/math_builtins.c:472:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:472:
function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:472: Warning: [eva:alarm] tests/float/math_builtins.c:472: Warning:
function fmod: precondition 'finite_logic_result' got status unknown. function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main. [eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:473. Called from tests/float/math_builtins.c:473.
[eva] Recording results for double_interval [eva] Recording results for double_interval
[eva] Done for function double_interval [eva] Done for function double_interval
[eva] tests/float/math_builtins.c:474: [eva] tests/float/math_builtins.c:474:
Call to builtin Frama_C_fmod for function fmod Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:474:
function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:474: Warning: [eva:alarm] tests/float/math_builtins.c:474: Warning:
function fmod: precondition 'finite_logic_result' got status unknown. function fmod: precondition 'in_domain' got status unknown.
[eva] Recording results for test_fmod [eva] Recording results for test_fmod
[eva] Done for function test_fmod [eva] Done for function test_fmod
[eva] computing for function test_sqrt_det <- main. [eva] computing for function test_sqrt_det <- main.
......
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