From 814db2c2b723a5fce7bbe9937ada33944c8252ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 19 May 2020 20:15:02 +0200
Subject: [PATCH] [Eva] Adds tests of builtins acos, asin and atan in
 math_builtins.

---
 tests/float/math_builtins.c                 |   73 +
 tests/float/oracle/math_builtins.res.oracle | 2219 +++++++++++--------
 2 files changed, 1328 insertions(+), 964 deletions(-)

diff --git a/tests/float/math_builtins.c b/tests/float/math_builtins.c
index db8f6293442..3ed738df405 100644
--- a/tests/float/math_builtins.c
+++ b/tests/float/math_builtins.c
@@ -6,6 +6,8 @@
 #include <math.h>
 
 static volatile int nondet;
+static volatile double any_double;
+static volatile float any_float;
 #define assert_bottom(exp) if (nondet) { exp; Frama_C_show_each_unreachable(); }
 
 double double_interval(double min, double max) {
@@ -25,6 +27,74 @@ void test_sin_det() {
   double z = sin(-1.);
 }
 
+void test_acos () {
+  double half_pi = acos(0.);
+  double pi = acos(-1.);
+  double zero = acos(1.);
+  double acos_image = acos(any_double);
+  if (nondet) {
+    double bottom = acos(-1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  if (nondet) {
+    double bottom = acos(1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  double x = acos(0.5);
+  double y = acos(-0.5);
+  double xy = double_interval(-0.5, 0.5);
+  xy = acos(xy);
+  /* Test acosf. */
+  float f32_half_pi = acosf(0.f);
+  float f32_pi = acosf(-1.f);
+  float f32_zero = acosf(1.f);
+  float f32_acosf_image = acosf(any_float);
+  if (nondet) {
+    float bottom = acosf(2.f);
+    Frama_C_show_each_bottom(bottom);
+  }
+}
+
+void test_asin () {
+  double zero = asin(0.);
+  double minus_half_pi = asin(-1.);
+  double half_pi = asin(1.);
+  double asin_image = asin(any_double);
+  if (nondet) {
+    double bottom = asin(-1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  if (nondet) {
+    double bottom = asin(1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  double x = asin(-0.5);
+  double y = asin(0.5);
+  double xy = double_interval(-0.5, 0.5);
+  xy = asin(xy);
+  /* Test asinf. */
+  float f32_zero = asinf(0.f);
+  float f32_minus_half_pi = asinf(-1.f);
+  float f32_half_pi = asinf(1.f);
+  float f32_asinf_image = asinf(any_float);
+  if (nondet) {
+    float bottom = asinf(2.f);
+    Frama_C_show_each_bottom(bottom);
+  }
+}
+
+void test_atan () {
+  double zero = atan(0.);
+  double atan_image = atan(any_double);
+  double x = atan(-2.);
+  double y = atan(2.);
+  double xy = double_interval(-2., 2.);
+  xy = atan(xy);
+  /* Test atanf. */
+  float f32_zero = atanf(0.f);
+  float f32_atanf_image = atanf(any_float);
+}
+
 void test_atan2_det() {
   double a = atan2(1.,0.);
   double b = atan2(0.,1.);
@@ -655,6 +725,9 @@ void test_roundf() {
 int main() {
   test_cos_det();
   test_sin_det();
+  test_acos();
+  test_asin();
+  test_atan();
   test_atan2_det();
   test_atan2();
   test_pow_det();
diff --git a/tests/float/oracle/math_builtins.res.oracle b/tests/float/oracle/math_builtins.res.oracle
index a53099f800a..c1889dd4b24 100644
--- a/tests/float/oracle/math_builtins.res.oracle
+++ b/tests/float/oracle/math_builtins.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/float/math_builtins.c (with preprocessing)
-[kernel:parser:decimal-float] tests/float/math_builtins.c:248: Warning: 
+[kernel:parser:decimal-float] tests/float/math_builtins.c:318: Warning: 
   Floating-point constant 5.8 is not represented exactly. Will use 0x1.7333333333333p2.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [eva] Analyzing a complete application starting at main
@@ -7,2292 +7,2423 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
+  any_double ∈ [--..--]
+  any_float ∈ [--..--]
 [eva] computing for function test_cos_det <- main.
-  Called from tests/float/math_builtins.c:656.
-[eva] tests/float/math_builtins.c:17: 
+  Called from tests/float/math_builtins.c:726.
+[eva] tests/float/math_builtins.c:19: 
   Call to builtin Frama_C_cos for function cos
-[eva] tests/float/math_builtins.c:17: 
+[eva] tests/float/math_builtins.c:19: 
   function cos: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:18: 
+[eva] tests/float/math_builtins.c:20: 
   Call to builtin Frama_C_cos for function cos
-[eva] tests/float/math_builtins.c:18: 
+[eva] tests/float/math_builtins.c:20: 
   function cos: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:19: 
+[eva] tests/float/math_builtins.c:21: 
   Call to builtin Frama_C_cos for function cos
-[eva] tests/float/math_builtins.c:19: 
+[eva] tests/float/math_builtins.c:21: 
   function cos: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_cos_det
 [eva] Done for function test_cos_det
 [eva] computing for function test_sin_det <- main.
-  Called from tests/float/math_builtins.c:657.
-[eva] tests/float/math_builtins.c:23: 
+  Called from tests/float/math_builtins.c:727.
+[eva] tests/float/math_builtins.c:25: 
   Call to builtin Frama_C_sin for function sin
-[eva] tests/float/math_builtins.c:23: 
+[eva] tests/float/math_builtins.c:25: 
   function sin: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:24: 
+[eva] tests/float/math_builtins.c:26: 
   Call to builtin Frama_C_sin for function sin
-[eva] tests/float/math_builtins.c:24: 
+[eva] tests/float/math_builtins.c:26: 
   function sin: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:25: 
+[eva] tests/float/math_builtins.c:27: 
   Call to builtin Frama_C_sin for function sin
-[eva] tests/float/math_builtins.c:25: 
+[eva] tests/float/math_builtins.c:27: 
   function sin: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_sin_det
 [eva] Done for function test_sin_det
+[eva] computing for function test_acos <- main.
+  Called from tests/float/math_builtins.c:728.
+[eva] tests/float/math_builtins.c:31: Call to builtin acos
+[eva] tests/float/math_builtins.c:31: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:32: Call to builtin acos
+[eva] tests/float/math_builtins.c:32: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:33: Call to builtin acos
+[eva] tests/float/math_builtins.c:33: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:34: Call to builtin acos
+[eva:alarm] tests/float/math_builtins.c:34: Warning: 
+  function acos: precondition 'in_domain' got status unknown.
+[eva] tests/float/math_builtins.c:36: Call to builtin acos
+[eva:alarm] tests/float/math_builtins.c:36: Warning: 
+  function acos: precondition 'in_domain' got status invalid.
+[eva] tests/float/math_builtins.c:40: Call to builtin acos
+[eva:alarm] tests/float/math_builtins.c:40: Warning: 
+  function acos: precondition 'in_domain' got status invalid.
+[eva] tests/float/math_builtins.c:43: Call to builtin acos
+[eva] tests/float/math_builtins.c:43: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:44: Call to builtin acos
+[eva] tests/float/math_builtins.c:44: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] computing for function double_interval <- test_acos <- main.
+  Called from tests/float/math_builtins.c:45.
+[eva] Recording results for double_interval
+[eva] Done for function double_interval
+[eva] tests/float/math_builtins.c:46: Call to builtin acos
+[eva] tests/float/math_builtins.c:46: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:48: Call to builtin acosf
+[eva] tests/float/math_builtins.c:48: 
+  function acosf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:49: Call to builtin acosf
+[eva] tests/float/math_builtins.c:49: 
+  function acosf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:50: Call to builtin acosf
+[eva] tests/float/math_builtins.c:50: 
+  function acosf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:51: Call to builtin acosf
+[eva:alarm] tests/float/math_builtins.c:51: Warning: 
+  function acosf: precondition 'in_domain' got status unknown.
+[eva] tests/float/math_builtins.c:53: Call to builtin acosf
+[eva:alarm] tests/float/math_builtins.c:53: Warning: 
+  function acosf: precondition 'in_domain' got status invalid.
+[eva] Recording results for test_acos
+[eva] Done for function test_acos
+[eva] computing for function test_asin <- main.
+  Called from tests/float/math_builtins.c:729.
+[eva] tests/float/math_builtins.c:59: Call to builtin asin
+[eva] tests/float/math_builtins.c:59: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:60: Call to builtin asin
+[eva] tests/float/math_builtins.c:60: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:61: Call to builtin asin
+[eva] tests/float/math_builtins.c:61: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:62: Call to builtin asin
+[eva:alarm] tests/float/math_builtins.c:62: Warning: 
+  function asin: precondition 'in_domain' got status unknown.
+[eva] tests/float/math_builtins.c:64: Call to builtin asin
+[eva:alarm] tests/float/math_builtins.c:64: Warning: 
+  function asin: precondition 'in_domain' got status invalid.
+[eva] tests/float/math_builtins.c:68: Call to builtin asin
+[eva:alarm] tests/float/math_builtins.c:68: Warning: 
+  function asin: precondition 'in_domain' got status invalid.
+[eva] tests/float/math_builtins.c:71: Call to builtin asin
+[eva] tests/float/math_builtins.c:71: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:72: Call to builtin asin
+[eva] tests/float/math_builtins.c:72: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] computing for function double_interval <- test_asin <- main.
+  Called from tests/float/math_builtins.c:73.
+[eva] Recording results for double_interval
+[eva] Done for function double_interval
+[eva] tests/float/math_builtins.c:74: Call to builtin asin
+[eva] tests/float/math_builtins.c:74: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:76: Call to builtin asinf
+[eva] tests/float/math_builtins.c:76: 
+  function asinf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:77: Call to builtin asinf
+[eva] tests/float/math_builtins.c:77: 
+  function asinf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:78: Call to builtin asinf
+[eva] tests/float/math_builtins.c:78: 
+  function asinf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:79: Call to builtin asinf
+[eva:alarm] tests/float/math_builtins.c:79: Warning: 
+  function asinf: precondition 'in_domain' got status unknown.
+[eva] tests/float/math_builtins.c:81: Call to builtin asinf
+[eva:alarm] tests/float/math_builtins.c:81: Warning: 
+  function asinf: precondition 'in_domain' got status invalid.
+[eva] Recording results for test_asin
+[eva] Done for function test_asin
+[eva] computing for function test_atan <- main.
+  Called from tests/float/math_builtins.c:730.
+[eva] tests/float/math_builtins.c:87: Call to builtin atan
+[eva] tests/float/math_builtins.c:87: 
+  function atan: precondition 'finite_arg' got status valid.
+[eva] tests/float/math_builtins.c:88: Call to builtin atan
+[eva:alarm] tests/float/math_builtins.c:88: Warning: 
+  function atan: precondition 'finite_arg' got status unknown.
+[eva] tests/float/math_builtins.c:89: Call to builtin atan
+[eva] tests/float/math_builtins.c:89: 
+  function atan: precondition 'finite_arg' got status valid.
+[eva] tests/float/math_builtins.c:90: Call to builtin atan
+[eva] tests/float/math_builtins.c:90: 
+  function atan: precondition 'finite_arg' got status valid.
+[eva] computing for function double_interval <- test_atan <- main.
+  Called from tests/float/math_builtins.c:91.
+[eva] Recording results for double_interval
+[eva] Done for function double_interval
+[eva] tests/float/math_builtins.c:92: Call to builtin atan
+[eva] tests/float/math_builtins.c:92: 
+  function atan: precondition 'finite_arg' got status valid.
+[eva] tests/float/math_builtins.c:94: Call to builtin atanf
+[eva] tests/float/math_builtins.c:94: 
+  function atanf: precondition 'finite_arg' got status valid.
+[eva] tests/float/math_builtins.c:95: Call to builtin atanf
+[eva:alarm] tests/float/math_builtins.c:95: Warning: 
+  function atanf: precondition 'finite_arg' got status unknown.
+[eva] Recording results for test_atan
+[eva] Done for function test_atan
 [eva] computing for function test_atan2_det <- main.
-  Called from tests/float/math_builtins.c:658.
-[eva] tests/float/math_builtins.c:29: 
+  Called from tests/float/math_builtins.c:731.
+[eva] tests/float/math_builtins.c:99: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:29: 
+[eva] tests/float/math_builtins.c:99: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:29: 
+[eva] tests/float/math_builtins.c:99: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:30: 
+[eva] tests/float/math_builtins.c:100: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:30: 
+[eva] tests/float/math_builtins.c:100: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:30: 
+[eva] tests/float/math_builtins.c:100: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:31: 
+[eva] tests/float/math_builtins.c:101: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:31: 
+[eva] tests/float/math_builtins.c:101: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:31: 
+[eva] tests/float/math_builtins.c:101: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:32: 
+[eva] tests/float/math_builtins.c:102: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:32: 
+[eva] tests/float/math_builtins.c:102: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:32: 
+[eva] tests/float/math_builtins.c:102: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:33: 
+[eva] tests/float/math_builtins.c:103: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:33: 
+[eva] tests/float/math_builtins.c:103: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:33: 
+[eva] tests/float/math_builtins.c:103: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:34: 
+[eva] tests/float/math_builtins.c:104: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:34: 
+[eva] tests/float/math_builtins.c:104: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:34: 
+[eva] tests/float/math_builtins.c:104: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:35: 
+[eva] tests/float/math_builtins.c:105: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:35: 
+[eva] tests/float/math_builtins.c:105: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:35: 
+[eva] tests/float/math_builtins.c:105: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:36: 
+[eva] tests/float/math_builtins.c:106: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:36: 
+[eva] tests/float/math_builtins.c:106: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:36: 
+[eva] tests/float/math_builtins.c:106: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:37: 
+[eva] tests/float/math_builtins.c:107: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:37: 
+[eva] tests/float/math_builtins.c:107: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:37: 
+[eva] tests/float/math_builtins.c:107: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:38: 
+[eva] tests/float/math_builtins.c:108: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:38: 
+[eva] tests/float/math_builtins.c:108: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:38: 
+[eva] tests/float/math_builtins.c:108: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:39: 
+[eva] tests/float/math_builtins.c:109: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:39: 
+[eva] tests/float/math_builtins.c:109: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:39: 
+[eva] tests/float/math_builtins.c:109: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:40: 
+[eva] tests/float/math_builtins.c:110: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:40: 
+[eva] tests/float/math_builtins.c:110: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:40: 
+[eva] tests/float/math_builtins.c:110: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:41: 
+[eva] tests/float/math_builtins.c:111: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:41: 
+[eva] tests/float/math_builtins.c:111: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:41: 
+[eva] tests/float/math_builtins.c:111: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] Recording results for test_atan2_det
 [eva] Done for function test_atan2_det
 [eva] computing for function test_atan2 <- main.
-  Called from tests/float/math_builtins.c:659.
+  Called from tests/float/math_builtins.c:732.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:46.
+  Called from tests/float/math_builtins.c:116.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:47.
+  Called from tests/float/math_builtins.c:117.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:48: 
+[eva] tests/float/math_builtins.c:118: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:48: 
+[eva] tests/float/math_builtins.c:118: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:48: 
+[eva] tests/float/math_builtins.c:118: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:49.
+  Called from tests/float/math_builtins.c:119.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:50: 
+[eva] tests/float/math_builtins.c:120: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:50: 
+[eva] tests/float/math_builtins.c:120: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:50: 
+[eva] tests/float/math_builtins.c:120: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:51.
+  Called from tests/float/math_builtins.c:121.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:52: 
+[eva] tests/float/math_builtins.c:122: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:52: 
+[eva] tests/float/math_builtins.c:122: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:52: 
+[eva] tests/float/math_builtins.c:122: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:53.
+  Called from tests/float/math_builtins.c:123.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:54: 
+[eva] tests/float/math_builtins.c:124: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:54: 
+[eva] tests/float/math_builtins.c:124: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:54: 
+[eva] tests/float/math_builtins.c:124: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:55.
+  Called from tests/float/math_builtins.c:125.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:56: 
+[eva] tests/float/math_builtins.c:126: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:56: 
+[eva] tests/float/math_builtins.c:126: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:56: 
+[eva] tests/float/math_builtins.c:126: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:57.
+  Called from tests/float/math_builtins.c:127.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:58.
+  Called from tests/float/math_builtins.c:128.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:59: 
+[eva] tests/float/math_builtins.c:129: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:59: 
+[eva] tests/float/math_builtins.c:129: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:59: 
+[eva] tests/float/math_builtins.c:129: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:60.
+  Called from tests/float/math_builtins.c:130.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:61: 
+[eva] tests/float/math_builtins.c:131: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:61: 
+[eva] tests/float/math_builtins.c:131: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:61: 
+[eva] tests/float/math_builtins.c:131: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:62.
+  Called from tests/float/math_builtins.c:132.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:63: 
+[eva] tests/float/math_builtins.c:133: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:63: 
+[eva] tests/float/math_builtins.c:133: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:63: 
+[eva] tests/float/math_builtins.c:133: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:64.
+  Called from tests/float/math_builtins.c:134.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:65: 
+[eva] tests/float/math_builtins.c:135: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:65: 
+[eva] tests/float/math_builtins.c:135: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:65: 
+[eva] tests/float/math_builtins.c:135: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:66.
+  Called from tests/float/math_builtins.c:136.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:67: 
+[eva] tests/float/math_builtins.c:137: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:67: 
+[eva] tests/float/math_builtins.c:137: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:67: 
+[eva] tests/float/math_builtins.c:137: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:68: 
+[eva] tests/float/math_builtins.c:138: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:68: 
+[eva] tests/float/math_builtins.c:138: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:68: 
+[eva] tests/float/math_builtins.c:138: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:69: 
+[eva] tests/float/math_builtins.c:139: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:69: 
+[eva] tests/float/math_builtins.c:139: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:69: 
+[eva] tests/float/math_builtins.c:139: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:70: 
+[eva] tests/float/math_builtins.c:140: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:70: 
+[eva] tests/float/math_builtins.c:140: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:70: 
+[eva] tests/float/math_builtins.c:140: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:71: 
+[eva] tests/float/math_builtins.c:141: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:71: 
+[eva] tests/float/math_builtins.c:141: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:71: 
+[eva] tests/float/math_builtins.c:141: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] Recording results for test_atan2
 [eva] Done for function test_atan2
 [eva] computing for function test_pow_det <- main.
-  Called from tests/float/math_builtins.c:660.
-[eva] tests/float/math_builtins.c:75: 
+  Called from tests/float/math_builtins.c:733.
+[eva] tests/float/math_builtins.c:145: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:75: 
+[eva] tests/float/math_builtins.c:145: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:75: 
+[eva] tests/float/math_builtins.c:145: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:76: 
+[eva] tests/float/math_builtins.c:146: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:76: 
+[eva] tests/float/math_builtins.c:146: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:76: 
+[eva] tests/float/math_builtins.c:146: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:77: 
+[eva] tests/float/math_builtins.c:147: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:77: 
+[eva] tests/float/math_builtins.c:147: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:77: 
+[eva] tests/float/math_builtins.c:147: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:78: 
+[eva] tests/float/math_builtins.c:148: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:78: 
+[eva] tests/float/math_builtins.c:148: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:78: 
+[eva] tests/float/math_builtins.c:148: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:79: 
+[eva] tests/float/math_builtins.c:149: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:79: 
+[eva] tests/float/math_builtins.c:149: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:79: 
+[eva] tests/float/math_builtins.c:149: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:80: 
+[eva] tests/float/math_builtins.c:150: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:80: 
+[eva] tests/float/math_builtins.c:150: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:80: 
+[eva] tests/float/math_builtins.c:150: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:81: 
+[eva] tests/float/math_builtins.c:151: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:81: 
+[eva] tests/float/math_builtins.c:151: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:81: 
+[eva] tests/float/math_builtins.c:151: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:82: 
+[eva] tests/float/math_builtins.c:152: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:82: 
+[eva] tests/float/math_builtins.c:152: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:82: 
+[eva] tests/float/math_builtins.c:152: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_pow_det
 [eva] Done for function test_pow_det
 [eva] computing for function test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:661.
+  Called from tests/float/math_builtins.c:734.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:98.
+  Called from tests/float/math_builtins.c:168.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:100: 
+[eva] tests/float/math_builtins.c:170: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:100: 
+[eva] tests/float/math_builtins.c:170: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:100: Warning: 
+[eva:alarm] tests/float/math_builtins.c:170: Warning: 
   function pow: precondition 'finite_logic_res' got status invalid.
-[eva] tests/float/math_builtins.c:102: 
+[eva] tests/float/math_builtins.c:172: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:102: 
+[eva] tests/float/math_builtins.c:172: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:102: Warning: 
+[eva:alarm] tests/float/math_builtins.c:172: Warning: 
   function pow: precondition 'finite_logic_res' got status invalid.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:105.
+  Called from tests/float/math_builtins.c:175.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:106: 
+[eva] tests/float/math_builtins.c:176: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:106: 
+[eva] tests/float/math_builtins.c:176: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:106: Warning: 
+[eva:alarm] tests/float/math_builtins.c:176: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:107: 
+[eva] tests/float/math_builtins.c:177: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:107: 
+[eva] tests/float/math_builtins.c:177: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:107: Warning: 
+[eva:alarm] tests/float/math_builtins.c:177: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:110: 
+[eva] tests/float/math_builtins.c:180: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:110: 
+[eva] tests/float/math_builtins.c:180: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:110: Warning: 
+[eva:alarm] tests/float/math_builtins.c:180: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:111: 
+[eva] tests/float/math_builtins.c:181: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:111: 
+[eva] tests/float/math_builtins.c:181: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:111: Warning: 
+[eva:alarm] tests/float/math_builtins.c:181: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:114.
+  Called from tests/float/math_builtins.c:184.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:115: 
+[eva] tests/float/math_builtins.c:185: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:115: 
+[eva] tests/float/math_builtins.c:185: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:115: Warning: 
+[eva:alarm] tests/float/math_builtins.c:185: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:116.
+  Called from tests/float/math_builtins.c:186.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:117: 
+[eva] tests/float/math_builtins.c:187: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:117: 
+[eva] tests/float/math_builtins.c:187: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:117: Warning: 
+[eva:alarm] tests/float/math_builtins.c:187: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:120.
+  Called from tests/float/math_builtins.c:190.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:121: 
+[eva] tests/float/math_builtins.c:191: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:121: 
+[eva] tests/float/math_builtins.c:191: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:121: 
+[eva] tests/float/math_builtins.c:191: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:122: 
+[eva] tests/float/math_builtins.c:192: 
   Frama_C_show_each_i: [0.0000000000000000 .. 1.0000000000000000*2^-1000]
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:123.
+  Called from tests/float/math_builtins.c:193.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:124: 
+[eva] tests/float/math_builtins.c:194: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:124: 
+[eva] tests/float/math_builtins.c:194: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:124: 
+[eva] tests/float/math_builtins.c:194: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:125: 
+[eva] tests/float/math_builtins.c:195: 
   Frama_C_show_each_j:
   [0.2500000000000000*2^-1022 .. 1.2707064924076672*2^-330]
-[eva] tests/float/math_builtins.c:129: 
+[eva] tests/float/math_builtins.c:199: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:129: 
+[eva] tests/float/math_builtins.c:199: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:129: 
+[eva] tests/float/math_builtins.c:199: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:130: 
+[eva] tests/float/math_builtins.c:200: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:130: 
+[eva] tests/float/math_builtins.c:200: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:130: 
+[eva] tests/float/math_builtins.c:200: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:132.
+  Called from tests/float/math_builtins.c:202.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:133: 
+[eva] tests/float/math_builtins.c:203: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:133: 
+[eva] tests/float/math_builtins.c:203: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:133: 
+[eva] tests/float/math_builtins.c:203: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:134: 
+[eva] tests/float/math_builtins.c:204: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:134: 
+[eva] tests/float/math_builtins.c:204: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:134: 
+[eva] tests/float/math_builtins.c:204: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:135: 
+[eva] tests/float/math_builtins.c:205: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:135: 
+[eva] tests/float/math_builtins.c:205: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:135: 
+[eva] tests/float/math_builtins.c:205: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:136: 
+[eva] tests/float/math_builtins.c:206: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:136: 
+[eva] tests/float/math_builtins.c:206: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:136: 
+[eva] tests/float/math_builtins.c:206: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:137: 
+[eva] tests/float/math_builtins.c:207: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:137: 
+[eva] tests/float/math_builtins.c:207: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:137: 
+[eva] tests/float/math_builtins.c:207: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:139.
+  Called from tests/float/math_builtins.c:209.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:140: 
+[eva] tests/float/math_builtins.c:210: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:140: 
+[eva] tests/float/math_builtins.c:210: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:140: 
+[eva] tests/float/math_builtins.c:210: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:141: 
+[eva] tests/float/math_builtins.c:211: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:141: 
+[eva] tests/float/math_builtins.c:211: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:141: 
+[eva] tests/float/math_builtins.c:211: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_pow_singleton_exp
 [eva] Done for function test_pow_singleton_exp
 [eva] computing for function test_pow <- main.
-  Called from tests/float/math_builtins.c:662.
+  Called from tests/float/math_builtins.c:735.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:147.
+  Called from tests/float/math_builtins.c:217.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:148: 
+[eva] tests/float/math_builtins.c:218: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:148: 
+[eva] tests/float/math_builtins.c:218: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:148: 
+[eva] tests/float/math_builtins.c:218: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:149.
+  Called from tests/float/math_builtins.c:219.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:150: 
+[eva] tests/float/math_builtins.c:220: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:150: 
+[eva] tests/float/math_builtins.c:220: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:150: 
+[eva] tests/float/math_builtins.c:220: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:151.
+  Called from tests/float/math_builtins.c:221.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:152: 
+[eva] tests/float/math_builtins.c:222: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:152: 
+[eva] tests/float/math_builtins.c:222: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:152: 
+[eva] tests/float/math_builtins.c:222: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:158.
+  Called from tests/float/math_builtins.c:228.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:159.
+  Called from tests/float/math_builtins.c:229.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:160: 
+[eva] tests/float/math_builtins.c:230: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:160: 
+[eva] tests/float/math_builtins.c:230: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:160: Warning: 
+[eva:alarm] tests/float/math_builtins.c:230: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:161.
+  Called from tests/float/math_builtins.c:231.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:162: 
+[eva] tests/float/math_builtins.c:232: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:162: 
+[eva] tests/float/math_builtins.c:232: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:162: Warning: 
+[eva:alarm] tests/float/math_builtins.c:232: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:163.
+  Called from tests/float/math_builtins.c:233.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:164: 
+[eva] tests/float/math_builtins.c:234: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:164: 
+[eva] tests/float/math_builtins.c:234: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:164: Warning: 
+[eva:alarm] tests/float/math_builtins.c:234: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:165.
+  Called from tests/float/math_builtins.c:235.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:166.
+  Called from tests/float/math_builtins.c:236.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:167: 
+[eva] tests/float/math_builtins.c:237: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:167: 
+[eva] tests/float/math_builtins.c:237: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:167: 
+[eva] tests/float/math_builtins.c:237: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:170.
+  Called from tests/float/math_builtins.c:240.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:171.
+  Called from tests/float/math_builtins.c:241.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:172: 
+[eva] tests/float/math_builtins.c:242: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:172: 
+[eva] tests/float/math_builtins.c:242: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:172: 
+[eva] tests/float/math_builtins.c:242: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:175.
+  Called from tests/float/math_builtins.c:245.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:176.
+  Called from tests/float/math_builtins.c:246.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:177: 
+[eva] tests/float/math_builtins.c:247: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:177: 
+[eva] tests/float/math_builtins.c:247: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:177: Warning: 
+[eva:alarm] tests/float/math_builtins.c:247: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:178.
+  Called from tests/float/math_builtins.c:248.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:179.
+  Called from tests/float/math_builtins.c:249.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:180: 
+[eva] tests/float/math_builtins.c:250: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:180: 
+[eva] tests/float/math_builtins.c:250: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:180: Warning: 
+[eva:alarm] tests/float/math_builtins.c:250: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:184.
+  Called from tests/float/math_builtins.c:254.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:185.
+  Called from tests/float/math_builtins.c:255.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:186: 
+[eva] tests/float/math_builtins.c:256: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:186: 
+[eva] tests/float/math_builtins.c:256: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:186: Warning: 
+[eva:alarm] tests/float/math_builtins.c:256: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:189.
+  Called from tests/float/math_builtins.c:259.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:190.
+  Called from tests/float/math_builtins.c:260.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:191: 
+[eva] tests/float/math_builtins.c:261: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:191: 
+[eva] tests/float/math_builtins.c:261: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:191: Warning: 
+[eva:alarm] tests/float/math_builtins.c:261: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:194.
+  Called from tests/float/math_builtins.c:264.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:195.
+  Called from tests/float/math_builtins.c:265.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:196: 
+[eva] tests/float/math_builtins.c:266: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:196: 
+[eva] tests/float/math_builtins.c:266: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:196: 
+[eva] tests/float/math_builtins.c:266: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:199.
+  Called from tests/float/math_builtins.c:269.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:200.
+  Called from tests/float/math_builtins.c:270.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:201: 
+[eva] tests/float/math_builtins.c:271: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:201: 
+[eva] tests/float/math_builtins.c:271: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:201: Warning: 
+[eva:alarm] tests/float/math_builtins.c:271: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:204.
+  Called from tests/float/math_builtins.c:274.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:205.
+  Called from tests/float/math_builtins.c:275.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:206: 
+[eva] tests/float/math_builtins.c:276: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:206: 
+[eva] tests/float/math_builtins.c:276: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:206: Warning: 
+[eva:alarm] tests/float/math_builtins.c:276: Warning: 
   function pow: precondition 'finite_logic_res' got status invalid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:207.
+  Called from tests/float/math_builtins.c:277.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:208: 
+[eva] tests/float/math_builtins.c:278: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:208: 
+[eva] tests/float/math_builtins.c:278: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:208: Warning: 
+[eva:alarm] tests/float/math_builtins.c:278: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:209.
+  Called from tests/float/math_builtins.c:279.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:210: 
+[eva] tests/float/math_builtins.c:280: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:210: 
+[eva] tests/float/math_builtins.c:280: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:210: Warning: 
+[eva:alarm] tests/float/math_builtins.c:280: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:211.
+  Called from tests/float/math_builtins.c:281.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:212: 
+[eva] tests/float/math_builtins.c:282: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:212: 
+[eva] tests/float/math_builtins.c:282: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:212: Warning: 
+[eva:alarm] tests/float/math_builtins.c:282: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:215.
+  Called from tests/float/math_builtins.c:285.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:216.
+  Called from tests/float/math_builtins.c:286.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:217: 
+[eva] tests/float/math_builtins.c:287: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:217: 
+[eva] tests/float/math_builtins.c:287: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:217: Warning: 
+[eva:alarm] tests/float/math_builtins.c:287: Warning: 
   function pow: precondition 'finite_logic_res' got status invalid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:220.
+  Called from tests/float/math_builtins.c:290.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:221.
+  Called from tests/float/math_builtins.c:291.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:222: 
+[eva] tests/float/math_builtins.c:292: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:222: 
+[eva] tests/float/math_builtins.c:292: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:222: Warning: 
+[eva:alarm] tests/float/math_builtins.c:292: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:222: Frama_C_show_each_unreachable:
+[eva] tests/float/math_builtins.c:292: Frama_C_show_each_unreachable:
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:224.
+  Called from tests/float/math_builtins.c:294.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:225: 
+[eva] tests/float/math_builtins.c:295: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:225: 
+[eva] tests/float/math_builtins.c:295: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:225: 
+[eva] tests/float/math_builtins.c:295: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_pow
 [eva] Done for function test_pow
 [eva] computing for function test_fmod_det <- main.
-  Called from tests/float/math_builtins.c:663.
-[eva] tests/float/math_builtins.c:335: 
+  Called from tests/float/math_builtins.c:736.
+[eva] tests/float/math_builtins.c:405: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:335: 
+[eva] tests/float/math_builtins.c:405: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:335: 
+[eva] tests/float/math_builtins.c:405: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:336: 
+[eva] tests/float/math_builtins.c:406: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:336: 
+[eva] tests/float/math_builtins.c:406: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:336: 
+[eva] tests/float/math_builtins.c:406: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:337: 
+[eva] tests/float/math_builtins.c:407: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:337: 
+[eva] tests/float/math_builtins.c:407: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:337: 
+[eva] tests/float/math_builtins.c:407: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:338: 
+[eva] tests/float/math_builtins.c:408: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:338: 
+[eva] tests/float/math_builtins.c:408: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:338: 
+[eva] tests/float/math_builtins.c:408: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:339: 
+[eva] tests/float/math_builtins.c:409: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:339: 
+[eva] tests/float/math_builtins.c:409: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:339: 
+[eva] tests/float/math_builtins.c:409: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:340: 
+[eva] tests/float/math_builtins.c:410: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:340: 
+[eva] tests/float/math_builtins.c:410: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:340: 
+[eva] tests/float/math_builtins.c:410: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:341: 
+[eva] tests/float/math_builtins.c:411: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:341: 
+[eva] tests/float/math_builtins.c:411: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:341: Warning: 
+[eva:alarm] tests/float/math_builtins.c:411: Warning: 
   function fmod: precondition 'finite_logic_result' got status invalid.
 [eva] Recording results for test_fmod_det
 [eva] Done for function test_fmod_det
 [eva] computing for function test_fmod <- main.
-  Called from tests/float/math_builtins.c:664.
+  Called from tests/float/math_builtins.c:737.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:346.
+  Called from tests/float/math_builtins.c:416.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:347: 
+[eva] tests/float/math_builtins.c:417: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:347: 
+[eva] tests/float/math_builtins.c:417: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:347: 
+[eva] tests/float/math_builtins.c:417: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:348: 
+[eva] tests/float/math_builtins.c:418: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:348: 
+[eva] tests/float/math_builtins.c:418: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:348: 
+[eva] tests/float/math_builtins.c:418: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:349: 
+[eva] tests/float/math_builtins.c:419: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:349: 
+[eva] tests/float/math_builtins.c:419: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:349: 
+[eva] tests/float/math_builtins.c:419: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:350: 
+[eva] tests/float/math_builtins.c:420: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:350: 
+[eva] tests/float/math_builtins.c:420: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:350: 
+[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.
-  Called from tests/float/math_builtins.c:351.
+  Called from tests/float/math_builtins.c:421.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:352: 
+[eva] tests/float/math_builtins.c:422: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:352: 
+[eva] tests/float/math_builtins.c:422: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:352: 
+[eva] tests/float/math_builtins.c:422: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:353: 
+[eva] tests/float/math_builtins.c:423: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:353: 
+[eva] tests/float/math_builtins.c:423: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:353: 
+[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.
-  Called from tests/float/math_builtins.c:354.
+  Called from tests/float/math_builtins.c:424.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:355.
+  Called from tests/float/math_builtins.c:425.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:356: 
+[eva] tests/float/math_builtins.c:426: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:356: 
+[eva] tests/float/math_builtins.c:426: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:356: 
+[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.
-  Called from tests/float/math_builtins.c:357.
+  Called from tests/float/math_builtins.c:427.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:358.
+  Called from tests/float/math_builtins.c:428.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:359: 
+[eva] tests/float/math_builtins.c:429: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:359: 
+[eva] tests/float/math_builtins.c:429: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:359: 
+[eva] tests/float/math_builtins.c:429: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:360: 
+[eva] tests/float/math_builtins.c:430: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:360: 
+[eva] tests/float/math_builtins.c:430: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:360: 
+[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.
-  Called from tests/float/math_builtins.c:361.
+  Called from tests/float/math_builtins.c:431.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:362.
+  Called from tests/float/math_builtins.c:432.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:363: 
+[eva] tests/float/math_builtins.c:433: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:363: 
+[eva] tests/float/math_builtins.c:433: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:363: Warning: 
+[eva:alarm] tests/float/math_builtins.c:433: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:364.
+  Called from tests/float/math_builtins.c:434.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:365.
+  Called from tests/float/math_builtins.c:435.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:366: 
+[eva] tests/float/math_builtins.c:436: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:366: 
+[eva] tests/float/math_builtins.c:436: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:366: Warning: 
+[eva:alarm] tests/float/math_builtins.c:436: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:367.
+  Called from tests/float/math_builtins.c:437.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:368: 
+[eva] tests/float/math_builtins.c:438: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:368: 
+[eva] tests/float/math_builtins.c:438: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:368: Warning: 
+[eva:alarm] tests/float/math_builtins.c:438: Warning: 
   function fmod: precondition 'finite_logic_result' got status invalid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:369.
+  Called from tests/float/math_builtins.c:439.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:370: 
+[eva] tests/float/math_builtins.c:440: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:370: 
+[eva] tests/float/math_builtins.c:440: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:370: Warning: 
+[eva:alarm] tests/float/math_builtins.c:440: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:371.
+  Called from tests/float/math_builtins.c:441.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:372: 
+[eva] tests/float/math_builtins.c:442: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:372: 
+[eva] tests/float/math_builtins.c:442: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:372: Warning: 
+[eva:alarm] tests/float/math_builtins.c:442: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:373.
+  Called from tests/float/math_builtins.c:443.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:374: 
+[eva] tests/float/math_builtins.c:444: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:374: 
+[eva] tests/float/math_builtins.c:444: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:374: 
+[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.
-  Called from tests/float/math_builtins.c:375.
+  Called from tests/float/math_builtins.c:445.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:376: 
+[eva] tests/float/math_builtins.c:446: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:376: 
+[eva] tests/float/math_builtins.c:446: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:376: 
+[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.
-  Called from tests/float/math_builtins.c:377.
+  Called from tests/float/math_builtins.c:447.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:378: 
+[eva] tests/float/math_builtins.c:448: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:378: 
+[eva] tests/float/math_builtins.c:448: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:378: 
+[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.
-  Called from tests/float/math_builtins.c:379.
+  Called from tests/float/math_builtins.c:449.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:380: 
+[eva] tests/float/math_builtins.c:450: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:380: 
+[eva] tests/float/math_builtins.c:450: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:380: 
+[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.
-  Called from tests/float/math_builtins.c:381.
+  Called from tests/float/math_builtins.c:451.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:382: 
+[eva] tests/float/math_builtins.c:452: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:382: 
+[eva] tests/float/math_builtins.c:452: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:382: 
+[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.
-  Called from tests/float/math_builtins.c:383.
+  Called from tests/float/math_builtins.c:453.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:384: 
+[eva] tests/float/math_builtins.c:454: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:384: 
+[eva] tests/float/math_builtins.c:454: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:384: 
+[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.
-  Called from tests/float/math_builtins.c:385.
+  Called from tests/float/math_builtins.c:455.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:386: 
+[eva] tests/float/math_builtins.c:456: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:386: 
+[eva] tests/float/math_builtins.c:456: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:386: 
+[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.
-  Called from tests/float/math_builtins.c:387.
+  Called from tests/float/math_builtins.c:457.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:388: 
+[eva] tests/float/math_builtins.c:458: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:388: 
+[eva] tests/float/math_builtins.c:458: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:388: 
+[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.
-  Called from tests/float/math_builtins.c:389.
+  Called from tests/float/math_builtins.c:459.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:390.
+  Called from tests/float/math_builtins.c:460.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:391: 
+[eva] tests/float/math_builtins.c:461: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:391: 
+[eva] tests/float/math_builtins.c:461: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:391: 
+[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.
-  Called from tests/float/math_builtins.c:392.
+  Called from tests/float/math_builtins.c:462.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:393: 
+[eva] tests/float/math_builtins.c:463: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:393: 
+[eva] tests/float/math_builtins.c:463: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:393: 
+[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.
-  Called from tests/float/math_builtins.c:394.
+  Called from tests/float/math_builtins.c:464.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:395: 
+[eva] tests/float/math_builtins.c:465: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:395: 
+[eva] tests/float/math_builtins.c:465: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:395: 
+[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.
-  Called from tests/float/math_builtins.c:396.
+  Called from tests/float/math_builtins.c:466.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:397: 
+[eva] tests/float/math_builtins.c:467: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:397: 
+[eva] tests/float/math_builtins.c:467: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:397: 
+[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.
-  Called from tests/float/math_builtins.c:398.
+  Called from tests/float/math_builtins.c:468.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:399.
+  Called from tests/float/math_builtins.c:469.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:400: 
+[eva] tests/float/math_builtins.c:470: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:400: 
+[eva] tests/float/math_builtins.c:470: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:400: Warning: 
+[eva:alarm] tests/float/math_builtins.c:470: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:401.
+  Called from tests/float/math_builtins.c:471.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:402: 
+[eva] tests/float/math_builtins.c:472: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:402: 
+[eva] tests/float/math_builtins.c:472: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:402: Warning: 
+[eva:alarm] tests/float/math_builtins.c:472: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:403.
+  Called from tests/float/math_builtins.c:473.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:404: 
+[eva] tests/float/math_builtins.c:474: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:404: 
+[eva] tests/float/math_builtins.c:474: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:404: Warning: 
+[eva:alarm] tests/float/math_builtins.c:474: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] Recording results for test_fmod
 [eva] Done for function test_fmod
 [eva] computing for function test_sqrt_det <- main.
-  Called from tests/float/math_builtins.c:665.
-[eva] tests/float/math_builtins.c:408: 
+  Called from tests/float/math_builtins.c:738.
+[eva] tests/float/math_builtins.c:478: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:408: 
+[eva] tests/float/math_builtins.c:478: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:408: 
+[eva] tests/float/math_builtins.c:478: 
   function sqrt: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:409: 
+[eva] tests/float/math_builtins.c:479: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:409: 
+[eva] tests/float/math_builtins.c:479: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:409: 
+[eva] tests/float/math_builtins.c:479: 
   function sqrt: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:410: 
+[eva] tests/float/math_builtins.c:480: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:410: 
+[eva] tests/float/math_builtins.c:480: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:410: Warning: 
+[eva:alarm] tests/float/math_builtins.c:480: Warning: 
   function sqrt: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:411: 
+[eva] tests/float/math_builtins.c:481: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:411: 
+[eva] tests/float/math_builtins.c:481: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:411: 
+[eva] tests/float/math_builtins.c:481: 
   function sqrt: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:412: 
+[eva] tests/float/math_builtins.c:482: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:412: 
+[eva] tests/float/math_builtins.c:482: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:412: 
+[eva] tests/float/math_builtins.c:482: 
   function sqrt: precondition 'arg_positive' got status valid.
 [eva] Recording results for test_sqrt_det
 [eva] Done for function test_sqrt_det
 [eva] computing for function test_sqrt <- main.
-  Called from tests/float/math_builtins.c:666.
+  Called from tests/float/math_builtins.c:739.
 [eva] computing for function double_interval <- test_sqrt <- main.
-  Called from tests/float/math_builtins.c:416.
+  Called from tests/float/math_builtins.c:486.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:417: 
+[eva] tests/float/math_builtins.c:487: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:417: 
+[eva] tests/float/math_builtins.c:487: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:417: 
+[eva] tests/float/math_builtins.c:487: 
   function sqrt: precondition 'arg_positive' got status valid.
 [eva] computing for function double_interval <- test_sqrt <- main.
-  Called from tests/float/math_builtins.c:418.
+  Called from tests/float/math_builtins.c:488.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:419: 
+[eva] tests/float/math_builtins.c:489: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:419: 
+[eva] tests/float/math_builtins.c:489: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:419: Warning: 
+[eva:alarm] tests/float/math_builtins.c:489: Warning: 
   function sqrt: precondition 'arg_positive' got status unknown.
 [eva] computing for function double_interval <- test_sqrt <- main.
-  Called from tests/float/math_builtins.c:420.
+  Called from tests/float/math_builtins.c:490.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:421: 
+[eva] tests/float/math_builtins.c:491: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:421: 
+[eva] tests/float/math_builtins.c:491: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:421: Warning: 
+[eva:alarm] tests/float/math_builtins.c:491: Warning: 
   function sqrt: precondition 'arg_positive' got status unknown.
 [eva] computing for function double_interval <- test_sqrt <- main.
-  Called from tests/float/math_builtins.c:422.
+  Called from tests/float/math_builtins.c:492.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:423: 
+[eva] tests/float/math_builtins.c:493: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:423: 
+[eva] tests/float/math_builtins.c:493: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:423: Warning: 
+[eva:alarm] tests/float/math_builtins.c:493: Warning: 
   function sqrt: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_sqrt
 [eva] Done for function test_sqrt
 [eva] computing for function test_exp_det <- main.
-  Called from tests/float/math_builtins.c:667.
-[eva] tests/float/math_builtins.c:446: 
+  Called from tests/float/math_builtins.c:740.
+[eva] tests/float/math_builtins.c:516: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:446: 
+[eva] tests/float/math_builtins.c:516: 
   function exp: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:446: 
+[eva] tests/float/math_builtins.c:516: 
   function exp: precondition 'finite_domain' got status valid.
-[eva] tests/float/math_builtins.c:447: 
+[eva] tests/float/math_builtins.c:517: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:447: 
+[eva] tests/float/math_builtins.c:517: 
   function exp: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:447: 
+[eva] tests/float/math_builtins.c:517: 
   function exp: precondition 'finite_domain' got status valid.
-[eva] tests/float/math_builtins.c:448: 
+[eva] tests/float/math_builtins.c:518: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:448: 
+[eva] tests/float/math_builtins.c:518: 
   function exp: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:448: 
+[eva] tests/float/math_builtins.c:518: 
   function exp: precondition 'finite_domain' got status valid.
-[eva] tests/float/math_builtins.c:449: 
+[eva] tests/float/math_builtins.c:519: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:449: 
+[eva] tests/float/math_builtins.c:519: 
   function exp: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:449: 
+[eva] tests/float/math_builtins.c:519: 
   function exp: precondition 'finite_domain' got status valid.
-[eva] tests/float/math_builtins.c:450: 
+[eva] tests/float/math_builtins.c:520: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:450: 
+[eva] tests/float/math_builtins.c:520: 
   function exp: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:450: 
+[eva] tests/float/math_builtins.c:520: 
   function exp: precondition 'finite_domain' got status valid.
-[eva] tests/float/math_builtins.c:451: 
+[eva] tests/float/math_builtins.c:521: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:451: 
+[eva] tests/float/math_builtins.c:521: 
   function exp: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:451: Warning: 
+[eva:alarm] tests/float/math_builtins.c:521: Warning: 
   function exp: precondition 'finite_domain' got status invalid.
 [eva] Recording results for test_exp_det
 [eva] Done for function test_exp_det
 [eva] computing for function test_log_det <- main.
-  Called from tests/float/math_builtins.c:668.
-[eva] tests/float/math_builtins.c:463: 
+  Called from tests/float/math_builtins.c:741.
+[eva] tests/float/math_builtins.c:533: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:463: 
+[eva] tests/float/math_builtins.c:533: 
   function log: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:463: 
+[eva] tests/float/math_builtins.c:533: 
   function log: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:464: 
+[eva] tests/float/math_builtins.c:534: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:464: 
+[eva] tests/float/math_builtins.c:534: 
   function log: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:464: 
+[eva] tests/float/math_builtins.c:534: 
   function log: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:465: 
+[eva] tests/float/math_builtins.c:535: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:465: 
+[eva] tests/float/math_builtins.c:535: 
   function log: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:465: Warning: 
+[eva:alarm] tests/float/math_builtins.c:535: Warning: 
   function log: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:466: 
+[eva] tests/float/math_builtins.c:536: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:466: 
+[eva] tests/float/math_builtins.c:536: 
   function log: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:466: Warning: 
+[eva:alarm] tests/float/math_builtins.c:536: Warning: 
   function log: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:467: 
+[eva] tests/float/math_builtins.c:537: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:467: 
+[eva] tests/float/math_builtins.c:537: 
   function log: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:467: Warning: 
+[eva:alarm] tests/float/math_builtins.c:537: Warning: 
   function log: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:468: 
+[eva] tests/float/math_builtins.c:538: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:468: 
+[eva] tests/float/math_builtins.c:538: 
   function log: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:468: Warning: 
+[eva:alarm] tests/float/math_builtins.c:538: Warning: 
   function log: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_log_det
 [eva] Done for function test_log_det
 [eva] computing for function test_log10_det <- main.
-  Called from tests/float/math_builtins.c:669.
-[eva] tests/float/math_builtins.c:481: 
+  Called from tests/float/math_builtins.c:742.
+[eva] tests/float/math_builtins.c:551: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:481: 
+[eva] tests/float/math_builtins.c:551: 
   function log10: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:481: 
+[eva] tests/float/math_builtins.c:551: 
   function log10: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:482: 
+[eva] tests/float/math_builtins.c:552: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:482: 
+[eva] tests/float/math_builtins.c:552: 
   function log10: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:482: 
+[eva] tests/float/math_builtins.c:552: 
   function log10: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:483: 
+[eva] tests/float/math_builtins.c:553: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:483: 
+[eva] tests/float/math_builtins.c:553: 
   function log10: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:483: Warning: 
+[eva:alarm] tests/float/math_builtins.c:553: Warning: 
   function log10: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:484: 
+[eva] tests/float/math_builtins.c:554: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:484: 
+[eva] tests/float/math_builtins.c:554: 
   function log10: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:484: Warning: 
+[eva:alarm] tests/float/math_builtins.c:554: Warning: 
   function log10: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:485: 
+[eva] tests/float/math_builtins.c:555: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:485: 
+[eva] tests/float/math_builtins.c:555: 
   function log10: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:485: Warning: 
+[eva:alarm] tests/float/math_builtins.c:555: Warning: 
   function log10: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:486: 
+[eva] tests/float/math_builtins.c:556: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:486: 
+[eva] tests/float/math_builtins.c:556: 
   function log10: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:486: Warning: 
+[eva:alarm] tests/float/math_builtins.c:556: Warning: 
   function log10: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_log10_det
 [eva] Done for function test_log10_det
 [eva] computing for function test_powf_det <- main.
-  Called from tests/float/math_builtins.c:671.
-[eva] tests/float/math_builtins.c:86: 
+  Called from tests/float/math_builtins.c:744.
+[eva] tests/float/math_builtins.c:156: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:86: 
+[eva] tests/float/math_builtins.c:156: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:86: 
+[eva] tests/float/math_builtins.c:156: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:87: 
+[eva] tests/float/math_builtins.c:157: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:87: 
+[eva] tests/float/math_builtins.c:157: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:87: 
+[eva] tests/float/math_builtins.c:157: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:88: 
+[eva] tests/float/math_builtins.c:158: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:88: 
+[eva] tests/float/math_builtins.c:158: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:88: 
+[eva] tests/float/math_builtins.c:158: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:89: 
+[eva] tests/float/math_builtins.c:159: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:89: 
+[eva] tests/float/math_builtins.c:159: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:89: 
+[eva] tests/float/math_builtins.c:159: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:90: 
+[eva] tests/float/math_builtins.c:160: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:90: 
+[eva] tests/float/math_builtins.c:160: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:90: 
+[eva] tests/float/math_builtins.c:160: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:91: 
+[eva] tests/float/math_builtins.c:161: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:91: 
+[eva] tests/float/math_builtins.c:161: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:91: 
+[eva] tests/float/math_builtins.c:161: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:92: 
+[eva] tests/float/math_builtins.c:162: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:92: 
+[eva] tests/float/math_builtins.c:162: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:92: 
+[eva] tests/float/math_builtins.c:162: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:93: 
+[eva] tests/float/math_builtins.c:163: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:93: 
+[eva] tests/float/math_builtins.c:163: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:93: 
+[eva] tests/float/math_builtins.c:163: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_powf_det
 [eva] Done for function test_powf_det
 [eva] computing for function test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:672.
+  Called from tests/float/math_builtins.c:745.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:231.
+  Called from tests/float/math_builtins.c:301.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:233: 
+[eva] tests/float/math_builtins.c:303: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:233: 
+[eva] tests/float/math_builtins.c:303: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:233: Warning: 
+[eva:alarm] tests/float/math_builtins.c:303: Warning: 
   function powf: precondition 'finite_logic_res' got status invalid.
-[eva] tests/float/math_builtins.c:235: 
+[eva] tests/float/math_builtins.c:305: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:235: 
+[eva] tests/float/math_builtins.c:305: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:235: Warning: 
+[eva:alarm] tests/float/math_builtins.c:305: Warning: 
   function powf: precondition 'finite_logic_res' got status invalid.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:238.
+  Called from tests/float/math_builtins.c:308.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:239: 
+[eva] tests/float/math_builtins.c:309: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:239: 
+[eva] tests/float/math_builtins.c:309: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:239: Warning: 
+[eva:alarm] tests/float/math_builtins.c:309: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:240: 
+[eva] tests/float/math_builtins.c:310: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:240: 
+[eva] tests/float/math_builtins.c:310: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:240: Warning: 
+[eva:alarm] tests/float/math_builtins.c:310: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:243: 
+[eva] tests/float/math_builtins.c:313: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:243: 
+[eva] tests/float/math_builtins.c:313: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:243: Warning: 
+[eva:alarm] tests/float/math_builtins.c:313: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:244: 
+[eva] tests/float/math_builtins.c:314: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:244: 
+[eva] tests/float/math_builtins.c:314: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:244: Warning: 
+[eva:alarm] tests/float/math_builtins.c:314: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:247.
+  Called from tests/float/math_builtins.c:317.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:248: 
+[eva] tests/float/math_builtins.c:318: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:248: 
+[eva] tests/float/math_builtins.c:318: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:248: 
+[eva] tests/float/math_builtins.c:318: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:249.
+  Called from tests/float/math_builtins.c:319.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:250: 
+[eva] tests/float/math_builtins.c:320: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:250: 
+[eva] tests/float/math_builtins.c:320: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:250: Warning: 
+[eva:alarm] tests/float/math_builtins.c:320: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:253.
+  Called from tests/float/math_builtins.c:323.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:254: 
+[eva] tests/float/math_builtins.c:324: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:254: 
+[eva] tests/float/math_builtins.c:324: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:254: 
+[eva] tests/float/math_builtins.c:324: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:255: 
+[eva] tests/float/math_builtins.c:325: 
   Frama_C_show_each_i: [0.0000000000000000 .. 1.0000000000000000*2^-120]
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:256.
+  Called from tests/float/math_builtins.c:326.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:257: 
+[eva] tests/float/math_builtins.c:327: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:257: 
+[eva] tests/float/math_builtins.c:327: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:257: 
+[eva] tests/float/math_builtins.c:327: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:258: Frama_C_show_each_j: {0}
-[eva] tests/float/math_builtins.c:262: 
+[eva] tests/float/math_builtins.c:328: Frama_C_show_each_j: {0}
+[eva] tests/float/math_builtins.c:332: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:262: 
+[eva] tests/float/math_builtins.c:332: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:262: 
+[eva] tests/float/math_builtins.c:332: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:263: 
+[eva] tests/float/math_builtins.c:333: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:263: 
+[eva] tests/float/math_builtins.c:333: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:263: 
+[eva] tests/float/math_builtins.c:333: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:265.
+  Called from tests/float/math_builtins.c:335.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:266: 
+[eva] tests/float/math_builtins.c:336: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:266: 
+[eva] tests/float/math_builtins.c:336: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:266: 
+[eva] tests/float/math_builtins.c:336: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:267: 
+[eva] tests/float/math_builtins.c:337: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:267: 
+[eva] tests/float/math_builtins.c:337: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:267: 
+[eva] tests/float/math_builtins.c:337: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:268: 
+[eva] tests/float/math_builtins.c:338: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:268: 
+[eva] tests/float/math_builtins.c:338: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:268: 
+[eva] tests/float/math_builtins.c:338: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:269: 
+[eva] tests/float/math_builtins.c:339: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:269: 
+[eva] tests/float/math_builtins.c:339: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:269: 
+[eva] tests/float/math_builtins.c:339: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:270: 
+[eva] tests/float/math_builtins.c:340: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:270: 
+[eva] tests/float/math_builtins.c:340: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:270: 
+[eva] tests/float/math_builtins.c:340: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:272.
+  Called from tests/float/math_builtins.c:342.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:273: 
+[eva] tests/float/math_builtins.c:343: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:273: 
+[eva] tests/float/math_builtins.c:343: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:273: 
+[eva] tests/float/math_builtins.c:343: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:274: 
+[eva] tests/float/math_builtins.c:344: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:274: 
+[eva] tests/float/math_builtins.c:344: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:274: 
+[eva] tests/float/math_builtins.c:344: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_powf_singleton_exp
 [eva] Done for function test_powf_singleton_exp
 [eva] computing for function test_powf <- main.
-  Called from tests/float/math_builtins.c:673.
+  Called from tests/float/math_builtins.c:746.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:280.
+  Called from tests/float/math_builtins.c:350.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:281: 
+[eva] tests/float/math_builtins.c:351: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:281: 
+[eva] tests/float/math_builtins.c:351: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:281: 
+[eva] tests/float/math_builtins.c:351: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:282.
+  Called from tests/float/math_builtins.c:352.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:283: 
+[eva] tests/float/math_builtins.c:353: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:283: 
+[eva] tests/float/math_builtins.c:353: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:283: 
+[eva] tests/float/math_builtins.c:353: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:284.
+  Called from tests/float/math_builtins.c:354.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:285: 
+[eva] tests/float/math_builtins.c:355: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:285: 
+[eva] tests/float/math_builtins.c:355: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:285: 
+[eva] tests/float/math_builtins.c:355: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:291.
+  Called from tests/float/math_builtins.c:361.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:292.
+  Called from tests/float/math_builtins.c:362.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:293: 
+[eva] tests/float/math_builtins.c:363: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:293: 
+[eva] tests/float/math_builtins.c:363: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:293: Warning: 
+[eva:alarm] tests/float/math_builtins.c:363: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:294.
+  Called from tests/float/math_builtins.c:364.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:295: 
+[eva] tests/float/math_builtins.c:365: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:295: 
+[eva] tests/float/math_builtins.c:365: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:295: Warning: 
+[eva:alarm] tests/float/math_builtins.c:365: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:296.
+  Called from tests/float/math_builtins.c:366.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:297: 
+[eva] tests/float/math_builtins.c:367: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:297: 
+[eva] tests/float/math_builtins.c:367: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:297: Warning: 
+[eva:alarm] tests/float/math_builtins.c:367: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:298.
+  Called from tests/float/math_builtins.c:368.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:299.
+  Called from tests/float/math_builtins.c:369.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:300: 
+[eva] tests/float/math_builtins.c:370: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:300: 
+[eva] tests/float/math_builtins.c:370: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:300: 
+[eva] tests/float/math_builtins.c:370: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:303.
+  Called from tests/float/math_builtins.c:373.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:304.
+  Called from tests/float/math_builtins.c:374.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:305: 
+[eva] tests/float/math_builtins.c:375: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:305: 
+[eva] tests/float/math_builtins.c:375: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:305: 
+[eva] tests/float/math_builtins.c:375: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:308.
+  Called from tests/float/math_builtins.c:378.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:309.
+  Called from tests/float/math_builtins.c:379.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:310: 
+[eva] tests/float/math_builtins.c:380: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:310: 
+[eva] tests/float/math_builtins.c:380: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:310: Warning: 
+[eva:alarm] tests/float/math_builtins.c:380: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:313.
+  Called from tests/float/math_builtins.c:383.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:314.
+  Called from tests/float/math_builtins.c:384.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:315: 
+[eva] tests/float/math_builtins.c:385: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:315: 
+[eva] tests/float/math_builtins.c:385: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:315: Warning: 
+[eva:alarm] tests/float/math_builtins.c:385: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:319.
+  Called from tests/float/math_builtins.c:389.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:320.
+  Called from tests/float/math_builtins.c:390.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:321: 
+[eva] tests/float/math_builtins.c:391: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:321: 
+[eva] tests/float/math_builtins.c:391: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:321: Warning: 
+[eva:alarm] tests/float/math_builtins.c:391: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:324.
+  Called from tests/float/math_builtins.c:394.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:325.
+  Called from tests/float/math_builtins.c:395.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:326: 
+[eva] tests/float/math_builtins.c:396: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:326: 
+[eva] tests/float/math_builtins.c:396: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:326: Warning: 
+[eva:alarm] tests/float/math_builtins.c:396: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:329.
+  Called from tests/float/math_builtins.c:399.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:330.
+  Called from tests/float/math_builtins.c:400.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:331: 
+[eva] tests/float/math_builtins.c:401: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:331: 
+[eva] tests/float/math_builtins.c:401: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:331: 
+[eva] tests/float/math_builtins.c:401: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_powf
 [eva] Done for function test_powf
 [eva] computing for function test_sqrtf_det <- main.
-  Called from tests/float/math_builtins.c:674.
-[eva] tests/float/math_builtins.c:427: 
+  Called from tests/float/math_builtins.c:747.
+[eva] tests/float/math_builtins.c:497: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:427: 
+[eva] tests/float/math_builtins.c:497: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:427: 
+[eva] tests/float/math_builtins.c:497: 
   function sqrtf: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:428: 
+[eva] tests/float/math_builtins.c:498: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:428: 
+[eva] tests/float/math_builtins.c:498: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:428: 
+[eva] tests/float/math_builtins.c:498: 
   function sqrtf: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:429: 
+[eva] tests/float/math_builtins.c:499: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:429: 
+[eva] tests/float/math_builtins.c:499: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:429: Warning: 
+[eva:alarm] tests/float/math_builtins.c:499: Warning: 
   function sqrtf: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:430: 
+[eva] tests/float/math_builtins.c:500: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:430: 
+[eva] tests/float/math_builtins.c:500: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:430: 
+[eva] tests/float/math_builtins.c:500: 
   function sqrtf: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:431: 
+[eva] tests/float/math_builtins.c:501: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:431: 
+[eva] tests/float/math_builtins.c:501: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:431: 
+[eva] tests/float/math_builtins.c:501: 
   function sqrtf: precondition 'arg_positive' got status valid.
 [eva] Recording results for test_sqrtf_det
 [eva] Done for function test_sqrtf_det
 [eva] computing for function test_sqrtf <- main.
-  Called from tests/float/math_builtins.c:675.
+  Called from tests/float/math_builtins.c:748.
 [eva] computing for function double_interval <- test_sqrtf <- main.
-  Called from tests/float/math_builtins.c:435.
+  Called from tests/float/math_builtins.c:505.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:436: 
+[eva] tests/float/math_builtins.c:506: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:436: 
+[eva] tests/float/math_builtins.c:506: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:436: 
+[eva] tests/float/math_builtins.c:506: 
   function sqrtf: precondition 'arg_positive' got status valid.
 [eva] computing for function double_interval <- test_sqrtf <- main.
-  Called from tests/float/math_builtins.c:437.
+  Called from tests/float/math_builtins.c:507.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:438: 
+[eva] tests/float/math_builtins.c:508: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:438: 
+[eva] tests/float/math_builtins.c:508: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:438: Warning: 
+[eva:alarm] tests/float/math_builtins.c:508: Warning: 
   function sqrtf: precondition 'arg_positive' got status unknown.
 [eva] computing for function double_interval <- test_sqrtf <- main.
-  Called from tests/float/math_builtins.c:439.
+  Called from tests/float/math_builtins.c:509.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:440: 
+[eva] tests/float/math_builtins.c:510: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:440: 
+[eva] tests/float/math_builtins.c:510: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:440: Warning: 
+[eva:alarm] tests/float/math_builtins.c:510: Warning: 
   function sqrtf: precondition 'arg_positive' got status unknown.
 [eva] computing for function double_interval <- test_sqrtf <- main.
-  Called from tests/float/math_builtins.c:441.
+  Called from tests/float/math_builtins.c:511.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:442: 
+[eva] tests/float/math_builtins.c:512: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:442: 
+[eva] tests/float/math_builtins.c:512: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:442: Warning: 
+[eva:alarm] tests/float/math_builtins.c:512: Warning: 
   function sqrt: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_sqrtf
 [eva] Done for function test_sqrtf
 [eva] computing for function test_expf_det <- main.
-  Called from tests/float/math_builtins.c:676.
-[eva] tests/float/math_builtins.c:455: 
+  Called from tests/float/math_builtins.c:749.
+[eva] tests/float/math_builtins.c:525: 
   Call to builtin Frama_C_expf for function expf
-[eva] tests/float/math_builtins.c:455: 
+[eva] tests/float/math_builtins.c:525: 
   function expf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:455: 
+[eva] tests/float/math_builtins.c:525: 
   function expf: precondition 'res_finite' got status valid.
-[eva] tests/float/math_builtins.c:456: 
+[eva] tests/float/math_builtins.c:526: 
   Call to builtin Frama_C_expf for function expf
-[eva] tests/float/math_builtins.c:456: 
+[eva] tests/float/math_builtins.c:526: 
   function expf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:456: 
+[eva] tests/float/math_builtins.c:526: 
   function expf: precondition 'res_finite' got status valid.
-[eva] tests/float/math_builtins.c:457: 
+[eva] tests/float/math_builtins.c:527: 
   Call to builtin Frama_C_expf for function expf
-[eva] tests/float/math_builtins.c:457: 
+[eva] tests/float/math_builtins.c:527: 
   function expf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:457: 
+[eva] tests/float/math_builtins.c:527: 
   function expf: precondition 'res_finite' got status valid.
-[eva] tests/float/math_builtins.c:458: 
+[eva] tests/float/math_builtins.c:528: 
   Call to builtin Frama_C_expf for function expf
-[eva] tests/float/math_builtins.c:458: 
+[eva] tests/float/math_builtins.c:528: 
   function expf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:458: 
+[eva] tests/float/math_builtins.c:528: 
   function expf: precondition 'res_finite' got status valid.
-[eva] tests/float/math_builtins.c:459: 
+[eva] tests/float/math_builtins.c:529: 
   Call to builtin Frama_C_expf for function expf
-[eva] tests/float/math_builtins.c:459: 
+[eva] tests/float/math_builtins.c:529: 
   function expf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:459: 
+[eva] tests/float/math_builtins.c:529: 
   function expf: precondition 'res_finite' got status valid.
 [eva] Recording results for test_expf_det
 [eva] Done for function test_expf_det
 [eva] computing for function test_logf_det <- main.
-  Called from tests/float/math_builtins.c:677.
-[eva] tests/float/math_builtins.c:472: 
+  Called from tests/float/math_builtins.c:750.
+[eva] tests/float/math_builtins.c:542: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:472: 
+[eva] tests/float/math_builtins.c:542: 
   function logf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:472: 
+[eva] tests/float/math_builtins.c:542: 
   function logf: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:473: 
+[eva] tests/float/math_builtins.c:543: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:473: 
+[eva] tests/float/math_builtins.c:543: 
   function logf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:473: 
+[eva] tests/float/math_builtins.c:543: 
   function logf: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:474: 
+[eva] tests/float/math_builtins.c:544: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:474: 
+[eva] tests/float/math_builtins.c:544: 
   function logf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:474: Warning: 
+[eva:alarm] tests/float/math_builtins.c:544: Warning: 
   function logf: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:475: 
+[eva] tests/float/math_builtins.c:545: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:475: 
+[eva] tests/float/math_builtins.c:545: 
   function logf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:475: Warning: 
+[eva:alarm] tests/float/math_builtins.c:545: Warning: 
   function logf: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:476: 
+[eva] tests/float/math_builtins.c:546: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:476: 
+[eva] tests/float/math_builtins.c:546: 
   function logf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:476: Warning: 
+[eva:alarm] tests/float/math_builtins.c:546: Warning: 
   function logf: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:477: 
+[eva] tests/float/math_builtins.c:547: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:477: 
+[eva] tests/float/math_builtins.c:547: 
   function logf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:477: Warning: 
+[eva:alarm] tests/float/math_builtins.c:547: Warning: 
   function logf: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_logf_det
 [eva] Done for function test_logf_det
 [eva] computing for function test_log10f_det <- main.
-  Called from tests/float/math_builtins.c:678.
-[eva] tests/float/math_builtins.c:490: 
+  Called from tests/float/math_builtins.c:751.
+[eva] tests/float/math_builtins.c:560: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:490: 
+[eva] tests/float/math_builtins.c:560: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:490: 
+[eva] tests/float/math_builtins.c:560: 
   function log10f: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:491: 
+[eva] tests/float/math_builtins.c:561: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:491: 
+[eva] tests/float/math_builtins.c:561: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:491: 
+[eva] tests/float/math_builtins.c:561: 
   function log10f: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:492: 
+[eva] tests/float/math_builtins.c:562: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:492: 
+[eva] tests/float/math_builtins.c:562: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:492: Warning: 
+[eva:alarm] tests/float/math_builtins.c:562: Warning: 
   function log10f: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:493: 
+[eva] tests/float/math_builtins.c:563: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:493: 
+[eva] tests/float/math_builtins.c:563: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:493: Warning: 
+[eva:alarm] tests/float/math_builtins.c:563: Warning: 
   function log10f: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:494: 
+[eva] tests/float/math_builtins.c:564: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:494: 
+[eva] tests/float/math_builtins.c:564: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:494: Warning: 
+[eva:alarm] tests/float/math_builtins.c:564: Warning: 
   function log10f: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:495: 
+[eva] tests/float/math_builtins.c:565: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:495: 
+[eva] tests/float/math_builtins.c:565: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:495: Warning: 
+[eva:alarm] tests/float/math_builtins.c:565: Warning: 
   function log10f: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_log10f_det
 [eva] Done for function test_log10f_det
 [eva] computing for function test_diff_pow_powf <- main.
-  Called from tests/float/math_builtins.c:680.
-[eva] tests/float/math_builtins.c:499: 
+  Called from tests/float/math_builtins.c:753.
+[eva] tests/float/math_builtins.c:569: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:499: 
+[eva] tests/float/math_builtins.c:569: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:499: 
+[eva] tests/float/math_builtins.c:569: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:500: 
+[eva] tests/float/math_builtins.c:570: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:500: 
+[eva] tests/float/math_builtins.c:570: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:500: 
+[eva] tests/float/math_builtins.c:570: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_diff_pow_powf
 [eva] Done for function test_diff_pow_powf
 [eva] computing for function test_floor_det <- main.
-  Called from tests/float/math_builtins.c:682.
-[eva] tests/float/math_builtins.c:504: 
+  Called from tests/float/math_builtins.c:755.
+[eva] tests/float/math_builtins.c:574: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:504: 
+[eva] tests/float/math_builtins.c:574: 
   function floor: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:505: 
+[eva] tests/float/math_builtins.c:575: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:505: 
+[eva] tests/float/math_builtins.c:575: 
   function floor: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:506: 
+[eva] tests/float/math_builtins.c:576: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:506: 
+[eva] tests/float/math_builtins.c:576: 
   function floor: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:507: 
+[eva] tests/float/math_builtins.c:577: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:507: 
+[eva] tests/float/math_builtins.c:577: 
   function floor: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:508: 
+[eva] tests/float/math_builtins.c:578: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:508: 
+[eva] tests/float/math_builtins.c:578: 
   function floor: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:509: 
+[eva] tests/float/math_builtins.c:579: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:509: 
+[eva] tests/float/math_builtins.c:579: 
   function floor: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_floor_det
 [eva] Done for function test_floor_det
 [eva] computing for function test_ceil_det <- main.
-  Called from tests/float/math_builtins.c:683.
-[eva] tests/float/math_builtins.c:513: 
+  Called from tests/float/math_builtins.c:756.
+[eva] tests/float/math_builtins.c:583: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:513: 
+[eva] tests/float/math_builtins.c:583: 
   function ceil: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:514: 
+[eva] tests/float/math_builtins.c:584: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:514: 
+[eva] tests/float/math_builtins.c:584: 
   function ceil: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:515: 
+[eva] tests/float/math_builtins.c:585: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:515: 
+[eva] tests/float/math_builtins.c:585: 
   function ceil: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:516: 
+[eva] tests/float/math_builtins.c:586: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:516: 
+[eva] tests/float/math_builtins.c:586: 
   function ceil: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:517: 
+[eva] tests/float/math_builtins.c:587: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:517: 
+[eva] tests/float/math_builtins.c:587: 
   function ceil: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:518: 
+[eva] tests/float/math_builtins.c:588: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:518: 
+[eva] tests/float/math_builtins.c:588: 
   function ceil: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_ceil_det
 [eva] Done for function test_ceil_det
 [eva] computing for function test_trunc_det <- main.
-  Called from tests/float/math_builtins.c:684.
-[eva] tests/float/math_builtins.c:522: 
+  Called from tests/float/math_builtins.c:757.
+[eva] tests/float/math_builtins.c:592: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:522: 
+[eva] tests/float/math_builtins.c:592: 
   function trunc: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:523: 
+[eva] tests/float/math_builtins.c:593: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:523: 
+[eva] tests/float/math_builtins.c:593: 
   function trunc: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:524: 
+[eva] tests/float/math_builtins.c:594: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:524: 
+[eva] tests/float/math_builtins.c:594: 
   function trunc: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:525: 
+[eva] tests/float/math_builtins.c:595: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:525: 
+[eva] tests/float/math_builtins.c:595: 
   function trunc: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:526: 
+[eva] tests/float/math_builtins.c:596: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:526: 
+[eva] tests/float/math_builtins.c:596: 
   function trunc: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:527: 
+[eva] tests/float/math_builtins.c:597: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:527: 
+[eva] tests/float/math_builtins.c:597: 
   function trunc: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_trunc_det
 [eva] Done for function test_trunc_det
 [eva] computing for function test_round_det <- main.
-  Called from tests/float/math_builtins.c:685.
-[eva] tests/float/math_builtins.c:531: 
+  Called from tests/float/math_builtins.c:758.
+[eva] tests/float/math_builtins.c:601: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:531: 
+[eva] tests/float/math_builtins.c:601: 
   function round: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:532: 
+[eva] tests/float/math_builtins.c:602: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:532: 
+[eva] tests/float/math_builtins.c:602: 
   function round: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:533: 
+[eva] tests/float/math_builtins.c:603: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:533: 
+[eva] tests/float/math_builtins.c:603: 
   function round: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:534: 
+[eva] tests/float/math_builtins.c:604: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:534: 
+[eva] tests/float/math_builtins.c:604: 
   function round: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:535: 
+[eva] tests/float/math_builtins.c:605: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:535: 
+[eva] tests/float/math_builtins.c:605: 
   function round: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:536: 
+[eva] tests/float/math_builtins.c:606: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:536: 
+[eva] tests/float/math_builtins.c:606: 
   function round: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_round_det
 [eva] Done for function test_round_det
 [eva] computing for function test_floor <- main.
-  Called from tests/float/math_builtins.c:686.
+  Called from tests/float/math_builtins.c:759.
 [eva] computing for function double_interval <- test_floor <- main.
-  Called from tests/float/math_builtins.c:541.
+  Called from tests/float/math_builtins.c:611.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:542: 
+[eva] tests/float/math_builtins.c:612: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:542: 
+[eva] tests/float/math_builtins.c:612: 
   function floor: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_floor <- main.
-  Called from tests/float/math_builtins.c:543.
+  Called from tests/float/math_builtins.c:613.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:544: 
+[eva] tests/float/math_builtins.c:614: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:544: 
+[eva] tests/float/math_builtins.c:614: 
   function floor: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_floor <- main.
-  Called from tests/float/math_builtins.c:545.
+  Called from tests/float/math_builtins.c:615.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:546: 
+[eva] tests/float/math_builtins.c:616: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:546: 
+[eva] tests/float/math_builtins.c:616: 
   function floor: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_floor
 [eva] Done for function test_floor
 [eva] computing for function test_ceil <- main.
-  Called from tests/float/math_builtins.c:687.
+  Called from tests/float/math_builtins.c:760.
 [eva] computing for function double_interval <- test_ceil <- main.
-  Called from tests/float/math_builtins.c:551.
+  Called from tests/float/math_builtins.c:621.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:552: 
+[eva] tests/float/math_builtins.c:622: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:552: 
+[eva] tests/float/math_builtins.c:622: 
   function ceil: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_ceil <- main.
-  Called from tests/float/math_builtins.c:553.
+  Called from tests/float/math_builtins.c:623.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:554: 
+[eva] tests/float/math_builtins.c:624: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:554: 
+[eva] tests/float/math_builtins.c:624: 
   function ceil: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_ceil <- main.
-  Called from tests/float/math_builtins.c:555.
+  Called from tests/float/math_builtins.c:625.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:556: 
+[eva] tests/float/math_builtins.c:626: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:556: 
+[eva] tests/float/math_builtins.c:626: 
   function ceil: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_ceil
 [eva] Done for function test_ceil
 [eva] computing for function test_trunc <- main.
-  Called from tests/float/math_builtins.c:688.
+  Called from tests/float/math_builtins.c:761.
 [eva] computing for function double_interval <- test_trunc <- main.
-  Called from tests/float/math_builtins.c:561.
+  Called from tests/float/math_builtins.c:631.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:562: 
+[eva] tests/float/math_builtins.c:632: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:562: 
+[eva] tests/float/math_builtins.c:632: 
   function trunc: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_trunc <- main.
-  Called from tests/float/math_builtins.c:563.
+  Called from tests/float/math_builtins.c:633.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:564: 
+[eva] tests/float/math_builtins.c:634: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:564: 
+[eva] tests/float/math_builtins.c:634: 
   function trunc: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_trunc <- main.
-  Called from tests/float/math_builtins.c:565.
+  Called from tests/float/math_builtins.c:635.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:566: 
+[eva] tests/float/math_builtins.c:636: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:566: 
+[eva] tests/float/math_builtins.c:636: 
   function trunc: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_trunc
 [eva] Done for function test_trunc
 [eva] computing for function test_round <- main.
-  Called from tests/float/math_builtins.c:689.
+  Called from tests/float/math_builtins.c:762.
 [eva] computing for function double_interval <- test_round <- main.
-  Called from tests/float/math_builtins.c:571.
+  Called from tests/float/math_builtins.c:641.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:572: 
+[eva] tests/float/math_builtins.c:642: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:572: 
+[eva] tests/float/math_builtins.c:642: 
   function round: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_round <- main.
-  Called from tests/float/math_builtins.c:573.
+  Called from tests/float/math_builtins.c:643.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:574: 
+[eva] tests/float/math_builtins.c:644: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:574: 
+[eva] tests/float/math_builtins.c:644: 
   function round: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_round <- main.
-  Called from tests/float/math_builtins.c:575.
+  Called from tests/float/math_builtins.c:645.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:576: 
+[eva] tests/float/math_builtins.c:646: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:576: 
+[eva] tests/float/math_builtins.c:646: 
   function round: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_round
 [eva] Done for function test_round
 [eva] computing for function test_floorf_det <- main.
-  Called from tests/float/math_builtins.c:691.
-[eva] tests/float/math_builtins.c:580: 
+  Called from tests/float/math_builtins.c:764.
+[eva] tests/float/math_builtins.c:650: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:580: 
+[eva] tests/float/math_builtins.c:650: 
   function floorf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:581: 
+[eva] tests/float/math_builtins.c:651: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:581: 
+[eva] tests/float/math_builtins.c:651: 
   function floorf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:582: 
+[eva] tests/float/math_builtins.c:652: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:582: 
+[eva] tests/float/math_builtins.c:652: 
   function floorf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:583: 
+[eva] tests/float/math_builtins.c:653: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:583: 
+[eva] tests/float/math_builtins.c:653: 
   function floorf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:584: 
+[eva] tests/float/math_builtins.c:654: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:584: 
+[eva] tests/float/math_builtins.c:654: 
   function floorf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:585: 
+[eva] tests/float/math_builtins.c:655: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:585: 
+[eva] tests/float/math_builtins.c:655: 
   function floorf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_floorf_det
 [eva] Done for function test_floorf_det
 [eva] computing for function test_ceilf_det <- main.
-  Called from tests/float/math_builtins.c:692.
-[eva] tests/float/math_builtins.c:589: 
+  Called from tests/float/math_builtins.c:765.
+[eva] tests/float/math_builtins.c:659: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:589: 
+[eva] tests/float/math_builtins.c:659: 
   function ceilf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:590: 
+[eva] tests/float/math_builtins.c:660: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:590: 
+[eva] tests/float/math_builtins.c:660: 
   function ceilf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:591: 
+[eva] tests/float/math_builtins.c:661: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:591: 
+[eva] tests/float/math_builtins.c:661: 
   function ceilf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:592: 
+[eva] tests/float/math_builtins.c:662: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:592: 
+[eva] tests/float/math_builtins.c:662: 
   function ceilf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:593: 
+[eva] tests/float/math_builtins.c:663: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:593: 
+[eva] tests/float/math_builtins.c:663: 
   function ceilf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:594: 
+[eva] tests/float/math_builtins.c:664: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:594: 
+[eva] tests/float/math_builtins.c:664: 
   function ceilf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_ceilf_det
 [eva] Done for function test_ceilf_det
 [eva] computing for function test_truncf_det <- main.
-  Called from tests/float/math_builtins.c:693.
-[eva] tests/float/math_builtins.c:598: 
+  Called from tests/float/math_builtins.c:766.
+[eva] tests/float/math_builtins.c:668: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:598: 
+[eva] tests/float/math_builtins.c:668: 
   function truncf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:599: 
+[eva] tests/float/math_builtins.c:669: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:599: 
+[eva] tests/float/math_builtins.c:669: 
   function truncf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:600: 
+[eva] tests/float/math_builtins.c:670: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:600: 
+[eva] tests/float/math_builtins.c:670: 
   function truncf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:601: 
+[eva] tests/float/math_builtins.c:671: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:601: 
+[eva] tests/float/math_builtins.c:671: 
   function truncf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:602: 
+[eva] tests/float/math_builtins.c:672: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:602: 
+[eva] tests/float/math_builtins.c:672: 
   function truncf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:603: 
+[eva] tests/float/math_builtins.c:673: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:603: 
+[eva] tests/float/math_builtins.c:673: 
   function truncf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_truncf_det
 [eva] Done for function test_truncf_det
 [eva] computing for function test_roundf_det <- main.
-  Called from tests/float/math_builtins.c:694.
-[eva] tests/float/math_builtins.c:607: 
+  Called from tests/float/math_builtins.c:767.
+[eva] tests/float/math_builtins.c:677: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:607: 
+[eva] tests/float/math_builtins.c:677: 
   function roundf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:608: 
+[eva] tests/float/math_builtins.c:678: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:608: 
+[eva] tests/float/math_builtins.c:678: 
   function roundf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:609: 
+[eva] tests/float/math_builtins.c:679: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:609: 
+[eva] tests/float/math_builtins.c:679: 
   function roundf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:610: 
+[eva] tests/float/math_builtins.c:680: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:610: 
+[eva] tests/float/math_builtins.c:680: 
   function roundf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:611: 
+[eva] tests/float/math_builtins.c:681: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:611: 
+[eva] tests/float/math_builtins.c:681: 
   function roundf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:612: 
+[eva] tests/float/math_builtins.c:682: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:612: 
+[eva] tests/float/math_builtins.c:682: 
   function roundf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_roundf_det
 [eva] Done for function test_roundf_det
 [eva] computing for function test_floorf <- main.
-  Called from tests/float/math_builtins.c:695.
+  Called from tests/float/math_builtins.c:768.
 [eva] computing for function double_interval <- test_floorf <- main.
-  Called from tests/float/math_builtins.c:617.
+  Called from tests/float/math_builtins.c:687.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:618: 
+[eva] tests/float/math_builtins.c:688: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:618: 
+[eva] tests/float/math_builtins.c:688: 
   function floorf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_floorf <- main.
-  Called from tests/float/math_builtins.c:619.
+  Called from tests/float/math_builtins.c:689.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:620: 
+[eva] tests/float/math_builtins.c:690: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:620: 
+[eva] tests/float/math_builtins.c:690: 
   function floorf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_floorf <- main.
-  Called from tests/float/math_builtins.c:621.
+  Called from tests/float/math_builtins.c:691.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:622: 
+[eva] tests/float/math_builtins.c:692: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:622: 
+[eva] tests/float/math_builtins.c:692: 
   function floorf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_floorf
 [eva] Done for function test_floorf
 [eva] computing for function test_ceilf <- main.
-  Called from tests/float/math_builtins.c:696.
+  Called from tests/float/math_builtins.c:769.
 [eva] computing for function double_interval <- test_ceilf <- main.
-  Called from tests/float/math_builtins.c:627.
+  Called from tests/float/math_builtins.c:697.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:628: 
+[eva] tests/float/math_builtins.c:698: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:628: 
+[eva] tests/float/math_builtins.c:698: 
   function ceilf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_ceilf <- main.
-  Called from tests/float/math_builtins.c:629.
+  Called from tests/float/math_builtins.c:699.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:630: 
+[eva] tests/float/math_builtins.c:700: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:630: 
+[eva] tests/float/math_builtins.c:700: 
   function ceilf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_ceilf <- main.
-  Called from tests/float/math_builtins.c:631.
+  Called from tests/float/math_builtins.c:701.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:632: 
+[eva] tests/float/math_builtins.c:702: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:632: 
+[eva] tests/float/math_builtins.c:702: 
   function ceilf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_ceilf
 [eva] Done for function test_ceilf
 [eva] computing for function test_truncf <- main.
-  Called from tests/float/math_builtins.c:697.
+  Called from tests/float/math_builtins.c:770.
 [eva] computing for function double_interval <- test_truncf <- main.
-  Called from tests/float/math_builtins.c:637.
+  Called from tests/float/math_builtins.c:707.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:638: 
+[eva] tests/float/math_builtins.c:708: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:638: 
+[eva] tests/float/math_builtins.c:708: 
   function truncf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_truncf <- main.
-  Called from tests/float/math_builtins.c:639.
+  Called from tests/float/math_builtins.c:709.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:640: 
+[eva] tests/float/math_builtins.c:710: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:640: 
+[eva] tests/float/math_builtins.c:710: 
   function truncf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_truncf <- main.
-  Called from tests/float/math_builtins.c:641.
+  Called from tests/float/math_builtins.c:711.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:642: 
+[eva] tests/float/math_builtins.c:712: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:642: 
+[eva] tests/float/math_builtins.c:712: 
   function truncf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_truncf
 [eva] Done for function test_truncf
 [eva] computing for function test_roundf <- main.
-  Called from tests/float/math_builtins.c:698.
+  Called from tests/float/math_builtins.c:771.
 [eva] computing for function double_interval <- test_roundf <- main.
-  Called from tests/float/math_builtins.c:647.
+  Called from tests/float/math_builtins.c:717.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:648: 
+[eva] tests/float/math_builtins.c:718: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:648: 
+[eva] tests/float/math_builtins.c:718: 
   function roundf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_roundf <- main.
-  Called from tests/float/math_builtins.c:649.
+  Called from tests/float/math_builtins.c:719.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:650: 
+[eva] tests/float/math_builtins.c:720: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:650: 
+[eva] tests/float/math_builtins.c:720: 
   function roundf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_roundf <- main.
-  Called from tests/float/math_builtins.c:651.
+  Called from tests/float/math_builtins.c:721.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:652: 
+[eva] tests/float/math_builtins.c:722: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:652: 
+[eva] tests/float/math_builtins.c:722: 
   function roundf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_roundf
 [eva] Done for function test_roundf
@@ -2301,6 +2432,38 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function double_interval:
   __retres ∈ [-1.2237906221789607*2^1023 .. 1.2237906221789607*2^1023]
+[eva:final-states] Values at end of function test_acos:
+  half_pi ∈ {1.5707963267948965}
+  pi ∈ {3.1415926535897931}
+  zero ∈ {0}
+  acos_image ∈ [0.0000000000000000 .. 3.1415926535897931]
+  x ∈ {1.0471975511965978}
+  y ∈ {2.0943951023931957}
+  xy ∈ [1.0471975511965978 .. 2.0943951023931957]
+  f32_half_pi ∈ {1.5707963705062866}
+  f32_pi ∈ {3.1415927410125732}
+  f32_zero ∈ {0}
+  f32_acosf_image ∈ [0.0000000000000000 .. 3.1415927410125732]
+[eva:final-states] Values at end of function test_asin:
+  zero ∈ {0}
+  minus_half_pi ∈ {-1.5707963267948965}
+  half_pi ∈ {1.5707963267948965}
+  asin_image ∈ [-1.5707963267948965 .. 1.5707963267948965]
+  x ∈ {-1.0471975511965978*2^-1}
+  y ∈ {1.0471975511965978*2^-1}
+  xy ∈ [-1.0471975511965978*2^-1 .. 1.0471975511965978*2^-1]
+  f32_zero ∈ {0}
+  f32_minus_half_pi ∈ {-1.5707963705062866}
+  f32_half_pi ∈ {1.5707963705062866}
+  f32_asinf_image ∈ [-1.5707963705062866 .. 1.5707963705062866]
+[eva:final-states] Values at end of function test_atan:
+  zero ∈ {0}
+  atan_image ∈ [-1.5707963267948965 .. 1.5707963267948965]
+  x ∈ {-1.1071487177940904}
+  y ∈ {1.1071487177940904}
+  xy ∈ [-1.1071487177940904 .. 1.1071487177940904]
+  f32_zero ∈ {0}
+  f32_atanf_image ∈ [-1.5707963705062866 .. 1.5707963705062866]
 [eva:final-states] Values at end of function test_atan2:
   x ∈ [1.0000000000000000 .. 5.0000000000000000]
   y ∈ [-0.0000000000000000 .. 0.0000000000000000]
@@ -2618,6 +2781,24 @@
   __retres ∈ {0}
 [from] Computing for function double_interval
 [from] Done for function double_interval
+[from] Computing for function test_acos
+[from] Computing for function acos <-test_acos
+[from] Done for function acos
+[from] Computing for function acosf <-test_acos
+[from] Done for function acosf
+[from] Done for function test_acos
+[from] Computing for function test_asin
+[from] Computing for function asin <-test_asin
+[from] Done for function asin
+[from] Computing for function asinf <-test_asin
+[from] Done for function asinf
+[from] Done for function test_asin
+[from] Computing for function test_atan
+[from] Computing for function atan <-test_atan
+[from] Done for function atan
+[from] Computing for function atanf <-test_atan
+[from] Done for function atanf
+[from] Done for function test_atan
 [from] Computing for function test_atan2
 [from] Computing for function atan2 <-test_atan2
 [from] Done for function atan2
@@ -2744,8 +2925,20 @@
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
+[from] Function acos:
+  \result FROM x
+[from] Function acosf:
+  \result FROM x
+[from] Function asin:
+  \result FROM x
+[from] Function asinf:
+  \result FROM x
+[from] Function atan:
+  \result FROM x
 [from] Function atan2:
   \result FROM y; x
+[from] Function atanf:
+  \result FROM x
 [from] Function ceil:
   \result FROM x
 [from] Function ceilf:
@@ -2786,6 +2979,12 @@
   \result FROM x
 [from] Function sqrtf:
   \result FROM x
+[from] Function test_acos:
+  NO EFFECTS
+[from] Function test_asin:
+  NO EFFECTS
+[from] Function test_atan:
+  NO EFFECTS
 [from] Function test_atan2:
   NO EFFECTS
 [from] Function test_atan2_det:
@@ -2875,6 +3074,20 @@
     __retres
 [inout] Inputs for function double_interval:
     nondet
+[inout] Out (internal) for function test_acos:
+    half_pi; pi; zero; acos_image; bottom; bottom_0; x; y; xy; f32_half_pi;
+    f32_pi; f32_zero; f32_acosf_image; bottom_1
+[inout] Inputs for function test_acos:
+    nondet; any_double; any_float
+[inout] Out (internal) for function test_asin:
+    zero; minus_half_pi; half_pi; asin_image; bottom; bottom_0; x; y; xy;
+    f32_zero; f32_minus_half_pi; f32_half_pi; f32_asinf_image; bottom_1
+[inout] Inputs for function test_asin:
+    nondet; any_double; any_float
+[inout] Out (internal) for function test_atan:
+    zero; atan_image; x; y; xy; f32_zero; f32_atanf_image
+[inout] Inputs for function test_atan:
+    nondet; any_double; any_float
 [inout] Out (internal) for function test_atan2:
     x; y; a; b; c; d; e; f; g; h; i; j; k; l; m; n
 [inout] Inputs for function test_atan2:
@@ -3040,11 +3253,13 @@
 [inout] Out (internal) for function main:
     __retres
 [inout] Inputs for function main:
-    nondet
+    nondet; any_double; any_float
 /* Generated by Frama-C */
 #include "errno.h"
 #include "math.h"
 static int volatile nondet;
+static double volatile any_double;
+static float volatile any_float;
 double double_interval(double min, double max)
 {
   double __retres;
@@ -3075,6 +3290,79 @@ void test_sin_det(void)
   return;
 }
 
+extern int ( /* missing proto */ Frama_C_show_each_bottom)();
+
+void test_acos(void)
+{
+  double half_pi = acos(0.);
+  double pi = acos(- 1.);
+  double zero = acos(1.);
+  double acos_image = acos(any_double);
+  if (nondet) {
+    double bottom = acos(- 1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  if (nondet) {
+    double bottom_0 = acos(1.5);
+    Frama_C_show_each_bottom(bottom_0);
+  }
+  double x = acos(0.5);
+  double y = acos(- 0.5);
+  double xy = double_interval(- 0.5,0.5);
+  xy = acos(xy);
+  float f32_half_pi = acosf(0.f);
+  float f32_pi = acosf(- 1.f);
+  float f32_zero = acosf(1.f);
+  float f32_acosf_image = acosf(any_float);
+  if (nondet) {
+    float bottom_1 = acosf(2.f);
+    Frama_C_show_each_bottom(bottom_1);
+  }
+  return;
+}
+
+void test_asin(void)
+{
+  double zero = asin(0.);
+  double minus_half_pi = asin(- 1.);
+  double half_pi = asin(1.);
+  double asin_image = asin(any_double);
+  if (nondet) {
+    double bottom = asin(- 1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  if (nondet) {
+    double bottom_0 = asin(1.5);
+    Frama_C_show_each_bottom(bottom_0);
+  }
+  double x = asin(- 0.5);
+  double y = asin(0.5);
+  double xy = double_interval(- 0.5,0.5);
+  xy = asin(xy);
+  float f32_zero = asinf(0.f);
+  float f32_minus_half_pi = asinf(- 1.f);
+  float f32_half_pi = asinf(1.f);
+  float f32_asinf_image = asinf(any_float);
+  if (nondet) {
+    float bottom_1 = asinf(2.f);
+    Frama_C_show_each_bottom(bottom_1);
+  }
+  return;
+}
+
+void test_atan(void)
+{
+  double zero = atan(0.);
+  double atan_image = atan(any_double);
+  double x = atan(- 2.);
+  double y = atan(2.);
+  double xy = double_interval(- 2.,2.);
+  xy = atan(xy);
+  float f32_zero = atanf(0.f);
+  float f32_atanf_image = atanf(any_float);
+  return;
+}
+
 void test_atan2_det(void)
 {
   double a = atan2(1.,0.);
@@ -3903,6 +4191,9 @@ int main(void)
   int __retres;
   test_cos_det();
   test_sin_det();
+  test_acos();
+  test_asin();
+  test_atan();
   test_atan2_det();
   test_atan2();
   test_pow_det();
-- 
GitLab