[kernel] Rewrites the test float/contract_finite_float.c

tests/float/contract_finite_float.c

-/* run.config*
-   OPT: -eva @EVA_CONFIG@ -warn-special-float none -contract-finite-float
-*/
-
-#include <math.h>
-
-
-/*@ 
-    assigns \result \from x;
-    behavior normal:
-      assumes finite_arg: \is_finite(x);
-      ensures res_finite: \is_finite(\result);
-      ensures positive_result: \result >= 0.;
-      ensures equal_magnitude_result: \result == x || \result == -x;
-    behavior nan:
-      assumes nan_arg: \is_NaN(x);
-      ensures  res_nan: \is_NaN(\result);
-    behavior infinite:
-      assumes infinite_arg: \is_infinite(x);
-      ensures  res_plus_infinity: \is_plus_infinity(\result);
-*/
-extern double myfabs(double x);
-
-volatile double x;
-
-int main(){
-  double z = x;
-  double y = myfabs(x);
-}

tests/float/contract_special_float.c

+/* run.config*
+   OPT: -eva @EVA_CONFIG@ -warn-special-float non-finite
+   OPT: -eva @EVA_CONFIG@ -warn-special-float nan
+   OPT: -eva @EVA_CONFIG@ -warn-special-float none
+*/
+
+/*@
+  assigns \result \from x;
+  behavior normal:
+    assumes domain_arg: \is_plus_infinity(x) || (\is_finite(x) && x >= 1.);
+    ensures finite_result: \is_finite(\result);
+    ensures positive_result: \result >= 0.;
+  behavior negative:
+    assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < 0.);
+    ensures nan_result: \is_NaN(\result);
+  behavior infinite:
+    assumes small_arg: \is_finite(x) && x >= 0. && x < 1.;
+    ensures infinite_result: \is_plus_infinity(\result);
+  behavior nan:
+    assumes nan_arg: \is_NaN(x);
+    ensures nan_result: \is_NaN(\result);
+  complete behaviors;
+  disjoint behaviors;
+*/
+extern double fun(double x);
+
+/*@
+  behavior normal:
+    assumes domain_arg: \is_plus_infinity(x) || (\is_finite(x) && x >= 1.);
+    assigns \result \from x;
+    ensures finite_result: \is_finite(\result);
+    ensures positive_result: \result >= 0.;
+  behavior negative:
+    assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < 0.);
+    assigns \result \from x;
+    ensures nan_result: \is_NaN(\result);
+  behavior infinite:
+    assumes small_arg: \is_finite(x) && x >= 0. && x < 1.;
+    assigns \result \from x;
+    ensures infinite_result: \is_plus_infinity(\result);
+  behavior nan:
+    assumes nan_arg: \is_NaN(x);
+    assigns \result \from x;
+    ensures nan_result: \is_NaN(\result);
+  complete behaviors;
+  disjoint behaviors;
+*/
+extern double fun_no_default(double x);
+
+/*@
+  assigns \result \from x;
+  behavior normal:
+    assumes domain_arg: \is_plus_infinity(x) || (\is_finite(x) && x >= 1.);
+    ensures finite_result: \is_finite(\result);
+    ensures positive_result: \result >= 0.;
+  behavior negative:
+    assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < 0.);
+    ensures nan_result: \is_NaN(\result);
+  behavior infinite:
+    assumes small_arg: \is_finite(x) && x >= 0. && x < 1.;
+    ensures infinite_result: \is_plus_infinity(\result);
+  behavior nan:
+    assumes nan_arg: \is_NaN(x);
+    ensures nan_result: \is_NaN(\result);
+  complete behaviors;
+*/
+extern double fun_no_disjoint(double x);
+
+/*@
+  assigns \result \from x;
+  behavior normal:
+    assumes domain_arg: \is_plus_infinity(x) || (\is_finite(x) && x >= 1.);
+    ensures finite_result: \is_finite(\result);
+    ensures positive_result: \result >= 0.;
+  behavior negative:
+    assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < 0.);
+    ensures nan_result: \is_NaN(\result);
+  behavior infinite:
+    assumes small_arg: \is_finite(x) && x >= 0. && x < 1.;
+    ensures infinite_result: \is_plus_infinity(\result);
+  behavior nan:
+    assumes nan_arg: \is_NaN(x);
+    ensures nan_result: \is_NaN(\result);
+  disjoint behaviors;
+*/
+extern double fun_no_complete(double x);
+
+volatile double v;
+
+int main(){
+  double a = v;
+  double w = fun(a);
+  double b = v;
+  double x = fun_no_default(b); // no default behavior
+  double c = v;
+  double y = fun_no_disjoint(c); // no disjoint behaviors
+  double d = v;
+  double z = fun_no_complete(d); // no complete behaviors
+}

