Updates test oracles.

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

 directory	file	line	function	property kind	status	property
-FRAMAC_SHARE/libc	math.h	526	pow	precondition	Unknown	finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc	math.h	522	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

@@ -40,7 +40,7 @@
    unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
    wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call); 
   
-  Undefined functions (382)
+  Undefined functions (384)
   =========================
    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);
@@ -61,64 +61,64 @@
    __builtin_umull_overflow (0 call); __builtin_umulll_overflow (0 call);
    __builtin_usub_overflow (0 call); __builtin_usubl_overflow (0 call);
    __builtin_usubll_overflow (0 call); __fc_fpclassify (0 call);
-   __fc_fpclassifyf (0 call); __va_fcntl_flock (0 call);
-   __va_fcntl_int (0 call); __va_fcntl_void (0 call); __va_ioctl_int (0 call);
-   __va_ioctl_ptr (0 call); __va_ioctl_void (0 call);
-   __va_open_mode_t (0 call); __va_open_void (0 call);
-   __va_openat_mode_t (0 call); __va_openat_void (0 call); _exit (0 call);
-   abort (0 call); accept (0 call); access (0 call); acos (0 call);
-   acosf (0 call); acosh (0 call); acoshf (0 call); acoshl (0 call);
-   acosl (0 call); alloca (0 call); asin (0 call); asinf (0 call);
-   asinl (0 call); at_quick_exit (0 call); atan (0 call); atan2 (0 call);
-   atan2f (0 call); atanf (0 call); atanl (0 call); atexit (0 call);
-   atof (0 call); atol (0 call); atoll (0 call); basename (0 call);
-   bind (0 call); bsearch (0 call); bzero (0 call); ceil (0 call);
-   ceilf (0 call); ceill (0 call); chdir (0 call); chown (0 call);
-   chroot (0 call); clearerr (0 call); clearerr_unlocked (0 call);
-   clock (0 call); clock_gettime (0 call); clock_nanosleep (0 call);
-   close (0 call); closedir (0 call); closelog (0 call); connect (0 call);
-   cos (0 call); cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
-   difftime (0 call); dirname (0 call); div (0 call); drand48 (0 call);
-   dup (0 call); dup2 (0 call); erand48 (0 call); execl (0 call);
-   execle (0 call); execlp (0 call); execv (0 call); execve (0 call);
-   execvp (0 call); exit (0 call); exp (0 call); expf (0 call); fabsl (0 call);
-   fclose (0 call); fcntl (0 call); fdopen (0 call); feof (2 calls);
-   feof_unlocked (0 call); ferror (2 calls); ferror_unlocked (0 call);
-   fflush (0 call); fgetc (1 call); fgetpos (0 call); fgets (0 call);
-   fgetws (0 call); fileno (0 call); fileno_unlocked (0 call); flock (0 call);
-   flockfile (0 call); floor (0 call); floorf (0 call); floorl (0 call);
-   fmod (0 call); fmodf (0 call); fopen (0 call); fork (0 call);
-   fputc (0 call); fputs (0 call); fread (0 call); free (1 call);
-   freeaddrinfo (0 call); freopen (0 call); fseek (0 call); fsetpos (0 call);
-   ftell (0 call); ftrylockfile (0 call); funlockfile (0 call);
-   fwrite (0 call); gai_strerror (0 call); getc (0 call);
-   getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
-   getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
-   gethostname (0 call); getitimer (0 call); getopt (0 call);
-   getopt_long (0 call); getopt_long_only (0 call); getpgid (0 call);
-   getpgrp (0 call); getpid (0 call); getppid (0 call); getpriority (0 call);
-   getpwnam (0 call); getpwuid (0 call); getresgid (0 call);
-   getresuid (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
-   getsid (0 call); getsockopt (0 call); gettimeofday (0 call);
-   getuid (0 call); gmtime (0 call); htonl (0 call); htons (0 call);
-   iconv (0 call); iconv_close (0 call); iconv_open (0 call);
-   inet_addr (2 calls); inet_ntoa (0 call); inet_ntop (0 call);
-   inet_pton (0 call); isascii (0 call); isatty (0 call); jrand48 (0 call);
-   kill (0 call); killpg (0 call); labs (0 call); lcong48 (0 call);
-   ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
-   localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
-   log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
-   logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
-   lseek (0 call); malloc (7 calls); mblen (0 call); mbstowcs (0 call);
-   mbtowc (0 call); mkdir (0 call); mkstemp (0 call); mktime (0 call);
-   mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
-   nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
-   open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
-   pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
-   poll (0 call); popen (0 call); pow (0 call); powf (0 call);
-   pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
-   pthread_cond_init (0 call); pthread_cond_wait (0 call);
-   pthread_create (0 call); pthread_join (0 call);
+   __fc_fpclassifyf (0 call); __fc_infinity (0 call); __fc_nan (0 call);
+   __va_fcntl_flock (0 call); __va_fcntl_int (0 call);
+   __va_fcntl_void (0 call); __va_ioctl_int (0 call); __va_ioctl_ptr (0 call);
+   __va_ioctl_void (0 call); __va_open_mode_t (0 call);
+   __va_open_void (0 call); __va_openat_mode_t (0 call);
+   __va_openat_void (0 call); _exit (0 call); abort (0 call); accept (0 call);
+   access (0 call); acos (0 call); acosf (0 call); acosh (0 call);
+   acoshf (0 call); acoshl (0 call); acosl (0 call); alloca (0 call);
+   asin (0 call); asinf (0 call); asinl (0 call); at_quick_exit (0 call);
+   atan (0 call); atan2 (0 call); atan2f (0 call); atanf (0 call);
+   atanl (0 call); atexit (0 call); atof (0 call); atol (0 call);
+   atoll (0 call); basename (0 call); bind (0 call); bsearch (0 call);
+   bzero (0 call); ceil (0 call); ceilf (0 call); ceill (0 call);
+   chdir (0 call); chown (0 call); chroot (0 call); clearerr (0 call);
+   clearerr_unlocked (0 call); clock (0 call); clock_gettime (0 call);
+   clock_nanosleep (0 call); close (0 call); closedir (0 call);
+   closelog (0 call); connect (0 call); cos (0 call); cosf (0 call);
+   cosl (0 call); creat (0 call); ctime (0 call); difftime (0 call);
+   dirname (0 call); div (0 call); drand48 (0 call); dup (0 call);
+   dup2 (0 call); erand48 (0 call); execl (0 call); execle (0 call);
+   execlp (0 call); execv (0 call); execve (0 call); execvp (0 call);
+   exit (0 call); exp (0 call); expf (0 call); fabsl (0 call); fclose (0 call);
+   fcntl (0 call); fdopen (0 call); feof (2 calls); feof_unlocked (0 call);
+   ferror (2 calls); ferror_unlocked (0 call); fflush (0 call); fgetc (1 call);
+   fgetpos (0 call); fgets (0 call); fgetws (0 call); fileno (0 call);
+   fileno_unlocked (0 call); flock (0 call); flockfile (0 call);
+   floor (0 call); floorf (0 call); floorl (0 call); fmod (0 call);
+   fmodf (0 call); fopen (0 call); fork (0 call); fputc (0 call);
+   fputs (0 call); fread (0 call); free (1 call); freeaddrinfo (0 call);
+   freopen (0 call); fseek (0 call); fsetpos (0 call); ftell (0 call);
+   ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call);
+   gai_strerror (0 call); getc (0 call); getc_unlocked (0 call);
+   getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
+   getegid (0 call); geteuid (0 call); getgid (0 call); gethostname (0 call);
+   getitimer (0 call); getopt (0 call); getopt_long (0 call);
+   getopt_long_only (0 call); getpgid (0 call); getpgrp (0 call);
+   getpid (0 call); getppid (0 call); getpriority (0 call); getpwnam (0 call);
+   getpwuid (0 call); getresgid (0 call); getresuid (0 call);
+   getrlimit (0 call); getrusage (0 call); gets (0 call); getsid (0 call);
+   getsockopt (0 call); gettimeofday (0 call); getuid (0 call);
+   gmtime (0 call); htonl (0 call); htons (0 call); iconv (0 call);
+   iconv_close (0 call); iconv_open (0 call); inet_addr (2 calls);
+   inet_ntoa (0 call); inet_ntop (0 call); inet_pton (0 call);
+   isascii (0 call); isatty (0 call); jrand48 (0 call); kill (0 call);
+   killpg (0 call); labs (0 call); lcong48 (0 call); ldiv (0 call);
+   listen (0 call); llabs (0 call); lldiv (0 call); localtime (0 call);
+   log (0 call); log10 (0 call); log10f (0 call); log10l (0 call);
+   log2 (0 call); log2f (0 call); log2l (0 call); logf (0 call); logl (0 call);
+   longjmp (0 call); lrand48 (0 call); lseek (0 call); malloc (7 calls);
+   mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call);
+   mkstemp (0 call); mktime (0 call); mrand48 (0 call); nan (0 call);
+   nanf (0 call); nanl (0 call); nanosleep (0 call); nrand48 (0 call);
+   ntohl (0 call); ntohs (0 call); open (0 call); openat (0 call);
+   opendir (0 call); openlog (0 call); pathconf (0 call); pclose (0 call);
+   perror (0 call); pipe (0 call); poll (0 call); popen (0 call); pow (0 call);
+   powf (0 call); pthread_cond_broadcast (0 call);
+   pthread_cond_destroy (0 call); pthread_cond_init (0 call);
+   pthread_cond_wait (0 call); pthread_create (0 call); pthread_join (0 call);
    pthread_mutex_destroy (0 call); pthread_mutex_init (0 call);
    pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call); putc (0 call);
    putc_unlocked (0 call); putchar (0 call); putchar_unlocked (0 call);
@@ -178,7 +178,7 @@
   Goto = 89
   Assignment = 438
   Exit point = 82
-  Function = 464
+  Function = 466
   Function call = 89
   Pointer dereferencing = 158
   Cyclomatic complexity = 286

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

@@ -3379,6 +3379,23 @@ int __finitef(float f);
 
 int __finite(double d);
 
+/*@ logic float __fc_infinity(ℤ x) = \plus_infinity;
+ */
+/*@ logic float __fc_nan(ℤ x) = \NaN;
+
+*/
+/*@ ensures result_is_infinity: \is_plus_infinity(\result);
+    assigns \result;
+    assigns \result \from \nothing;
+ */
+extern float __fc_infinity(int x);
+
+/*@ ensures result_is_nan: \is_NaN(\result);
+    assigns \result;
+    assigns \result \from \nothing;
+ */
+extern float __fc_nan(int x);
+
 /*@ requires finite_arg: \is_finite(x);
     ensures res_finite: \is_finite(\result);
     ensures positive_result: \result ≥ 0.;