update test oracles

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	1221	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/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,81 @@ extern float sinf(float x);
  */
 extern long double sinl(long double x);
 
+/*@ requires ¬(infinite_arg: \is_infinite(x));
+    requires ¬(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 result_not_nan: ¬\is_NaN(\result);
+      ensures maybe_error: __fc_errno ≡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    complete behaviors finite_non_zero, zero;
+    disjoint behaviors finite_non_zero, zero;
+ */
+extern double tan(double x);
+
+/*@ requires ¬(infinite_arg: \is_infinite(x));
+    requires ¬(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 result_not_nan: ¬\is_NaN(\result);
+      ensures maybe_error: __fc_errno ≡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    complete behaviors finite_non_zero, zero;
+    disjoint behaviors finite_non_zero, zero;
+ */
+extern float tanf(float x);
+
+/*@ requires ¬(infinite_arg: \is_infinite(x));
+    requires ¬(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 result_not_nan: ¬\is_NaN(\result);
+      ensures maybe_error: __fc_errno ≡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    complete behaviors finite_non_zero, zero;
+    disjoint behaviors finite_non_zero, zero;
+ */
+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);