Merge branch 'feature/andre/libc-tan' into 'master'

[Libc] add specs for tan* functions

See merge request frama-c/frama-c!3190

share/libc/math.h

@@ -467,8 +467,68 @@ extern float sinf(float x);
 */
 extern long double sinl(long double x);
 
+/* Note: the specs of tan/tanf below assume that, for a finite x,
+ *       the result is always finite. This is _not_ guaranteed by the standard,
+ *       but testing with the GNU libc, plus some mathematical arguments
+ *       (see https://stackoverflow.com/questions/67482420) indicate that,
+ *       in practice, the result is _never_ infinite.
+ *       If you know of any implementations in which a finite argument
+ *       produces an infinite result, please inform us.
+ */
+/*@
+  assigns errno, \result \from x;
+  behavior zero:
+    assumes zero_arg: \is_finite(x) && x == 0.;
+    assigns \result \from x;
+    ensures zero_res: \is_finite(\result) && \result == x;
+    ensures no_error: errno == \old(errno);
+  behavior finite_non_zero:
+    assumes finite_arg: \is_finite(x) && x != 0.;
+    ensures finite_result: \is_finite(\result);
+    ensures maybe_error: errno == \old(errno) || errno == ERANGE;
+  behavior infinity:
+    assumes infinite_arg: \is_infinite(x);
+    ensures nan_result: \is_NaN(\result);
+    ensures errno_set: errno == EDOM;
+  behavior nan:
+    assumes nan_arg: \is_NaN(x);
+    assigns \result \from x;
+    ensures nan_result: \is_NaN(\result);
+    ensures no_error: errno == \old(errno);
+  complete behaviors;
+  disjoint behaviors;
+*/
 extern double tan(double x);
+
+/*@
+  assigns errno, \result \from x;
+  behavior zero:
+    assumes zero_arg: \is_finite(x) && x == 0.;
+    assigns \result \from x;
+    ensures zero_res: \is_finite(\result) && \result == x;
+    ensures no_error: errno == \old(errno);
+  behavior finite_non_zero:
+    assumes finite_arg: \is_finite(x) && x != 0.;
+    ensures finite_result: \is_finite(\result);
+    ensures maybe_error: errno == \old(errno) || errno == ERANGE;
+  behavior infinity:
+    assumes infinite_arg: \is_infinite(x);
+    ensures nan_result: \is_NaN(\result);
+    ensures errno_set: errno == EDOM;
+  behavior nan:
+    assumes nan_arg: \is_NaN(x);
+    assigns \result \from x;
+    ensures nan_result: \is_NaN(\result);
+    ensures no_error: errno == \old(errno);
+  complete behaviors;
+  disjoint behaviors;
+*/
 extern float tanf(float x);
+
+/*@
+  assigns errno, \result \from x;
+  ensures maybe_error: errno == \old(errno) || errno == EDOM || errno == ERANGE;
+*/
 extern long double tanl(long double x);
 
 /*@

src/plugins/report/tests/report/oracle/csv.csv

 directory	file	line	function	property kind	status	property
-FRAMAC_SHARE/libc	math.h	1147	pow	precondition	Unknown	finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc	math.h	1207	pow	precondition	Unknown	finite_logic_res: \is_finite(pow(x, y))
 tests/report	csv.c	11	main1	signed_overflow	Unknown	-2147483648 ≤ x * x
 tests/report	csv.c	11	main1	signed_overflow	Unknown	x * x ≤ 2147483647
 tests/report	csv.c	12	main1	index_bound	Unknown	0 ≤ x

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\"" #"-eva-slevel 4"
+   STDOPT: #"-warn-special-float nan" #"-cpp-extra-args=\"-DNONFINITE -DNONAN\"" #"-eva-slevel 4"
+   STDOPT: #"-eva-slevel 4"
 */
 #include <math.h>
 const double pi = 3.14159265358979323846264338327950288;
