Merge branch 'fix/andre/libc-wchar' into 'master'

[Libc] Fix/improve several specifications

Closes #693

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

share/libc/__fc_machdep.h

@@ -99,6 +99,10 @@
 /* POSIX */
 #define __SSIZE_T int
 #define __SSIZE_MAX __FC_INT_MAX
+/* stdio.h */
+#ifndef __FC_L_tmpnam
+#define __FC_L_tmpnam 1024
+#endif
 /* stdint.h */
 #define __FC_PTRDIFF_MIN __FC_INT_MIN
 #define __FC_PTRDIFF_MAX __FC_INT_MAX
@@ -195,6 +199,10 @@
 /* POSIX */
 #define __SSIZE_T signed long
 #define __SSIZE_MAX __FC_LONG_MAX
+/* stdio.h */
+#ifndef __FC_L_tmpnam
+#define __FC_L_tmpnam 1024
+#endif
 /* stdint.h */
 #define __FC_PTRDIFF_MIN __FC_LONG_MIN
 #define __FC_PTRDIFF_MAX __FC_LONG_MAX
@@ -293,6 +301,10 @@
 /* POSIX */
 #define __SSIZE_T signed long
 #define __SSIZE_MAX __FC_LONG_MAX
+/* stdio.h */
+#ifndef __FC_L_tmpnam
+#define __FC_L_tmpnam 1024
+#endif
 /* stdint.h */
 #define __FC_PTRDIFF_MIN __FC_LONG_MIN
 #define __FC_PTRDIFF_MAX __FC_LONG_MAX
@@ -388,6 +400,10 @@
 /* POSIX */
 #define __SSIZE_T int
 #define __SSIZE_MAX __FC_INT_MAX
+/* stdio.h */
+#ifndef __FC_L_tmpnam
+#define __FC_L_tmpnam 1024
+#endif
 /* stdint.h */
 #define __FC_PTRDIFF_MIN __FC_INT_MIN
 #define __FC_PTRDIFF_MAX __FC_INT_MAX
@@ -558,6 +574,10 @@
 
 /* POSIX */
 #define __SSIZE_T signed long long
+/* stdio.h */
+#ifndef __FC_L_tmpnam
+#define __FC_L_tmpnam 20
+#endif
 /* stdint.h */
 #define __FC_WCHAR_MIN 0
 #define __FC_WCHAR_MAX __FC_USHRT_MAX

share/libc/__fc_string_axiomatic.h

@@ -171,6 +171,21 @@ __BEGIN_DECLS
   @ }
   @*/
 
+/*@ axiomatic WMemChr {
+  @ logic 𝔹 wmemchr{L}(wchar_t *s, wchar_t c, ℤ n)
+  @   reads s[0..n - 1];
+  @ // Returns [true] iff wide char array [s] contains wide character [c]
+  @
+  @ logic ℤ wmemchr_off{L}(wchar_t *s, wchar_t c, ℤ n)
+  @   reads s[0..n - 1];
+  @ // Returns the offset at which [c] appears in [s].
+  @
+  @ axiom wmemchr_def{L}:
+  @   \forall wchar_t *s; \forall wchar_t c; \forall ℤ n;
+  @      wmemchr(s,c,n) <==> \exists int i; 0 <= i < n && s[i] == c;
+  @ }
+  @*/
+
 /*@ axiomatic WcsLen {
   @ logic ℤ wcslen{L}(wchar_t *s)
   @   reads s[0..];

share/libc/stdio.h

@@ -44,6 +44,9 @@ __PUSH_FC_STDLIB
 #define BUFSIZ __FC_BUFSIZ
 #define FOPEN_MAX __FC_FOPEN_MAX
 #define FILENAME_MAX __FC_FILENAME_MAX
+#ifndef __FC_L_tmpnam
+#error machdep should have defined __FC_L_tmpnam!
+#endif
 #define L_tmpnam __FC_L_tmpnam
 
 #include "__fc_define_seek_macros.h"
@@ -67,10 +70,22 @@ extern FILE * __fc_stdout;
         non-interferent between them.
 */
 
-/*@ assigns \nothing; */ 
+/*@ // missing: assigns 'filesystem' \from filename[0..];
+    // missing: assigns errno one of several possible values
+  requires valid_filename: valid_read_string(filename);
+  assigns \result \from indirect:filename[0..strlen(filename)];
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
 extern int remove(const char *filename);
 
-/*@ assigns \nothing; */ 
+/*@ // missing: assigns 'filesystem' \from old_name[0..], new_name[0..];
+    // missing: assigns errno one of 21 different possible values
+  requires valid_old_name: valid_read_string(old_name);
+  requires valid_new_name: valid_read_string(new_name);
+  assigns \result \from indirect:old_name[0..strlen(old_name)],
+                        indirect:new_name[0..strlen(new_name)];
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
 extern int rename(const char *old_name, const char *new_name);
 
 FILE __fc_fopen[__FC_FOPEN_MAX];
@@ -83,33 +98,59 @@ FILE* const __fc_p_fopen = __fc_fopen;
 */
 extern FILE *tmpfile(void);
 
