[Libc] more fixes after review

share/libc/stdio.h

@@ -104,6 +104,7 @@ char * const __fc_p_tmpnam = __fc_tmpnam;
 /*@
   // 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;
@@ -285,7 +286,7 @@ extern int fputc(int c, FILE *stream);
 
 /*@
   requires valid_string_s: valid_read_string(s);
-  assigns *stream \from s[0..strlen(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,
@@ -320,20 +321,20 @@ extern char *gets(char *s);
 
 /*@
   requires valid_stream: \valid(stream);
-  assigns *stream \from c;
+  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);
 
 /*@
   requires valid_string_s: valid_read_string(s);
-  assigns *__fc_stdout \from s[0..strlen(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);
@@ -349,7 +350,7 @@ 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))
+  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;

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

-[variadic] FRAMAC_SHARE/libc/stdio.h:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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

@@ -10,21 +10,21 @@
   Declaration of variadic function fwscanf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:276: 
   Declaration of variadic function swscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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.

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

-[variadic] FRAMAC_SHARE/libc/stdio.h:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[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:

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

@@ -10,21 +10,21 @@
   Declaration of variadic function fwscanf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:276: 
   Declaration of variadic function swscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/swprintf.c:12: 
   Translating call to swprintf to a call to the specialized version swprintf_va_1.

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

@@ -10,21 +10,21 @@
   Declaration of variadic function fwscanf.
 [variadic] FRAMAC_SHARE/libc/wchar.h:276: 
   Declaration of variadic function swscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:206: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:208: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
   Declaration of variadic function fscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:210: 
-  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:211: 
-  Declaration of variadic function scanf.
+  Declaration of variadic function printf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
   Declaration of variadic function snprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:214: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
   Declaration of variadic function sprintf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:216: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:520: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:521: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/wchar.c:11: 
   Translating call to wprintf to a call to the specialized version wprintf_va_1.

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

@@ -4668,7 +4668,7 @@ extern int fputc(int c, FILE *stream);
 
 /*@ requires valid_string_s: valid_read_string(s);
     assigns *stream, \result;
-    assigns *stream \from *(s + (0 .. strlen{Old}(s)));
+    assigns *stream \from *(s + (0 .. strlen{Old}(s))), *stream;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: *stream);
  */
@@ -4705,20 +4705,20 @@ extern char *gets(char *s);
 
 /*@ requires valid_stream: \valid(stream);
     assigns *stream, \result;
-    assigns *stream \from c;
+    assigns *stream \from c, *stream;
     assigns \result \from (indirect: *stream);
  */
 extern int putc(int c, FILE *stream);
 
 /*@ assigns *__fc_stdout, \result;
-    assigns *__fc_stdout \from c;
+    assigns *__fc_stdout \from c, *__fc_stdout;
     assigns \result \from (indirect: *__fc_stdout);
  */
 extern int putchar(int c);
 
 /*@ requires valid_string_s: valid_read_string(s);
     assigns *__fc_stdout, \result;
-    assigns *__fc_stdout \from *(s + (0 .. strlen{Old}(s)));
+    assigns *__fc_stdout \from *(s + (0 .. strlen{Old}(s))), *__fc_stdout;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))),
             (indirect: *__fc_stdout);
@@ -4739,9 +4739,11 @@ extern int ungetc(int c, FILE *stream);
     ensures
       initialization:
         \initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
-    assigns *((char *)ptr + (0 .. nmemb * size - 1)), \result;
+    assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream, \result;
     assigns *((char *)ptr + (0 .. nmemb * size - 1))
       \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+    assigns *stream
+      \from (indirect: size), (indirect: nmemb), (indirect: *stream);
     assigns \result \from size, (indirect: *stream);
  */
 extern size_t fread(void * __restrict ptr, size_t size, size_t nmemb,
@@ -7264,11 +7266,12 @@ extern int __va_openat_mode_t(int dirfd, char const *filename, int flags,
 /*@ ghost extern int __fc_tz __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@ requires valid_path: valid_read_string(path);
-    requires valid_times: \valid_read(times + (0 .. 1));
+    requires
+      valid_times_or_null: \valid_read(times + (0 .. 1)) ∨ times ≡ \null;
     assigns \result;
     assigns \result
       \from (indirect: *(path + (0 .. strlen{Old}(path)))),
-            (indirect: *(times + (0 .. 1)));
+            (indirect: times), (indirect: *(times + (0 .. 1)));
  */
 extern int utimes(char const *path, struct timeval const * /*[2]*/ times);