tests/float/oracle/contract_finite_float.res.oracle

-[kernel] Parsing tests/float/contract_finite_float.c (with preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-  x ∈ [--..--]
-[eva] computing for function myfabs <- main.
-  Called from tests/float/contract_finite_float.c:28.
-[eva] using specification for function myfabs
-[eva:alarm] tests/float/contract_finite_float.c:28: Warning: 
-  function myfabs: precondition ¬(infinite_arg: \is_infinite(x)) got status unknown.
-[eva:alarm] tests/float/contract_finite_float.c:28: Warning: 
-  function myfabs: precondition ¬(nan_arg: \is_NaN(x)) got status unknown.
-[eva] Done for function myfabs
-[eva] Recording results for main
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
-  z ∈ [-inf .. inf] ∪ {NaN}
-  y ∈ [-inf .. inf] ∪ {NaN}
-  __retres ∈ {0}

tests/float/oracle/contract_special_float.0.res.oracle

+[kernel] Parsing tests/float/contract_special_float.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  v ∈ [--..--]
+[eva:alarm] tests/float/contract_special_float.c:91: Warning: 
+  non-finite double value. assert \is_finite(v);
+[eva] computing for function fun <- main.
+  Called from tests/float/contract_special_float.c:92.
+[eva] using specification for function fun
+[eva:alarm] tests/float/contract_special_float.c:92: Warning: 
+  function fun: precondition 'domain_arg' got status unknown.
+[eva] Done for function fun
+[eva:alarm] tests/float/contract_special_float.c:93: Warning: 
+  non-finite double value. assert \is_finite(v);
+[eva] computing for function fun_no_default <- main.
+  Called from tests/float/contract_special_float.c:94.
+[eva] using specification for function fun_no_default
+[eva:alarm] tests/float/contract_special_float.c:94: Warning: 
+  function fun_no_default: precondition 'domain_arg' got status unknown.
+[eva] Done for function fun_no_default
+[eva:alarm] tests/float/contract_special_float.c:95: Warning: 
+  non-finite double value. assert \is_finite(v);
+[eva] computing for function fun_no_disjoint <- main.
+  Called from tests/float/contract_special_float.c:96.
+[eva] using specification for function fun_no_disjoint
+[eva:alarm] tests/float/contract_special_float.c:96: Warning: 
+  function fun_no_disjoint: precondition ¬(negative_arg:
+                                              \is_minus_infinity(x) ∨
+                                              (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva:alarm] tests/float/contract_special_float.c:96: Warning: 
+  function fun_no_disjoint: precondition ¬(small_arg:
+                                              \is_finite(x) ∧ x ≥ 0. ∧
+                                              x < 1.) got status unknown.
+[eva] tests/float/contract_special_float.c:96: 
+  function fun_no_disjoint: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun_no_disjoint
+[eva:alarm] tests/float/contract_special_float.c:97: Warning: 
+  non-finite double value. assert \is_finite(v);
+[eva] computing for function fun_no_complete <- main.
+  Called from tests/float/contract_special_float.c:98.
+[eva] using specification for function fun_no_complete
+[eva:alarm] tests/float/contract_special_float.c:98: Warning: 
+  function fun_no_complete: precondition ¬(negative_arg:
+                                              \is_minus_infinity(x) ∨
+                                              (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva:alarm] tests/float/contract_special_float.c:98: Warning: 
+  function fun_no_complete: precondition ¬(small_arg:
+                                              \is_finite(x) ∧ x ≥ 0. ∧
+                                              x < 1.) got status unknown.
+[eva] tests/float/contract_special_float.c:98: 
+  function fun_no_complete: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun_no_complete
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  a ∈ [1. .. 1.79769313486e+308]
+  w ∈ [-0. .. 1.79769313486e+308]
+  b ∈ [1. .. 1.79769313486e+308]
+  x ∈ [-0. .. 1.79769313486e+308]
+  c ∈ [1. .. 1.79769313486e+308]
+  y ∈ [-0. .. 1.79769313486e+308]
+  d ∈ [1. .. 1.79769313486e+308]
+  z ∈ [-0. .. 1.79769313486e+308]
+  __retres ∈ {0}

tests/float/oracle/contract_special_float.1.res.oracle

+[kernel] Parsing tests/float/contract_special_float.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  v ∈ [--..--]
+[eva:alarm] tests/float/contract_special_float.c:91: Warning: 
+  NaN double value. assert ¬\is_NaN(v);
+[eva] computing for function fun <- main.
+  Called from tests/float/contract_special_float.c:92.
+[eva] using specification for function fun
+[eva:alarm] tests/float/contract_special_float.c:92: Warning: 
+  function fun: precondition ¬(negative_arg:
+                                  \is_minus_infinity(x) ∨
+                                  (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva] tests/float/contract_special_float.c:92: 
+  function fun: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun
+[eva:alarm] tests/float/contract_special_float.c:93: Warning: 
+  NaN double value. assert ¬\is_NaN(v);
+[eva] computing for function fun_no_default <- main.
+  Called from tests/float/contract_special_float.c:94.
+[kernel] tests/float/contract_special_float.c:94: Warning: 
+  No code nor explicit assigns clause for function fun_no_default, generating default assigns from the specification
+[eva] using specification for function fun_no_default
+[eva:alarm] tests/float/contract_special_float.c:94: Warning: 
+  function fun_no_default: precondition ¬(negative_arg:
+                                             \is_minus_infinity(x) ∨
+                                             (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva] tests/float/contract_special_float.c:94: 
+  function fun_no_default: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun_no_default
+[eva:alarm] tests/float/contract_special_float.c:95: Warning: 
+  NaN double value. assert ¬\is_NaN(v);
+[eva] computing for function fun_no_disjoint <- main.
+  Called from tests/float/contract_special_float.c:96.
+[eva] using specification for function fun_no_disjoint
+[eva:alarm] tests/float/contract_special_float.c:96: Warning: 
+  function fun_no_disjoint: precondition ¬(negative_arg:
+                                              \is_minus_infinity(x) ∨
+                                              (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva] tests/float/contract_special_float.c:96: 
+  function fun_no_disjoint: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun_no_disjoint
+[eva:alarm] tests/float/contract_special_float.c:97: Warning: 
+  NaN double value. assert ¬\is_NaN(v);
+[eva] computing for function fun_no_complete <- main.
+  Called from tests/float/contract_special_float.c:98.
+[eva] using specification for function fun_no_complete
+[eva:alarm] tests/float/contract_special_float.c:98: Warning: 
+  function fun_no_complete: precondition ¬(negative_arg:
+                                              \is_minus_infinity(x) ∨
+                                              (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva] tests/float/contract_special_float.c:98: 
+  function fun_no_complete: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun_no_complete
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  a ∈ [-0. .. inf]
+  w ∈ [-0. .. inf]
+  b ∈ [-0. .. inf]
+  x ∈ [-0. .. inf]
+  c ∈ [-0. .. inf]
+  y ∈ [-0. .. inf]
+  d ∈ [-1.79769313486e+308 .. inf]
+  z ∈ [-inf .. inf] ∪ {NaN}
+  __retres ∈ {0}

tests/float/oracle/contract_special_float.2.res.oracle

+[kernel] Parsing tests/float/contract_special_float.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  v ∈ [--..--]
+[eva] computing for function fun <- main.
+  Called from tests/float/contract_special_float.c:92.
+[eva] using specification for function fun
+[eva] Done for function fun
+[eva] computing for function fun_no_default <- main.
+  Called from tests/float/contract_special_float.c:94.
+[kernel] tests/float/contract_special_float.c:94: Warning: 
+  No code nor explicit assigns clause for function fun_no_default, generating default assigns from the specification
+[eva] using specification for function fun_no_default
+[eva] Done for function fun_no_default
+[eva] computing for function fun_no_disjoint <- main.
+  Called from tests/float/contract_special_float.c:96.
+[eva] using specification for function fun_no_disjoint
+[eva] Done for function fun_no_disjoint
+[eva] computing for function fun_no_complete <- main.
+  Called from tests/float/contract_special_float.c:98.
+[eva] using specification for function fun_no_complete
+[eva] Done for function fun_no_complete
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  a ∈ [-inf .. inf] ∪ {NaN}
+  w ∈ [-0. .. inf] ∪ {NaN}
+  b ∈ [-inf .. inf] ∪ {NaN}
+  x ∈ [-0. .. inf] ∪ {NaN}
+  c ∈ [-inf .. inf] ∪ {NaN}
+  y ∈ [-0. .. inf] ∪ {NaN}
+  d ∈ [-inf .. inf] ∪ {NaN}
+  z ∈ [-inf .. inf] ∪ {NaN}
+  __retres ∈ {0}