+char __fc_tmpnam[L_tmpnam];
+char * const __fc_p_tmpnam = __fc_tmpnam;
+
 /*@
-  assigns \result \from s[..]; 
-  assigns s[..] \from \nothing; 
-  // TODO: more precise behaviors from ISO C 7.19.4.4 
+  // Note: the tmpnam example in POSIX uses an array of size L_tmpnam+1
+  // missing: assigns __fc_p_tmpnam[0..L_tmpnam] \from 'PRNG and internal state'
+  // missing: if called more than TMP_MAX, behavior is implementation-defined
+  requires valid_s_or_null: s == \null || \valid(s+(0 .. L_tmpnam));
+  assigns __fc_p_tmpnam[0 .. L_tmpnam] \from __fc_p_tmpnam[0 .. L_tmpnam],
+                                             indirect:s;
+  assigns s[0 .. L_tmpnam] \from indirect:s, __fc_p_tmpnam[0 .. L_tmpnam];
+  assigns \result \from s, __fc_p_tmpnam;
+  ensures result_string_or_null: \result == \null || \result == s ||
+                                 \result == __fc_p_tmpnam;
 */
 extern char *tmpnam(char *s);
 
 /*@
+  // missing: assigns errno
   requires valid_stream: \valid(stream);
-  assigns \result \from stream, stream->__fc_FILE_id;
+  assigns \result \from indirect:stream, indirect:*stream;
   ensures result_zero_or_EOF: \result == 0 || \result == EOF;
-  // TODO: more precise behaviors from ISO C 7.19.4.1 
 */
 extern int fclose(FILE *stream);
 
 /*@
+  // missing: assigns errno
   requires null_or_valid_stream: stream == \null || \valid_read(stream);
-  assigns \result \from stream, stream->__fc_FILE_id;
   ensures result_zero_or_EOF: \result == 0 || \result == EOF;
-  // TODO: more precise behaviors from ISO C 7.19.5.2
+  assigns \result
+    \from indirect:*stream, indirect:__fc_fopen[0 .. __FC_FOPEN_MAX-1];
+  assigns *stream, __fc_fopen[0 .. __FC_FOPEN_MAX-1]
+    \from indirect:stream, *stream,
+          __fc_fopen[0 .. __FC_FOPEN_MAX-1]; // may flush ALL open streams
+  behavior flush_all:
+    assumes all_streams: stream == \null;
+    assigns __fc_fopen[0 .. __FC_FOPEN_MAX-1]
+      \from __fc_fopen[0 .. __FC_FOPEN_MAX-1]; // flush ALL open streams
+    assigns \result \from indirect:__fc_fopen[0 .. __FC_FOPEN_MAX-1];
+  behavior flush_stream:
+    assumes single_stream: stream != \null;
+    assigns *stream \from *stream;
+    assigns \result \from indirect:*stream;
+  complete behaviors;
+  disjoint behaviors;
  */
 extern int fflush(FILE *stream);
 
 /*@
   requires valid_filename: valid_read_string(filename);
   requires valid_mode: valid_read_string(mode);
-  assigns \result \from indirect:filename[..], indirect:mode[..], __fc_p_fopen;
+  assigns \result \from indirect:filename[0..strlen(filename)],
+                        indirect:mode[0..strlen(mode)], __fc_p_fopen;
   ensures result_null_or_valid_fd:
     \result==\null || (\subset(\result,&__fc_fopen[0 .. __FC_FOPEN_MAX-1])) ;
 */ 