@@ -21,16 +23,22 @@ const double one = 1.0;
 const double minus_one = -1.0;
 const double large = 1e38;
 #ifdef NONFINITE
-const double huge_val = HUGE_VAL;
-const float huge_valf = HUGE_VALF;
-const long double huge_vall = HUGE_VALL;
+const float f_pos_inf = HUGE_VALF;
+const double pos_inf = HUGE_VAL;
+const long double ld_pos_inf = HUGE_VALL;
+const float f_neg_inf = -HUGE_VALF;
+const double neg_inf = -HUGE_VAL;
+const long double ld_neg_inf = -HUGE_VALL;
 const float infinity = INFINITY;
 #endif
 const double fp_ilogb0 = FP_ILOGB0;
 const double fp_ilogbnan = FP_ILOGBNAN;
 volatile int int_top;
 
-#define TEST_VAL_CONST(type,f,cst) type f##_##cst = f(cst)
+volatile int nondet;
+
+#define TEST_VAL_CONST(type,f,cst) \
+  if (nondet) { type f##_##cst = f(cst); }
 #define TEST_FUN_CONSTS(type,f,prefix)          \
   TEST_VAL_CONST(type,f,prefix##pi);            \
   TEST_VAL_CONST(type,f,prefix##half_pi);       \
@@ -45,25 +53,39 @@ volatile int int_top;
 // tests functions with 2 arguments, where the first one changes,
 // but the second one is fixed by the caller.
 // suffix prevents redeclaring variables with the same name
-#define TEST_VAL2_FST_CONST(type,f,cst,snd_arg,suffix) type f##_##cst##suffix = f(cst,snd_arg)
-#define TEST_FUN2_FST_CONSTS(type,f,prefix,snd_arg,suffix)    \
-  TEST_VAL2_FST_CONST(type,f,prefix##pi,snd_arg,suffix);            \
-  TEST_VAL2_FST_CONST(type,f,prefix##half_pi,snd_arg,suffix);  \
-  TEST_VAL2_FST_CONST(type,f,prefix##e,snd_arg,suffix);        \
-  TEST_VAL2_FST_CONST(type,f,zero,snd_arg,suffix);             \
-  TEST_VAL2_FST_CONST(type,f,minus_zero,snd_arg,suffix);       \
-  TEST_VAL2_FST_CONST(type,f,one,snd_arg,suffix);              \
-  TEST_VAL2_FST_CONST(type,f,minus_one,snd_arg,suffix);        \
-  TEST_VAL2_FST_CONST(type,f,large,snd_arg,suffix);            \
+#define TEST_VAL2_FST_CONST(type,f,cst,snd_arg,suffix)  \
+  if (nondet) { type f##_##cst##suffix = f(cst,snd_arg); }
+#define TEST_FUN2_FST_CONSTS(type,f,prefix,snd_arg,suffix)      \
+  TEST_VAL2_FST_CONST(type,f,prefix##pi,snd_arg,suffix);        \
+  TEST_VAL2_FST_CONST(type,f,prefix##half_pi,snd_arg,suffix);   \
+  TEST_VAL2_FST_CONST(type,f,prefix##e,snd_arg,suffix);         \
+  TEST_VAL2_FST_CONST(type,f,zero,snd_arg,suffix);              \
+  TEST_VAL2_FST_CONST(type,f,minus_zero,snd_arg,suffix);        \
+  TEST_VAL2_FST_CONST(type,f,one,snd_arg,suffix);               \
+  TEST_VAL2_FST_CONST(type,f,minus_one,snd_arg,suffix);         \
+  TEST_VAL2_FST_CONST(type,f,large,snd_arg,suffix);      \
   TEST_VAL2_FST_CONST(type,f,prefix##top,snd_arg,suffix)
 
+#ifdef NONFINITE
+#define TEST_FUN_NONFINITE(type,f,prefix)     \
+  TEST_VAL_CONST(type,f,prefix##pos_inf);     \
+  TEST_VAL_CONST(type,f,prefix##neg_inf)
+#else
+#define TEST_FUN_NONFINITE(type,f,prefix)
+#endif
+
+#define TEST_FUN_ALL_PREC(fun)                  \
+  TEST_FUN_CONSTS(double,fun,);                 \
+  TEST_FUN_CONSTS(float,fun ## f,f_);           \
+  TEST_FUN_CONSTS(long double,fun ## l,ld_);    \
+  TEST_FUN_NONFINITE(double,fun,);              \
+  TEST_FUN_NONFINITE(float,fun ## f,f_);        \
+  TEST_FUN_NONFINITE(long double,fun ## l,ld_)
+
 int main() {
-  TEST_FUN_CONSTS(double,atan,);
-  TEST_FUN_CONSTS(float,atanf,f_);
-  TEST_FUN_CONSTS(long double,atanl,ld_);
-  TEST_FUN_CONSTS(double,fabs,);
-  TEST_FUN_CONSTS(float,fabsf,f_);
-  TEST_FUN_CONSTS(long double,fabsl,ld_);
+  TEST_FUN_ALL_PREC(atan);
+  TEST_FUN_ALL_PREC(fabs);
+  TEST_FUN_ALL_PREC(tan);
   int exponent;
   TEST_FUN2_FST_CONSTS(double,frexp,,&exponent,);
   TEST_FUN2_FST_CONSTS(float,frexpf,f_,&exponent,);
@@ -77,9 +99,9 @@ int main() {
   TEST_FUN2_FST_CONSTS(double,ldexp,,-5,_minus5);
   TEST_FUN2_FST_CONSTS(float,ldexpf,f_,-5,_minus5);
   //TEST_FUN2_FST_CONSTS(long double,ldexpl,ld_,-5,_minus5);
-  TEST_FUN2_FST_CONSTS(double,ldexp,,100000,_huge);
-  TEST_FUN2_FST_CONSTS(float,ldexpf,f_,100000,_huge);
-  //TEST_FUN2_FST_CONSTS(long double,ldexpl,ld_,100000,_huge);
+  TEST_FUN2_FST_CONSTS(double,ldexp,,100000,_pos_inf);
+  TEST_FUN2_FST_CONSTS(float,ldexpf,f_,100000,_pos_inf);
+  //TEST_FUN2_FST_CONSTS(long double,ldexpl,ld_,100000,_pos_inf);
 
 #ifdef NONFINITE
   int r;
@@ -89,11 +111,13 @@ int main() {
   //@ assert r;
   r = isfinite(0.0f);
   //@ assert r;
-  r = isfinite(huge_val);
+  r = isfinite(pos_inf);
   //@ assert !r;
   r = isfinite(-INFINITY);
   //@ assert !r;
+#ifndef NONAN
   r = isfinite(NAN);
+#endif
   //@ assert !r;
 #endif
 }

tests/libc/oracle/fc_libc.0.res.oracle

@@ -46,7 +46,7 @@
    wcslen (3 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (1 call);
    wmemset (0 call); 
   
-  Specified-only functions (423)
+  Specified-only functions (426)
   ==============================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
    Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -163,17 +163,18 @@
    strtok (0 call); strtok_r (0 call); strtol (0 call); strtold (0 call);
    strtoll (0 call); strtoul (0 call); strtoull (0 call); strxfrm (0 call);
    sync (0 call); sysconf (0 call); syslog (0 call); system (0 call);
-   tcflush (0 call); tcgetattr (0 call); tcsetattr (0 call); time (0 call);
-   times (0 call); tmpfile (0 call); tmpnam (0 call); trunc (0 call);
-   truncf (0 call); truncl (0 call); ttyname (0 call); tzset (0 call);
-   umask (0 call); uname (0 call); ungetc (0 call); unlink (0 call);
-   usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
-   vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
-   vsyslog (0 call); wait (0 call); waitpid (0 call); wcscasecmp (0 call);
-   wcschr (0 call); wcscmp (0 call); wcscspn (0 call); wcslcat (0 call);
-   wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call);
-   wcsspn (0 call); wcsstr (0 call); wcstombs (0 call); wctomb (0 call);
-   wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call); write (0 call); 
+   tan (0 call); tanf (0 call); tanl (0 call); tcflush (0 call);
+   tcgetattr (0 call); tcsetattr (0 call); time (0 call); times (0 call);
+   tmpfile (0 call); tmpnam (0 call); trunc (0 call); truncf (0 call);
+   truncl (0 call); ttyname (0 call); tzset (0 call); umask (0 call);
+   uname (0 call); ungetc (0 call); unlink (0 call); usleep (0 call);
+   utimes (0 call); vfprintf (0 call); vfscanf (0 call); vprintf (0 call);
+   vscanf (0 call); vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call);
+   wait (0 call); waitpid (0 call); wcscasecmp (0 call); wcschr (0 call);
+   wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
+   wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
+   wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
+   wmemcmp (0 call); wmemmove (0 call); write (0 call); 
   
   Undefined and unspecified functions (1)
   =======================================
@@ -202,7 +203,7 @@
   Goto = 112
   Assignment = 618
   Exit point = 99
-  Function = 523
+  Function = 526
   Function call = 141
   Pointer dereferencing = 249
   Cyclomatic complexity = 369

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

@@ -3758,6 +3758,64 @@ extern float sinf(float x);
  */
 extern long double sinl(long double x);
 
+/*@ requires not_infinity: ¬(infinite_arg: \is_infinite(x));
+    requires not_nan: ¬(nan_arg: \is_NaN(x));
+    assigns __fc_errno, \result;
+    assigns __fc_errno \from x;
+    assigns \result \from x;
+    
+    behavior zero:
+      assumes zero_arg: \is_finite(x) ∧ x ≡ 0.;
+      ensures zero_res: \is_finite(\result) ∧ \result ≡ \old(x);
+      ensures no_error: __fc_errno ≡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    behavior finite_non_zero:
+      assumes finite_arg: \is_finite(x) ∧ x ≢ 0.;
+      ensures finite_result: \is_finite(\result);
+      ensures
+        maybe_error: __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 34;
+    
+    complete behaviors finite_non_zero, zero;
+    disjoint behaviors finite_non_zero, zero;
+ */
+extern double tan(double x);
+
+/*@ requires not_infinity: ¬(infinite_arg: \is_infinite(x));
+    requires not_nan: ¬(nan_arg: \is_NaN(x));
+    assigns __fc_errno, \result;
+    assigns __fc_errno \from x;
+    assigns \result \from x;
+    
+    behavior zero:
+      assumes zero_arg: \is_finite(x) ∧ x ≡ 0.;
+      ensures zero_res: \is_finite(\result) ∧ \result ≡ \old(x);
+      ensures no_error: __fc_errno ≡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    behavior finite_non_zero:
+      assumes finite_arg: \is_finite(x) ∧ x ≢ 0.;
+      ensures finite_result: \is_finite(\result);
+      ensures
+        maybe_error: __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 34;
+    
+    complete behaviors finite_non_zero, zero;
+    disjoint behaviors finite_non_zero, zero;
+ */
+extern float tanf(float x);
+
+/*@ ensures
+      maybe_error:
+        __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 33 ∨
+        __fc_errno ≡ 34;
+    assigns __fc_errno, \result;
+    assigns __fc_errno \from x;
+    assigns \result \from x;
+ */
+extern long double tanl(long double x);
+
 /*@ requires in_domain: \is_finite(x) ∧ x ≥ 1;
     ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
     ensures no_error: __fc_errno ≡ \old(__fc_errno);