[Libc] add specs for __finite and __finitef

share/libc/math.h

@@ -702,8 +702,30 @@ extern double fma(double x, double y, double z);
 extern float fmaf(float x, float y, float z);
 extern long double fmal(long double x, long double y, long double z);
 
+/*@
+  assigns \result \from f;
+  behavior finite:
+    assumes isfinite_f: \is_finite(f);
+    ensures nonzero_result: \result > 0 || \result < 0;
+  behavior nonfinite:
+    assumes nonfinite_f: !\is_finite(f);
+    ensures zero_result: \result == 0;
+  complete behaviors;
+  disjoint behaviors;
+*/
 extern int __finitef(float f);
 
+/*@
+  assigns \result \from d;
+  behavior finite:
+    assumes isfinite_d: \is_finite(d);
+    ensures nonzero_result: \result > 0 || \result < 0;
+  behavior nonfinite:
+    assumes nonfinite_d: !\is_finite(d);
+    ensures zero_result: \result == 0;
+  complete behaviors;
+  disjoint behaviors;
+*/
 extern int __finite(double d);
 
 #  define isfinite(x) \

tests/idct/oracle/ieee_1180_1990.res.oracle

@@ -3561,6 +3561,58 @@
             default behavior
             by Frama-C kernel.
 
+--------------------------------------------------------------------------------
+--- Properties of Function '__finitef'
+--------------------------------------------------------------------------------
+
+[ Extern  ] Post-condition for 'finite' 'nonzero_result'
+            ensures nonzero_result: \result > 0 ∨ \result < 0
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'nonfinite' 'zero_result'
+            ensures zero_result: \result ≡ 0
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns nothing
+            assigns \nothing;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/math.h, line 706)
+            assigns \result \from f;
+            Unverifiable but considered Valid.
+[  Valid  ] Default behavior
+            default behavior
+            by Frama-C kernel.
+[  Valid  ] Behavior 'finite'
+            behavior finite
+            by Frama-C kernel.
+[  Valid  ] Behavior 'nonfinite'
+            behavior nonfinite
+            by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function '__finite'
+--------------------------------------------------------------------------------
+
+[ Extern  ] Post-condition for 'finite' 'nonzero_result'
+            ensures nonzero_result: \result > 0 ∨ \result < 0
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'nonfinite' 'zero_result'
+            ensures zero_result: \result ≡ 0
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns nothing
+            assigns \nothing;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/math.h, line 719)
+            assigns \result \from d;
+            Unverifiable but considered Valid.
+[  Valid  ] Default behavior
+            default behavior
+            by Frama-C kernel.
+[  Valid  ] Behavior 'finite'
+            behavior finite
+            by Frama-C kernel.
+[  Valid  ] Behavior 'nonfinite'
+            behavior nonfinite
+            by Frama-C kernel.
+
 --------------------------------------------------------------------------------
 --- Properties of Function '__fc_infinity'
 --------------------------------------------------------------------------------
@@ -3571,7 +3623,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 724)
+[ Extern  ] Froms (file share/libc/math.h, line 746)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3588,7 +3640,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 730)
+[ Extern  ] Froms (file share/libc/math.h, line 752)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3950,9 +4002,9 @@
 --------------------------------------------------------------------------------
 --- Status Report Summary
 --------------------------------------------------------------------------------
-   169 Completely validated
+   175 Completely validated
     16 Locally validated
-   454 Considered valid
+   462 Considered valid
     56 To be validated
-   695 Total
+   709 Total
 --------------------------------------------------------------------------------

tests/libc/math_h.c

 /* run.config
    FILTER: sed -E -e '/atanf_/ s/([0-9][.][0-9]{6})[0-9]+/\1/g'
-   STDOPT: #"-warn-special-float none" #"-cpp-extra-args=\"-DNONFINITE\""
+   STDOPT: #"-warn-special-float none" #"-cpp-extra-args=\"-DNONFINITE\"" #"-eva-slevel 4"
 */
 #include <math.h>
 const double pi = 3.14159265358979323846264338327950288;
@@ -48,4 +48,20 @@ int main() {
   TEST_FUN(double,fabs,);
   TEST_FUN(float,fabsf,f_);
   TEST_FUN(long double,fabsl,ld_);
+
+#ifdef NONFINITE
+  int r;
+  r = isfinite(pi);
+  //@ assert r;
+  r = isfinite(large);
+  //@ assert r;
+  r = isfinite(0.0f);
+  //@ assert r;
+  r = isfinite(huge_val);
+  //@ assert !r;
+  r = isfinite(-INFINITY);
+  //@ assert !r;
+  r = isfinite(NAN);
+  //@ assert !r;
+#endif
 }

tests/libc/oracle/fc_libc.1.res.oracle

@@ -3390,6 +3390,20 @@ float fabsf(float x)
   return_label: return __retres;
 }
 
+/*@ assigns \result;
+    assigns \result \from f;
+    
+    behavior finite:
+      assumes isfinite_f: \is_finite(f);
+      ensures nonzero_result: \result > 0 ∨ \result < 0;
+    
+    behavior nonfinite:
+      assumes nonfinite_f: ¬\is_finite(f);
+      ensures zero_result: \result ≡ 0;
+    
+    complete behaviors nonfinite, finite;
+    disjoint behaviors nonfinite, finite;
+ */
 int __finitef(float f)
 {
   int __retres;
@@ -3402,6 +3416,20 @@ int __finitef(float f)
   return __retres;
 }
 
+/*@ assigns \result;
+    assigns \result \from d;
+    
+    behavior finite:
+      assumes isfinite_d: \is_finite(d);
+      ensures nonzero_result: \result > 0 ∨ \result < 0;
+    
+    behavior nonfinite:
+      assumes nonfinite_d: ¬\is_finite(d);
+      ensures zero_result: \result ≡ 0;
+    
+    complete behaviors nonfinite, finite;
+    disjoint behaviors nonfinite, finite;
+ */
 int __finite(double d)
 {
   int __retres;

tests/libc/oracle/math_h.res.oracle

@@ -267,6 +267,41 @@
 [eva:alarm] tests/libc/math_h.c:50: Warning: 
   function fabsl: precondition 'finite_arg' got status unknown.
 [eva] Done for function fabsl
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:54.
+[eva] using specification for function __finite
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:55: assertion got status valid.
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:56.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:56.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:57: assertion got status valid.
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:58.
+[eva] using specification for function __finitef
+[eva] Done for function __finitef
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:58.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:59: assertion got status valid.
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:60.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:60.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:61: assertion got status valid.
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:62.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:63: assertion got status valid.
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:64.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:65: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -325,4 +360,5 @@
   fabsl_minus_one ∈ [-inf .. inf]
   fabsl_large ∈ [-inf .. inf]
   fabsl_ld_top ∈ [-inf .. inf]
+  r ∈ {0}
   __retres ∈ {0}