@@ -118,8 +159,9 @@ extern FILE *fopen(const char * restrict filename,
 
 /*@
   requires valid_mode: valid_read_string(mode);
-  assigns \result, __fc_fopen[fd] \from indirect:fd, indirect:mode[0..],
-    indirect:__fc_fopen[fd], __fc_p_fopen;
+  assigns \result, __fc_fopen[fd] \from indirect:fd,
+                                        indirect:mode[0..strlen(mode)],
+                                        indirect:__fc_fopen[fd], __fc_p_fopen;
   ensures result_null_or_valid_fd:
     \result == \null || (\subset(\result,&__fc_fopen[0 .. __FC_FOPEN_MAX-1])) ;
  */
@@ -222,55 +264,97 @@ extern int fgetc(FILE *stream);
 
 /*@
   requires valid_stream: \valid(stream);
-  assigns s[0..size] \from indirect:size, indirect:*stream;
+  requires room_s: \valid(s+(0..size-1));
+  assigns s[0..size-1] \from indirect:size, indirect:*stream;
   assigns \result \from s, indirect:size, indirect:*stream;
   ensures result_null_or_same: \result == \null || \result == s;
+  ensures initialization:at_least_one:\result != \null ==> \initialized(&s[0]);
+          // the return value does not tell how many characters were written,
+          // so we can only ensure the first one was initialized
   ensures terminated_string_on_success:
     \result != \null ==> valid_string(s);
  */
 extern char *fgets(char * restrict s, int size,
     FILE * restrict stream);
 
-/*@ assigns *stream ; */
+/*@
+  requires valid_stream: \valid(stream);
+  assigns *stream \from c, *stream;
+  assigns \result \from indirect:*stream;
+*/
 extern int fputc(int c, FILE *stream);
 
-/*@ assigns *stream \from s[..]; */
+/*@
+  requires valid_string_s: valid_read_string(s);
+  assigns *stream \from s[0..strlen(s)], *stream;
+  assigns \result \from indirect:s[0..strlen(s)], indirect:*stream;
+*/
 extern int fputs(const char * restrict s,
      FILE * restrict stream);
 
-/*@ assigns \result,*stream \from *stream; */
+/*@
+  requires valid_stream: \valid(stream);
+  assigns \result, *stream \from *stream;
+*/
 extern int getc(FILE *stream);
 
-/*@ assigns \result \from *__fc_stdin ; */
+/*@
+  assigns \result, *__fc_stdin \from *__fc_stdin;
+*/
 extern int getchar(void);
 
+// Number of characters that will read by gets()
+/*@
+  axiomatic GetsLength {
+    logic size_t gets_length{L} reads *__fc_stdin;
+  }
+*/
+
 /*@
-  assigns s[..] \from *__fc_stdin ;
-  assigns \result \from s, __fc_stdin;
+  requires room_s: \valid(s+(0..gets_length));
+  assigns s[0..gets_length] \from *__fc_stdin ;
+  assigns \result \from s, *__fc_stdin;
+  assigns *__fc_stdin \from *__fc_stdin;
   ensures result_null_or_same: \result == s || \result == \null;
  */
 extern char *gets(char *s);
 
-/*@ assigns *stream \from c; */
+/*@
+  requires valid_stream: \valid(stream);
+  assigns *stream \from c, *stream;
+  assigns \result \from indirect:*stream;
+*/
 extern int putc(int c, FILE *stream);
 
-/*@ assigns *__fc_stdout \from c; */
+/*@
+  assigns *__fc_stdout \from c, *__fc_stdout;
+  assigns \result \from indirect:*__fc_stdout;
+*/
 extern int putchar(int c);
 
-/*@ assigns *__fc_stdout \from s[..]; */
+/*@
+  requires valid_string_s: valid_read_string(s);
+  assigns *__fc_stdout \from s[0..strlen(s)], *__fc_stdout;
+  assigns \result \from indirect:s[0..strlen(s)], indirect:*__fc_stdout;
+*/
 extern int puts(const char *s);
 
-/*@ assigns *stream \from c; */
+/*@
+  requires valid_stream: \valid(stream);
+  assigns *stream \from indirect:c;
+  assigns \result \from indirect:c, indirect:*stream;
+  ensures result_ok_or_error: \result == c || \result == EOF;
+*/
 extern int ungetc(int c, FILE *stream);
 
 /*@
   requires valid_ptr_block: \valid(((char*)ptr)+(0..(nmemb*size)-1));
   requires valid_stream: \valid(stream);
-  assigns *(((char*)ptr)+(0..(nmemb*size)-1)) \from size, nmemb, *stream;
-  assigns \result \from size, *stream;
+  assigns *(((char*)ptr)+(0..(nmemb*size)-1)), *stream
+    \from indirect:size, indirect:nmemb, indirect:*stream;
+  assigns \result \from size, indirect:*stream;
   ensures size_read: \result <= nmemb;
   ensures initialization: \initialized(((char*)ptr)+(0..(\result*size)-1));
-  //TODO: specify precise fields from struct FILE
 */
 extern size_t fread(void * restrict ptr,
      size_t size, size_t nmemb,
@@ -279,15 +363,20 @@ extern size_t fread(void * restrict ptr,
 /*@
   requires valid_ptr_block: \valid_read(((char*)ptr)+(0..(nmemb*size)-1));
   requires valid_stream: \valid(stream);
-  assigns *stream, \result \from *(((char*)ptr)+(0..(nmemb*size)-1));
+  assigns *stream, \result \from indirect:*(((char*)ptr)+(0..(nmemb*size)-1));
   ensures size_written: \result <= nmemb;
-  //TODO: specify precise fields from struct FILE
 */
 extern size_t fwrite(const void * restrict ptr,
      size_t size, size_t nmemb,
      FILE * restrict stream);
 
-/*@ assigns *pos \from *stream ; */
+/*@
+  requires valid_stream: \valid(stream);
+  requires valid_pos: \valid(pos);
+  requires initialization:pos: \initialized(pos);
+  assigns *pos \from indirect:*stream;
+  assigns \result \from indirect:*stream;
+ */
 extern int fgetpos(FILE * restrict stream,
      fpos_t * restrict pos);
 
@@ -300,7 +389,12 @@ extern int fgetpos(FILE * restrict stream,
 */
 extern int fseek(FILE *stream, long int offset, int whence);
 
-/*@ assigns *stream \from *pos; */
+/*@
+  requires valid_stream: \valid(stream);
+  requires valid_pos: \valid_read(pos);
+  requires initialization:pos: \initialized(pos);
+  assigns *stream \from *pos;
+*/
 extern int fsetpos(FILE *stream, const fpos_t *pos);
 
 /*@
@@ -311,50 +405,108 @@ extern int fsetpos(FILE *stream, const fpos_t *pos);
 */
 extern long int ftell(FILE *stream);
 
-/*@  assigns *stream \from \nothing; */
+/*@
+  requires valid_stream: \valid(stream);
+  assigns *stream \from \nothing;
+ */
 extern void rewind(FILE *stream);
 
-/*@  assigns *stream  \from \nothing; */
+/*@
+  requires valid_stream: \valid(stream);
+  assigns *stream  \from \nothing;
+ */
 extern void clearerr(FILE *stream);
 
-/*@ assigns \result \from *stream ;*/
+/*@
+  requires valid_stream: \valid(stream);
+  assigns \result \from indirect:*stream;
+*/
 extern int feof(FILE *stream);
 
-/*@ assigns \result \from *stream ;*/
+/*@
+  requires valid_stream: \valid(stream);
+  assigns \result \from indirect:*stream;
+*/
 extern int fileno(FILE *stream);
 
-/*@ assigns *stream \from \nothing ;*/
+/*@
+  requires valid_stream: \valid(stream);
+  assigns *stream \from \nothing;
+*/
 extern void flockfile(FILE *stream);
 
-/*@ assigns *stream \from \nothing ;*/
+/*@
+  requires valid_stream: \valid(stream);
+  assigns *stream \from \nothing;
+*/
 extern void funlockfile(FILE *stream);
 
-/*@ assigns \result,*stream \from \nothing ;*/
+/*@
+  requires valid_stream: \valid(stream);
+  assigns \result,*stream \from \nothing;
+*/
 extern int ftrylockfile(FILE *stream);
 
-/*@ assigns \result \from *stream ;*/
+/*@
+  requires valid_stream: \valid(stream);
+  assigns \result \from indirect:*stream;
+*/
 extern int ferror(FILE *stream);
 
-/*@ assigns __fc_stdout \from __fc_errno, s[..]; */
+/*@
+  requires valid_string_s: valid_read_string(s);
+  assigns __fc_stdout \from __fc_errno, s[0..strlen(s)];
+ */
 extern void perror(const char *s);
 
-/*@ assigns \result,*stream \from *stream; */
+/*@
+  requires valid_stream: \valid(stream);
+  assigns \result,*stream \from *stream;
+*/
 extern int getc_unlocked(FILE *stream);
-/*@ assigns \result \from *__fc_stdin ; */
+
+/*@
+  assigns \result \from *__fc_stdin;
+ */
 extern int getchar_unlocked(void);
-/*@ assigns *stream \from c; */
+
+/*@
+  requires valid_stream: \valid(stream);
+  assigns *stream \from c;
+  assigns \result \from indirect:*stream;
+*/
 extern int putc_unlocked(int c, FILE *stream);
-/*@ assigns *__fc_stdout \from c; */
+
+/*@
+  assigns *__fc_stdout \from c;
+  assigns \result \from indirect:*__fc_stdout;
+ */
 extern int putchar_unlocked(int c);
 
-/*@  assigns *stream  \from \nothing; */
+/*@
+  requires valid_stream: \valid(stream);
+  assigns *stream  \from \nothing;
+*/
 extern void clearerr_unlocked(FILE *stream);
-/*@ assigns \result \from *stream ;*/
+
+/*@
+  requires valid_stream: \valid(stream);
+  assigns \result \from indirect:*stream;
+*/
 extern int feof_unlocked(FILE *stream);
-/*@ assigns \result \from *stream ;*/
+
+/*@
+  requires valid_stream: \valid(stream);
+  assigns \result \from indirect:*stream;
+*/
 extern int ferror_unlocked(FILE *stream);
-/*@ assigns \result \from *stream ;*/
+
+/*@
+  requires valid_stream: \valid(stream);
+  assigns \result \from indirect:*stream;
+*/
 extern int fileno_unlocked(FILE *stream);
+
 extern int fflush_unlocked(FILE *stream);
 extern int fgetc_unlocked(FILE *stream);
 extern int fputc_unlocked(int c, FILE *stream);

share/libc/sys/resource.h

@@ -65,21 +65,27 @@ extern int getpriority(int which, id_t who);
 /*@ assigns \result \from which,who,prio; */
 extern int setpriority(int which, id_t who, int prio);
 
-/*@ assigns \result \from r;
-  @ assigns rl->rlim_cur \from r;
-  @ assigns rl->rlim_max \from r;
+/*@
+  requires valid_rlp: \valid(rlp);
+  assigns \result, *rlp \from resource;
 */
-extern int getrlimit(int r, struct rlimit *rl);
+extern int getrlimit(int resource, struct rlimit *rlp);
 
-/*@ assigns \result \from r;
-  @ assigns ru->ru_utime \from r;
-  @ assigns ru->ru_stime \from r;
+/*@
+  requires valid_r_usage: \valid(r_usage);
+  assigns *r_usage \from who;
+  assigns \result \from indirect:who;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
 */
-extern int getrusage(int r, struct rusage *ru);
+extern int getrusage(int who, struct rusage *r_usage);
 
-/*@ assigns \result \from r,rl->rlim_cur,rl->rlim_max;
+/*@
+  requires valid_rlp: \valid_read(rlp);
+  assigns *rlp \from resource;
+  assigns \result \from indirect:resource, indirect:*rlp;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
 */
-extern int setrlimit(int r, const struct rlimit * rl);
+extern int setrlimit(int resource, const struct rlimit *rlp);
 
 __END_DECLS
 __POP_FC_STDLIB

share/libc/sys/time.h

@@ -30,6 +30,7 @@ __BEGIN_DECLS
 #include "../__fc_define_suseconds_t.h"
 #include "../__fc_define_fd_set_t.h"
 #include "../__fc_define_timespec.h"
+#include "../__fc_string_axiomatic.h"
 struct timeval {
   time_t         tv_sec;
   suseconds_t    tv_usec;
@@ -44,7 +45,12 @@ struct timezone {
 //@ ghost volatile unsigned int __fc_time __attribute__((FRAMA_C_MODEL));
 //@ ghost extern int __fc_tz __attribute__((FRAMA_C_MODEL));
 
-/*@ assigns \result \from path[0..],times[0..1]; */
+/*@
+  requires valid_path: valid_read_string(path);
+  requires valid_times_or_null: \valid_read(times+(0..1)) || times == \null;
+  assigns \result \from indirect:path[0..strlen(path)],
+    indirect:times, indirect:times[0..1];
+*/
 extern int utimes(const char *path, const struct timeval times[2]);
 
 /*@ assigns tv->tv_sec, tv->tv_usec \from __fc_time;
@@ -83,10 +89,14 @@ extern int utimes(const char *path, const struct timeval times[2]);
   @*/
 extern int gettimeofday(struct timeval * restrict tv, void * restrict tz);
 
-/*@ assigns \result,__fc_time,__fc_tz 
-  @            \from      tv->tv_sec, tv->tv_usec,
-  @                       tz->tz_dsttime, tz->tz_minuteswest; 
-  @*/
+/*@
+  requires valid_tv_or_null: \valid_read(tv) || tv == \null;
+  requires valid_tz_or_null: \valid_read(tz) || tz == \null;
+  assigns __fc_time, __fc_tz \from tv->tv_sec, tv->tv_usec,
+                                   tz->tz_dsttime, tz->tz_minuteswest;
+  assigns \result \from indirect:*tv, indirect:*tz;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
 extern int settimeofday(const struct timeval *tv, const struct timezone *tz);
 
 #if (defined _POSIX_C_SOURCE && (_POSIX_C_SOURCE) >= 200112L) ||        \

share/libc/time.h

@@ -86,7 +86,11 @@ extern clock_t clock(void);
 /*@ assigns \result \from time1, time0; */
 extern double difftime(time_t time1, time_t time0);
 
-/*@ assigns *timeptr, \result \from *timeptr; */
+/*@
+  requires valid_timeptr: \valid(timeptr);
+  assigns *timeptr \from *timeptr;
+  assigns \result \from indirect:*timeptr;
+ */
 extern time_t mktime(struct tm *timeptr);
 
 /*@
@@ -122,14 +126,18 @@ extern char *ctime(const time_t *timer);
 struct tm __fc_time_tm;
 struct tm * const  __fc_p_time_tm = &__fc_time_tm;
 
-/*@ assigns \result \from __fc_p_time_tm;
+/*@
+  requires valid_timer: \valid_read(timer);
+  assigns \result \from __fc_p_time_tm;
   assigns __fc_time_tm \from *timer;
   ensures result_null_or_internal_tm:
     \result == &__fc_time_tm || \result == \null ;
 */
 extern struct tm *gmtime(const time_t *timer);
 
-/*@ assigns \result \from __fc_p_time_tm;
+/*@
+  requires valid_timer: \valid_read(timer);
+  assigns \result \from __fc_p_time_tm;
   assigns __fc_time_tm \from *timer;
   ensures result_null_or_internal_tm:
     \result == &__fc_time_tm || \result == \null;
@@ -290,7 +298,6 @@ extern int timer_getoverrun(timer_t);
 extern int timer_gettime(timer_t, struct itimerspec *);
 extern int timer_settime(timer_t, int, const struct itimerspec *restrict,
                          struct itimerspec *restrict);
-extern void tzset(void);
 
 extern int daylight;
 extern long timezone;

share/libc/unistd.h

@@ -985,6 +985,7 @@ extern long pathconf(char const *path, int name);
 extern int          pause(void);
 
 /*@
+  requires valid_pipefd: \valid(pipefd+(0..1));
   assigns pipefd[0..1] \from indirect:__fc_fds[0..];
   assigns \result \from indirect:__fc_fds[0..];
   ensures initialization:pipefd: \initialized(&pipefd[0..1]);
@@ -1100,6 +1101,7 @@ volatile char *__fc_p_ttyname = __fc_ttyname;
 
 /*@
   // missing: may assign to errno: EBADF, ENOTTY
+  requires valid_fildes: 0 <= fildes < __FC_MAX_OPEN_FILES;
   assigns \result \from __fc_p_ttyname, indirect:fildes;
   ensures result_name_or_null: \result == __fc_p_ttyname || \result == \null;
  */

share/libc/wchar.h

@@ -41,6 +41,8 @@ __PUSH_FC_STDLIB
 // ISO C requires the tag 'struct tm' (as declared in <time.h>) to be declared.
 #include "time.h"
 
+#include "string.h"
+
 __BEGIN_DECLS
 
 #ifndef WEOF
@@ -48,16 +50,35 @@ __BEGIN_DECLS
 #endif
 
 /*@
+  requires valid:
+    valid_read_or_empty((char*)s, (size_t)(sizeof(wchar_t)*n))
+    || \valid_read(((unsigned char*)s)+(0..wmemchr_off(s,c,n)));
+  @ requires initialization:
+        \initialized(s+(0..n - 1))
+     || \initialized(s+(0..wmemchr_off(s,c,n)));
+  @ requires danglingness:
+        non_escaping(s, (size_t)(sizeof(wchar_t)*n))
+     || non_escaping(s, (size_t)(sizeof(wchar_t)*(wmemchr_off(s,c,n)+1)));
   assigns \result \from s, indirect:s[0 .. n-1], indirect:c, indirect:n;
   ensures result_null_or_inside_s:
     \result == \null || \subset (\result, s+(0 .. n-1));
  */
 extern wchar_t * wmemchr(const wchar_t *s, wchar_t c, size_t n);
 
-/*@ assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n; */
+/*@
+  requires valid_s1: valid_read_or_empty(s1, (size_t)(sizeof(wchar_t)*n));
+  requires valid_s2: valid_read_or_empty(s2, (size_t)(sizeof(wchar_t)*n));
+  requires initialization:s1: \initialized(s1+(0..n-1));
+  requires initialization:s2: \initialized(s2+(0..n-1));
+  requires danglingness:s1: non_escaping(s1, (size_t)(sizeof(wchar_t)*n));
+  requires danglingness:s2: non_escaping(s2, (size_t)(sizeof(wchar_t)*n));
+  assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n;
+*/
 extern int wmemcmp(const wchar_t *s1, const wchar_t *s2, size_t n);
 
 /*@
+  requires valid_dest: valid_or_empty(dest, (size_t)(sizeof(wchar_t)*n));
+  requires valid_src: valid_read_or_empty(src, (size_t)(sizeof(wchar_t)*n));
   requires separation:dest:src: \separated(dest+(0 .. n-1), src+(0 .. n-1));
   assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from dest;
@@ -66,6 +87,8 @@ extern int wmemcmp(const wchar_t *s1, const wchar_t *s2, size_t n);
 extern wchar_t * wmemcpy(wchar_t *restrict dest, const wchar_t *restrict src, size_t n);
 
 /*@
+  requires valid_src: \valid_read(src+(0..n-1));
+  requires valid_dest: \valid(dest+(0..n-1));
   assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from dest;
   ensures result_ptr: \result == dest;
@@ -73,6 +96,7 @@ extern wchar_t * wmemcpy(wchar_t *restrict dest, const wchar_t *restrict src, si
 extern wchar_t * wmemmove(wchar_t *dest, const wchar_t *src, size_t n);
 
 /*@
+  requires valid_wcs: \valid(wcs+(0..n-1));
   assigns wcs[0 .. n-1] \from wc, indirect:n;
   assigns \result \from wcs;
   ensures result_ptr: \result == wcs;
@@ -82,6 +106,10 @@ extern wchar_t * wmemmove(wchar_t *dest, const wchar_t *src, size_t n);
 extern wchar_t * wmemset(wchar_t *wcs, wchar_t wc, size_t n);
 
 /*@
+  requires valid_wstring_src: valid_read_wstring(src);
+  requires valid_wstring_dest: valid_wstring(dest);
+  requires room_for_concatenation: \valid(dest+(wcslen(dest)..wcslen(dest)+wcslen(src)));
+  requires separation:\separated(dest+(0..wcslen(dest)+wcslen(src)),src+(0..wcslen(src)));
   assigns dest[0 .. ] \from dest[0 .. ], indirect:dest, src[0 .. ], indirect:src;
   assigns \result \from dest;
   ensures result_ptr: \result == dest;
@@ -96,21 +124,36 @@ extern wchar_t * wcscat(wchar_t *restrict dest, const wchar_t *restrict src);
 */
 extern wchar_t * wcschr(const wchar_t *wcs, wchar_t wc);
 
-/*@ assigns \result \from indirect:s1[0 .. ], indirect:s2[0 .. ]; */
+/*@
+  requires valid_wstring_s1: valid_read_wstring(s1); // over-strong
+  requires valid_wstring_s2: valid_read_wstring(s2); // over-strong
+  assigns \result \from indirect:s1[0 .. ], indirect:s2[0 .. ];
+*/
 extern int wcscmp(const wchar_t *s1, const wchar_t *s2);
 
 /*@
-  assigns dest[0 .. ] \from src[0 .. ], indirect:src, dest[0 .. ], indirect:dest;
+  requires valid_wstring_src: valid_read_wstring(src);
+  requires room_wstring: \valid(dest+(0 .. wcslen(src)));
+  requires separation:\separated(dest+(0..wcslen(src)),src+(0..wcslen(src)));
+  assigns dest[0 .. wcslen(src)] \from src[0 .. wcslen(src)], indirect:src;
   assigns \result \from dest;
   ensures result_ptr: \result == dest;
  */
 extern wchar_t * wcscpy(wchar_t *restrict dest, const wchar_t *restrict src);
 
-/*@ assigns \result \from indirect:wcs[0 .. ], indirect:accept[0 .. ]; */
+/*@
+  requires valid_wstring_wcs: valid_read_wstring(wcs);
+  requires valid_wstring_accept: valid_read_wstring(accept);
+  assigns \result \from indirect:wcs[0 .. ], indirect:accept[0 .. ];
+ */
 extern size_t wcscspn(const wchar_t *wcs, const wchar_t *accept);
 
 // wcslcat is a BSD extension (non-C99, non-POSIX)
 /*@
+  requires valid_nwstring_src: valid_read_nwstring(src, n);
+  requires valid_wstring_dest: valid_wstring(dest);
+  requires room_for_concatenation: \valid(dest+(wcslen(dest)..wcslen(dest)+\min(wcslen(src), n)));
+  requires separation:\separated(dest+(0..wcslen(dest)+wcslen(src)),src+(0..wcslen(src)));
   assigns dest[0 .. ] \from dest[0 .. ], indirect:dest, src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from indirect:dest[0 .. ], indirect:src[0 .. n-1], indirect:n;
 */
@@ -118,6 +161,8 @@ extern size_t wcslcat(wchar_t *restrict dest, const wchar_t *restrict src, size_
 
 // wcslcpy is a BSD extension (non-C99, non-POSIX)
 /*@
+  requires valid_wstring_src: valid_read_wstring(src);
+  requires room_nwstring: \valid(dest+(0 .. n));
   requires separation:dest:src: \separated(dest+(0 .. n-1), src+(0 .. n-1));
   assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from indirect:dest[0 .. n-1], indirect:dest,
@@ -125,29 +170,45 @@ extern size_t wcslcat(wchar_t *restrict dest, const wchar_t *restrict src, size_
  */
 extern size_t wcslcpy(wchar_t *dest, const wchar_t *src, size_t n);
 
-/*@ requires valid_string_s: valid_read_wstring(s);
-  assigns \result \from indirect:s[0 .. ]; */
+/*@
+  requires valid_string_s: valid_read_wstring(s);
+  assigns \result \from indirect:s[0 .. wcslen(s)];
+  ensures result_is_length: \result == wcslen(s);
+ */
 extern size_t wcslen(const wchar_t *s);
 
 /*@
+  requires valid_nwstring_src: valid_read_nwstring(src, n);
+  requires valid_wstring_dest: valid_wstring(dest);
+  requires room_for_concatenation: \valid(dest+(wcslen(dest)..wcslen(dest)+\min(wcslen(src), n)));
+  requires separation:\separated(dest+(0..wcslen(dest)+wcslen(src)),src+(0..wcslen(src)));
   assigns dest[0 .. ] \from dest[0 .. ], indirect:dest, src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from dest;
   ensures result_ptr: \result == dest;
 */
 extern wchar_t * wcsncat(wchar_t *restrict dest, const wchar_t *restrict src, size_t n);
 
-/*@ assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n; */
+/*@
+  requires valid_wstring_s1: valid_read_wstring(s1); // over-strong
+  requires valid_wstring_s2: valid_read_wstring(s2); // over-strong
+  assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n;
+*/
 extern int wcsncmp(const wchar_t *s1, const wchar_t *s2, size_t n);
 
 /*@
+  requires valid_wstring_src: valid_read_wstring(src);
+  requires room_nwstring: \valid(dest+(0 .. n-1));
   requires separation:dest:src: \separated(dest+(0 .. n-1), src+(0 .. n-1));
   assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from dest;
   ensures result_ptr: \result == dest;
+  ensures initialization: \initialized(dest+(0 .. n-1));
  */
 extern wchar_t * wcsncpy(wchar_t *restrict dest, const wchar_t *restrict src, size_t n);
 
 /*@
+  requires valid_wstring_wcs: valid_read_wstring(wcs);
+  requires valid_wstring_accept: valid_read_wstring(accept);
   assigns \result \from wcs, indirect:wcs[0 .. ], indirect:accept[0 .. ];
   ensures result_null_or_inside_wcs:
     \result == \null || \subset (\result, wcs+(0 .. ));
@@ -155,16 +216,24 @@ extern wchar_t * wcsncpy(wchar_t *restrict dest, const wchar_t *restrict src, si
 extern wchar_t * wcspbrk(const wchar_t *wcs, const wchar_t *accept);
 
 /*@
-  assigns \result \from wcs, indirect:wcs[0 .. ], indirect:wc;
+  requires valid_wstring_wcs: valid_read_wstring(wcs);
+  assigns \result \from wcs, indirect:wcs[0 .. wcslen(wcs)], indirect:wc;
   ensures result_null_or_inside_wcs:
     \result == \null || \subset (\result, wcs+(0 .. ));
  */
 extern wchar_t * wcsrchr(const wchar_t *wcs, wchar_t wc);
 
-/*@ assigns \result \from indirect:wcs[0 .. ], indirect:accept[0 .. ]; */
+/*@
+  requires valid_wstring_wcs: valid_read_wstring(wcs);
+  requires valid_wstring_accept: valid_read_wstring(accept);
+  assigns \result \from indirect:wcs[0 .. wcslen(wcs)],
+                        indirect:accept[0 .. wcslen(accept)];
+*/
 extern size_t wcsspn(const wchar_t *wcs, const wchar_t *accept);
 
 /*@
+  requires valid_wstring_haystack: valid_read_wstring(haystack);
+  requires valid_wstring_needle: valid_read_wstring(needle);
   assigns \result \from haystack, indirect:haystack[0 .. ], indirect:needle[0 .. ];
   ensures result_null_or_inside_haystack:
     \result == \null || \subset (\result, haystack+(0 .. ));
@@ -172,8 +241,9 @@ extern size_t wcsspn(const wchar_t *wcs, const wchar_t *accept);
 extern wchar_t * wcsstr(const wchar_t *haystack, const wchar_t *needle);
 
 /*@
+  requires room_nwstring: \valid(ws+(0..n-1));
   requires valid_stream: \valid(stream);
-  assigns ws[0..n] \from indirect:n, indirect:*stream;
+  assigns ws[0..n-1] \from indirect:n, indirect:*stream;
   assigns \result \from ws, indirect:n, indirect:*stream;
   ensures result_null_or_same: \result == \null || \result == ws;
   ensures terminated_string_on_success:

src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/erroneous/printf.c:8: Warning: Multiple usage of flag '-'.
 [variadic] tests/erroneous/printf.c:8: Warning: 

src/plugins/variadic/tests/known/oracle/printf.res.oracle

-[variadic] FRAMAC_SHARE/libc/wchar.h:195: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:265: 
   Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:197: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:267: 
   Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:199: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:269: 
   Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:202: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
   Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:204: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
   Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:206: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
   Declaration of variadic function swscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/printf.c:37: 
   Translating call to printf to a call to the specialized version printf_va_1.
@@ -162,6 +162,8 @@
 #include "stdio.c"
 #include "stdio.h"
 #include "stdlib.h"
+#include "string.h"
+#include "strings.h"
 #include "time.h"
 #include "wchar.h"
 /*@ requires valid_read_string(format);

src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/printf_garbled_mix.c:8: 
   Variadic builtin Frama_C_show_each_nb_printed left untransformed.

src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/printf_wrong_arity.c:8: 
   Translating call to printf to a call to the specialized version printf_va_1.

src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/printf_wrong_pointers.c:14: 
   Translating call to printf to a call to the specialized version printf_va_1.

src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/printf_wrong_types.c:18: 
   Translating call to printf to a call to the specialized version printf_va_1.
@@ -410,21 +410,21 @@ int main(void)
 }
 
 
-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/printf_wrong_types.c:18: 
   Translating call to printf to a call to the specialized version printf_va_1.

src/plugins/variadic/tests/known/oracle/scanf.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/scanf.c:7: 
   Translating call to scanf to a call to the specialized version scanf_va_1.

src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/scanf_loop.c:6: 
   Translating call to scanf to a call to the specialized version scanf_va_1.

src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/scanf_wrong.c:8: 
   Translating call to scanf to a call to the specialized version scanf_va_1.

src/plugins/variadic/tests/known/oracle/snprintf.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/snprintf.c:12: 
   Translating call to snprintf to a call to the specialized version snprintf_va_1.

src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/stdio_print.c:9: Warning: 
   Call to function fprintf with non-static format argument:

src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle

-[variadic] FRAMAC_SHARE/libc/stdio.h:165: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:167: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:169: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
   Declaration of variadic function printf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:170: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
   Declaration of variadic function scanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:171: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:173: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:175: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/stdio_scan.c:10: Warning: 
   Call to function fscanf with non-static format argument: