[Eva] Adds tests of the evaluation of ACSL predicate is_infinite.

tests/float/oracle/special_floats.res.oracle

@@ -8,11 +8,11 @@
   global_infinity ∈ {inf}
   global_nan ∈ NaN
 [eva] computing for function nan_comparisons <- main.
-  Called from tests/float/special_floats.c:94.
+  Called from tests/float/special_floats.c:117.
 [eva] Recording results for nan_comparisons
 [eva] Done for function nan_comparisons
 [eva] computing for function is_infinite <- main.
-  Called from tests/float/special_floats.c:95.
+  Called from tests/float/special_floats.c:118.
 [eva] tests/float/special_floats.c:29: check 'true' got status valid.
 [eva:alarm] tests/float/special_floats.c:30: Warning: 
   check 'false' got status invalid.
@@ -20,53 +20,80 @@
   check 'false' got status invalid.
 [eva:alarm] tests/float/special_floats.c:32: Warning: 
   check 'false' got status invalid.
-[eva:alarm] tests/float/special_floats.c:34: Warning: 
+[eva:alarm] tests/float/special_floats.c:33: Warning: 
   check 'false' got status invalid.
-[eva] tests/float/special_floats.c:35: check 'true' got status valid.
-[eva] tests/float/special_floats.c:36: check 'true' got status valid.
-[eva:alarm] tests/float/special_floats.c:37: Warning: 
+[eva:alarm] tests/float/special_floats.c:35: Warning: 
   check 'false' got status invalid.
+[eva] tests/float/special_floats.c:36: check 'true' got status valid.
+[eva] tests/float/special_floats.c:37: check 'true' got status valid.
+[eva] tests/float/special_floats.c:38: check 'true' got status valid.
 [eva:alarm] tests/float/special_floats.c:39: Warning: 
   check 'false' got status invalid.
-[eva] tests/float/special_floats.c:40: check 'true' got status valid.
 [eva:alarm] tests/float/special_floats.c:41: Warning: 
   check 'false' got status invalid.
-[eva:alarm] tests/float/special_floats.c:42: Warning: 
+[eva] tests/float/special_floats.c:42: check 'true' got status valid.
+[eva:alarm] tests/float/special_floats.c:43: Warning: 
   check 'false' got status invalid.
-[eva:alarm] tests/float/special_floats.c:46: Warning: 
-  assertion got status unknown.
-[eva] tests/float/special_floats.c:47: Frama_C_show_each_pos_infinity: {inf}
+[eva:alarm] tests/float/special_floats.c:44: Warning: 
+  check 'false' got status invalid.
+[eva:alarm] tests/float/special_floats.c:45: Warning: 
+  check 'false' got status invalid.
+[eva:alarm] tests/float/special_floats.c:49: Warning: 
+  check 'unknown' got status unknown.
 [eva:alarm] tests/float/special_floats.c:50: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/float/special_floats.c:51: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/float/special_floats.c:52: Warning: 
+  check 'false' got status invalid.
+[eva:alarm] tests/float/special_floats.c:53: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/float/special_floats.c:57: Warning: 
   assertion got status unknown.
-[eva] tests/float/special_floats.c:51: Frama_C_show_each_neg_infinity: {-inf}
-[eva:alarm] tests/float/special_floats.c:54: Warning: 
+[eva] tests/float/special_floats.c:58: Frama_C_show_each_pos_infinity: {inf}
+[eva:alarm] tests/float/special_floats.c:61: Warning: 
   assertion got status unknown.
-[eva:alarm] tests/float/special_floats.c:55: Warning: 
+[eva] tests/float/special_floats.c:62: Frama_C_show_each_neg_infinity: {-inf}
+[eva:alarm] tests/float/special_floats.c:65: Warning: 
   assertion got status unknown.
-[eva] tests/float/special_floats.c:56: 
+[eva] tests/float/special_floats.c:66: 
+  Frama_C_show_each_infinities: [-inf .. inf]
+[eva:alarm] tests/float/special_floats.c:69: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/float/special_floats.c:70: Warning: 
+  assertion got status unknown.
+[eva] tests/float/special_floats.c:71: 
+  Frama_C_show_each_finite_nan:
+  [-1.79769313486e+308 .. 1.79769313486e+308] ∪ {NaN}
+[eva:alarm] tests/float/special_floats.c:74: Warning: 
+  assertion got status unknown.
+[eva] tests/float/special_floats.c:75: 
   Frama_C_show_each_finite_nan:
   [-1.79769313486e+308 .. 1.79769313486e+308] ∪ {NaN}
-[eva:alarm] tests/float/special_floats.c:59: Warning: 
+[eva:alarm] tests/float/special_floats.c:78: Warning: 
   assertion got status unknown.
-[eva] tests/float/special_floats.c:60: 
+[eva] tests/float/special_floats.c:79: 
   Frama_C_show_each_top: [-inf .. inf] ∪ {NaN}
-[eva:alarm] tests/float/special_floats.c:63: Warning: 
+[eva:alarm] tests/float/special_floats.c:82: Warning: 
+  assertion got status unknown.
+[eva] tests/float/special_floats.c:83: Frama_C_show_each_pos_infinity: {inf;NaN}
+[eva:alarm] tests/float/special_floats.c:86: Warning: 
   assertion got status unknown.
-[eva] tests/float/special_floats.c:64: Frama_C_show_each_pos_infinity: {inf;NaN}
+[eva] tests/float/special_floats.c:87: Frama_C_show_each_neg_infinity: {-inf}
 [eva] Recording results for is_infinite
 [eva] Done for function is_infinite
 [eva] computing for function macro_infinity <- main.
-  Called from tests/float/special_floats.c:96.
-[eva] tests/float/special_floats.c:74: Frama_C_show_each_infinity: {inf}
-[eva] tests/float/special_floats.c:75: assertion got status valid.
+  Called from tests/float/special_floats.c:119.
+[eva] tests/float/special_floats.c:97: Frama_C_show_each_infinity: {inf}
+[eva] tests/float/special_floats.c:98: assertion got status valid.
 [eva] Recording results for macro_infinity
 [eva] Done for function macro_infinity
 [eva] computing for function macro_nan <- main.
-  Called from tests/float/special_floats.c:97.
-[eva] tests/float/special_floats.c:84: Frama_C_show_each_nan: NaN
-[eva] tests/float/special_floats.c:85: assertion got status valid.
-[eva] tests/float/special_floats.c:86: assertion got status valid.
-[eva] tests/float/special_floats.c:87: assertion got status valid.
+  Called from tests/float/special_floats.c:120.
+[eva] tests/float/special_floats.c:107: Frama_C_show_each_nan: NaN
+[eva] tests/float/special_floats.c:108: assertion got status valid.
+[eva] tests/float/special_floats.c:109: assertion got status valid.
+[eva] tests/float/special_floats.c:110: assertion got status valid.
 [eva] Recording results for macro_nan
 [eva] Done for function macro_nan
 [eva] Recording results for main

tests/float/special_floats.c

@@ -28,19 +28,30 @@ void is_infinite () {
   double zero = -0.;
   /*@ check true: \is_finite(zero); */
   /*@ check false: !\is_finite(zero); */
+  /*@ check false: \is_infinite(zero); */
   /*@ check false: \is_plus_infinity(zero); */
   /*@ check false: \is_minus_infinity(zero); */
   double inf = INFINITY;
   /*@ check false: \is_finite(inf); */
   /*@ check true: !\is_finite(inf); */
+  /*@ check true: \is_infinite(inf); */
   /*@ check true: \is_plus_infinity(inf); */
   /*@ check false: \is_minus_infinity(inf); */
   double nan = NAN;
   /*@ check false: \is_finite(nan); */
   /*@ check true: !\is_finite(nan); */
+  /*@ check false: \is_infinite(nan); */
   /*@ check false: \is_plus_infinity(nan); */
   /*@ check false: \is_minus_infinity(nan); */
-  double d = any_double;
+  double d;
+  /* Tests the evaluation on imprecise values. */
+  d = rand ? zero : (rand ? -inf : nan);
+  /*@ check unknown:  \is_finite(d); */
+  /*@ check unknown: !\is_finite(d); */
+  /*@ check unknown:  \is_infinite(d); */
+  /*@ check false:    \is_plus_infinity(d); */
+  /*@ check unknown:  \is_minus_infinity(d); */
+  d = any_double;
   /* Tests the reduction by assertions. */
   if (rand) {
     /*@ assert \is_plus_infinity(d); */
@@ -50,11 +61,19 @@ void is_infinite () {
     /*@ assert \is_minus_infinity(d); */
     Frama_C_show_each_neg_infinity(d);
   }
+  if (rand) {
+    /*@ assert \is_infinite(d); */
+    Frama_C_show_each_infinities(d);
+  }
   if (rand) {
     /*@ assert !\is_plus_infinity(d); */
     /*@ assert !\is_minus_infinity(d); */
     Frama_C_show_each_finite_nan(d);
   }
+  if (rand) {
+    /*@ assert !\is_infinite(d); */
+    Frama_C_show_each_finite_nan(d);
+  }
   if (rand) {
     /*@ assert !\is_finite(d); */
     Frama_C_show_each_top(d);
@@ -63,6 +82,10 @@ void is_infinite () {
     /*@ assert !\is_finite(d); */
     Frama_C_show_each_pos_infinity(d);
   }
+  if (d < 0.) {
+    /*@ assert \is_infinite(d); */
+    Frama_C_show_each_neg_infinity(d);
+  }
 }
 
 float global_infinity = INFINITY;