From 6664c43ff1ff928becc39ddb759ee1234c0eaea8 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 21 Oct 2019 17:55:20 +0200
Subject: [PATCH] [Libc] more fixes after review

---
 share/libc/stdio.h                            |  11 +-
 .../tests/erroneous/oracle/printf.res.oracle  |  16 +-
 .../tests/known/oracle/printf.res.oracle      |  16 +-
 .../oracle/printf_garbled_mix.res.oracle      |  16 +-
 .../oracle/printf_wrong_arity.res.oracle      |  16 +-
 .../oracle/printf_wrong_pointers.res.oracle   |  16 +-
 .../oracle/printf_wrong_types.res.oracle      |  32 +--
 .../tests/known/oracle/scanf.res.oracle       |  16 +-
 .../tests/known/oracle/scanf_loop.res.oracle  |  16 +-
 .../tests/known/oracle/scanf_wrong.res.oracle |  16 +-
 .../tests/known/oracle/snprintf.res.oracle    |  16 +-
 .../tests/known/oracle/stdio_print.res.oracle |  16 +-
 .../tests/known/oracle/stdio_scan.res.oracle  |  16 +-
 .../tests/known/oracle/swprintf.res.oracle    |  16 +-
 .../tests/known/oracle/wchar.res.oracle       |  16 +-
 tests/idct/oracle/ieee_1180_1990.res.oracle   | 270 +++++++++---------
 tests/libc/oracle/fc_libc.1.res.oracle        |  17 +-
 tests/rte/oracle/value_rte.res.oracle         | 254 ++++++++--------
 18 files changed, 402 insertions(+), 390 deletions(-)

diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index 4b731825a24..b571cce1e3e 100644
--- a/share/libc/stdio.h
+++ b/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;
diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index 9ba50c252e7..ebb217fac02 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
@@ -1,18 +1,18 @@
-[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: 
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 2086be710e5..83d6f21822e 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/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.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index c5e28901b42..ec9df06d3ed 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -1,18 +1,18 @@
-[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.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index 22ad4025e3c..f04220bcfaa 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -1,18 +1,18 @@
-[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.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
index c74bf8f3f6a..48af02448ee 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
@@ -1,18 +1,18 @@
-[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.
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index 139282aeba4..b720645e934 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -1,18 +1,18 @@
-[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.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
index 1f0511d9f6f..cd8ae9652f3 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
@@ -1,18 +1,18 @@
-[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.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
index f77f9482f09..db959e60948 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
@@ -1,18 +1,18 @@
-[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.
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
index 260805b698c..b468aea8aca 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
@@ -1,18 +1,18 @@
-[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.
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index f93ca2c4b32..2b2dd3e7684 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -1,18 +1,18 @@
-[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.
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
index bfab9888396..0cacefc0330 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -1,18 +1,18 @@
-[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:
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
index 9e98889dccb..671f5bf3f35 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -1,18 +1,18 @@
-[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:
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 9dd32fc9b58..79025ff0d26 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/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.
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index 9818b53a6c2..0e93065e23f 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/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.
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index d9e69b7e83c..1b12533c9f8 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1339,19 +1339,19 @@
               \result ≡ \null ∨ \result ≡ \old(s) ∨
               \result ≡ __fc_p_tmpnam
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 108)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 109)
             assigns *(__fc_p_tmpnam + (0 .. 2048)), *(s + (0 .. 2048)),
                     \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 108)
+[ Extern  ] Froms (file share/libc/stdio.h, line 109)
             assigns *(__fc_p_tmpnam + (0 .. 2048))
               \from *(__fc_p_tmpnam + (0 .. 2048)), (indirect: s);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 110)
+[ Extern  ] Froms (file share/libc/stdio.h, line 111)
             assigns *(s + (0 .. 2048))
               \from (indirect: s), *(__fc_p_tmpnam + (0 .. 2048));
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 111)
+[ Extern  ] Froms (file share/libc/stdio.h, line 112)
             assigns \result \from s, __fc_p_tmpnam;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1368,7 +1368,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 120)
+[ Extern  ] Froms (file share/libc/stdio.h, line 121)
             assigns \result \from (indirect: stream), (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1382,37 +1382,37 @@
 [ Extern  ] Post-condition 'result_zero_or_EOF'
             ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 129)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 130)
             assigns \result, *stream, __fc_fopen[0 .. 16 - 1];
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'flush_all' (file share/libc/stdio.h, line 136)
+[ Extern  ] Assigns for 'flush_all' (file share/libc/stdio.h, line 137)
             assigns __fc_fopen[0 .. 16 - 1], \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'flush_stream' (file share/libc/stdio.h, line 141)
+[ Extern  ] Assigns for 'flush_stream' (file share/libc/stdio.h, line 142)
             assigns *stream, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 129)
+[ Extern  ] Froms (file share/libc/stdio.h, line 130)
             assigns \result
               \from (indirect: *stream), (indirect: __fc_fopen[0 .. 16 - 1]);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 131)
+[ Extern  ] Froms (file share/libc/stdio.h, line 132)
             assigns *stream
               \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 131)
+[ Extern  ] Froms (file share/libc/stdio.h, line 132)
             assigns __fc_fopen[0 .. 16 - 1]
               \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1];
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'flush_all' (file share/libc/stdio.h, line 136)
+[ Extern  ] Froms for 'flush_all' (file share/libc/stdio.h, line 137)
             assigns __fc_fopen[0 .. 16 - 1] \from __fc_fopen[0 .. 16 - 1];
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'flush_all' (file share/libc/stdio.h, line 138)
+[ Extern  ] Froms for 'flush_all' (file share/libc/stdio.h, line 139)
             assigns \result \from (indirect: __fc_fopen[0 .. 16 - 1]);
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'flush_stream' (file share/libc/stdio.h, line 141)
+[ Extern  ] Froms for 'flush_stream' (file share/libc/stdio.h, line 142)
             assigns *stream \from *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'flush_stream' (file share/libc/stdio.h, line 142)
+[ Extern  ] Froms for 'flush_stream' (file share/libc/stdio.h, line 143)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1438,7 +1438,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 151)
+[ Extern  ] Froms (file share/libc/stdio.h, line 152)
             assigns \result
               \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
                     (indirect: *(mode + (0 .. strlen{Old}(mode)))),
@@ -1458,16 +1458,16 @@
               \result ≡ \null ∨
               \subset(\result, &__fc_fopen[0 .. 16 - 1])
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 161)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 162)
             assigns \result, __fc_fopen[fd];
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 161)
+[ Extern  ] Froms (file share/libc/stdio.h, line 162)
             assigns \result
               \from (indirect: fd),
                     (indirect: *(mode + (0 .. strlen{Old}(mode)))),
                     (indirect: __fc_fopen[fd]), __fc_p_fopen;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 161)
+[ Extern  ] Froms (file share/libc/stdio.h, line 162)
             assigns __fc_fopen[fd]
               \from (indirect: fd),
                     (indirect: *(mode + (0 .. strlen{Old}(mode)))),
@@ -1489,16 +1489,16 @@
 [ Extern  ] Post-condition 'stream_opened'
             ensures stream_opened: *\old(stream) ∈ __fc_fopen[0 .. 16 - 1]
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 173)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 174)
             assigns \result, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 173)
+[ Extern  ] Froms (file share/libc/stdio.h, line 174)
             assigns \result
               \from (indirect: *(filename + (..))),
                     (indirect: *(mode + (..))), __fc_p_fopen,
                     (indirect: stream);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 175)
+[ Extern  ] Froms (file share/libc/stdio.h, line 176)
             assigns *stream
               \from (indirect: *(filename + (..))),
                     (indirect: *(mode + (..))), __fc_p_fopen,
@@ -1512,10 +1512,10 @@
 --- Properties of Function 'setbuf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 186)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 187)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 186)
+[ Extern  ] Froms (file share/libc/stdio.h, line 187)
             assigns *stream \from buf;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1526,10 +1526,10 @@
 --- Properties of Function 'setvbuf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 190)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 191)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 190)
+[ Extern  ] Froms (file share/libc/stdio.h, line 191)
             assigns *stream \from buf, mode, size;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1540,10 +1540,10 @@
 --- Properties of Function 'vfprintf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 219)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 220)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 219)
+[ Extern  ] Froms (file share/libc/stdio.h, line 220)
             assigns *stream \from *(format + (..)), arg;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1554,10 +1554,10 @@
 --- Properties of Function 'vfscanf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 224)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 225)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 224)
+[ Extern  ] Froms (file share/libc/stdio.h, line 225)
             assigns *stream \from *(format + (..)), *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1568,10 +1568,10 @@
 --- Properties of Function 'vprintf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 230)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 231)
             assigns *__fc_stdout;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 230)
+[ Extern  ] Froms (file share/libc/stdio.h, line 231)
             assigns *__fc_stdout \from arg;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1582,10 +1582,10 @@
 --- Properties of Function 'vscanf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 234)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 235)
             assigns *__fc_stdin;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 234)
+[ Extern  ] Froms (file share/libc/stdio.h, line 235)
             assigns *__fc_stdin \from *(format + (..));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1596,10 +1596,10 @@
 --- Properties of Function 'vsnprintf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 239)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 240)
             assigns *(s + (0 .. n - 1));
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 239)
+[ Extern  ] Froms (file share/libc/stdio.h, line 240)
             assigns *(s + (0 .. n - 1)) \from *(format + (..)), arg;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1610,10 +1610,10 @@
 --- Properties of Function 'vsprintf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 245)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 246)
             assigns *(s + (0 ..));
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 245)
+[ Extern  ] Froms (file share/libc/stdio.h, line 246)
             assigns *(s + (0 ..)) \from *(format + (..)), arg;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1628,13 +1628,13 @@
             ensures
             result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 258)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 259)
             assigns *stream, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 258)
+[ Extern  ] Froms (file share/libc/stdio.h, line 259)
             assigns *stream \from *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 259)
+[ Extern  ] Froms (file share/libc/stdio.h, line 260)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1659,14 +1659,14 @@
             terminated_string_on_success:
               \result ≢ \null ⇒ valid_string(\old(s))
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 267)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 268)
             assigns *(s + (0 .. size - 1)), \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 267)
+[ Extern  ] Froms (file share/libc/stdio.h, line 268)
             assigns *(s + (0 .. size - 1))
               \from (indirect: size), (indirect: *stream);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 268)
+[ Extern  ] Froms (file share/libc/stdio.h, line 269)
             assigns \result \from s, (indirect: size), (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1677,13 +1677,13 @@
 --- Properties of Function 'fputc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 281)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 282)
             assigns *stream, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 281)
+[ Extern  ] Froms (file share/libc/stdio.h, line 282)
             assigns *stream \from c, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 282)
+[ Extern  ] Froms (file share/libc/stdio.h, line 283)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1694,13 +1694,13 @@
 --- Properties of Function 'fputs'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 288)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 289)
             assigns *stream, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 288)
-            assigns *stream \from *(s + (0 .. strlen{Old}(s)));
-            Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 289)
+            assigns *stream \from *(s + (0 .. strlen{Old}(s))), *stream;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 290)
             assigns \result
               \from (indirect: *(s + (0 .. strlen{Old}(s)))),
                     (indirect: *stream);
@@ -1713,13 +1713,13 @@
 --- Properties of Function 'getc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 296)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 297)
             assigns \result, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 296)
+[ Extern  ] Froms (file share/libc/stdio.h, line 297)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 296)
+[ Extern  ] Froms (file share/libc/stdio.h, line 297)
             assigns *stream \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1730,13 +1730,13 @@
 --- Properties of Function 'getchar'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 301)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 302)
             assigns \result, *__fc_stdin;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 301)
+[ Extern  ] Froms (file share/libc/stdio.h, line 302)
             assigns \result \from *__fc_stdin;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 301)
+[ Extern  ] Froms (file share/libc/stdio.h, line 302)
             assigns *__fc_stdin \from *__fc_stdin;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1751,16 +1751,16 @@
             ensures
             result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 314)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 315)
             assigns *(s + (0 .. gets_length{Old})), \result, *__fc_stdin;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 314)
+[ Extern  ] Froms (file share/libc/stdio.h, line 315)
             assigns *(s + (0 .. gets_length{Old})) \from *__fc_stdin;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 315)
+[ Extern  ] Froms (file share/libc/stdio.h, line 316)
             assigns \result \from s, *__fc_stdin;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 316)
+[ Extern  ] Froms (file share/libc/stdio.h, line 317)
             assigns *__fc_stdin \from *__fc_stdin;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1771,13 +1771,13 @@
 --- Properties of Function 'putc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 323)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 324)
             assigns *stream, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 323)
-            assigns *stream \from c;
-            Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 324)
+            assigns *stream \from c, *stream;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 325)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1788,13 +1788,13 @@
 --- Properties of Function 'putchar'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 329)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 330)
             assigns *__fc_stdout, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 329)
-            assigns *__fc_stdout \from c;
-            Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 330)
+            assigns *__fc_stdout \from c, *__fc_stdout;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 331)
             assigns \result \from (indirect: *__fc_stdout);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1805,13 +1805,14 @@
 --- Properties of Function 'puts'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 336)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 337)
             assigns *__fc_stdout, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 336)
-            assigns *__fc_stdout \from *(s + (0 .. strlen{Old}(s)));
-            Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 337)
+            assigns *__fc_stdout
+              \from *(s + (0 .. strlen{Old}(s))), *__fc_stdout;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 338)
             assigns \result
               \from (indirect: *(s + (0 .. strlen{Old}(s)))),
                     (indirect: *__fc_stdout);
@@ -1828,13 +1829,13 @@
             ensures
             result_ok_or_error: \result ≡ \old(c) ∨ \result ≡ -1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 343)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 344)
             assigns *stream, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 343)
+[ Extern  ] Froms (file share/libc/stdio.h, line 344)
             assigns *stream \from (indirect: c);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 344)
+[ Extern  ] Froms (file share/libc/stdio.h, line 345)
             assigns \result \from (indirect: c), (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1854,14 +1855,19 @@
               \initialized((char *)\old(ptr) +
                            (0 .. \result * \old(size) - 1))
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 352)
-            assigns *((char *)ptr + (0 .. nmemb * size - 1)), \result;
+[ Extern  ] Assigns (file share/libc/stdio.h, line 353)
+            assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream,
+                    \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 352)
+[ Extern  ] Froms (file share/libc/stdio.h, line 353)
             assigns *((char *)ptr + (0 .. nmemb * size - 1))
               \from (indirect: size), (indirect: nmemb), (indirect: *stream);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 354)
+[ Extern  ] Froms (file share/libc/stdio.h, line 353)
+            assigns *stream
+              \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 355)
             assigns \result \from size, (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1875,14 +1881,14 @@
 [ Extern  ] Post-condition 'size_written'
             ensures size_written: \result ≤ \old(nmemb)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 365)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 366)
             assigns *stream, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 365)
+[ Extern  ] Froms (file share/libc/stdio.h, line 366)
             assigns *stream
               \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 365)
+[ Extern  ] Froms (file share/libc/stdio.h, line 366)
             assigns \result
               \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1)));
             Unverifiable but considered Valid.
@@ -1894,13 +1900,13 @@
 --- Properties of Function 'fgetpos'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 376)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 377)
             assigns *pos, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 376)
+[ Extern  ] Froms (file share/libc/stdio.h, line 377)
             assigns *pos \from (indirect: *stream);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 377)
+[ Extern  ] Froms (file share/libc/stdio.h, line 378)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1911,19 +1917,19 @@
 --- Properties of Function 'fseek'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 385)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 386)
             assigns *stream, \result, __fc_errno;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 385)
+[ Extern  ] Froms (file share/libc/stdio.h, line 386)
             assigns *stream
               \from *stream, (indirect: offset), (indirect: whence);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 386)
+[ Extern  ] Froms (file share/libc/stdio.h, line 387)
             assigns \result
               \from (indirect: *stream), (indirect: offset),
                     (indirect: whence);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 386)
+[ Extern  ] Froms (file share/libc/stdio.h, line 387)
             assigns __fc_errno
               \from (indirect: *stream), (indirect: offset),
                     (indirect: whence);
@@ -1936,10 +1942,10 @@
 --- Properties of Function 'fsetpos'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 395)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 396)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 395)
+[ Extern  ] Froms (file share/libc/stdio.h, line 396)
             assigns *stream \from *pos;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1956,13 +1962,13 @@
               \result ≡ -1 ∨
               (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 401)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 402)
             assigns \result, __fc_errno;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 401)
+[ Extern  ] Froms (file share/libc/stdio.h, line 402)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 401)
+[ Extern  ] Froms (file share/libc/stdio.h, line 402)
             assigns __fc_errno \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1973,10 +1979,10 @@
 --- Properties of Function 'rewind'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 409)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 410)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 409)
+[ Extern  ] Froms (file share/libc/stdio.h, line 410)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1987,10 +1993,10 @@
 --- Properties of Function 'clearerr'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 415)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 416)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 415)
+[ Extern  ] Froms (file share/libc/stdio.h, line 416)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2004,7 +2010,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 421)
+[ Extern  ] Froms (file share/libc/stdio.h, line 422)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2018,7 +2024,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 427)
+[ Extern  ] Froms (file share/libc/stdio.h, line 428)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2029,10 +2035,10 @@
 --- Properties of Function 'flockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 433)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 434)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 433)
+[ Extern  ] Froms (file share/libc/stdio.h, line 434)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2043,10 +2049,10 @@
 --- Properties of Function 'funlockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 439)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 440)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 439)
+[ Extern  ] Froms (file share/libc/stdio.h, line 440)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2057,13 +2063,13 @@
 --- Properties of Function 'ftrylockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 445)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 446)
             assigns \result, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 445)
+[ Extern  ] Froms (file share/libc/stdio.h, line 446)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 445)
+[ Extern  ] Froms (file share/libc/stdio.h, line 446)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2077,7 +2083,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 451)
+[ Extern  ] Froms (file share/libc/stdio.h, line 452)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2088,10 +2094,10 @@
 --- Properties of Function 'perror'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 457)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 458)
             assigns __fc_stdout;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 457)
+[ Extern  ] Froms (file share/libc/stdio.h, line 458)
             assigns __fc_stdout
               \from __fc_errno, *(s + (0 .. strlen{Old}(s)));
             Unverifiable but considered Valid.
@@ -2103,13 +2109,13 @@
 --- Properties of Function 'getc_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 463)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 464)
             assigns \result, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 463)
+[ Extern  ] Froms (file share/libc/stdio.h, line 464)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 463)
+[ Extern  ] Froms (file share/libc/stdio.h, line 464)
             assigns *stream \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2123,7 +2129,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 468)
+[ Extern  ] Froms (file share/libc/stdio.h, line 469)
             assigns \result \from *__fc_stdin;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2134,13 +2140,13 @@
 --- Properties of Function 'putc_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 474)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 475)
             assigns *stream, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 474)
+[ Extern  ] Froms (file share/libc/stdio.h, line 475)
             assigns *stream \from c;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 475)
+[ Extern  ] Froms (file share/libc/stdio.h, line 476)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2151,13 +2157,13 @@
 --- Properties of Function 'putchar_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 480)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 481)
             assigns *__fc_stdout, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 480)
+[ Extern  ] Froms (file share/libc/stdio.h, line 481)
             assigns *__fc_stdout \from c;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 481)
+[ Extern  ] Froms (file share/libc/stdio.h, line 482)
             assigns \result \from (indirect: *__fc_stdout);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2168,10 +2174,10 @@
 --- Properties of Function 'clearerr_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 487)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 488)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 487)
+[ Extern  ] Froms (file share/libc/stdio.h, line 488)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2185,7 +2191,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 493)
+[ Extern  ] Froms (file share/libc/stdio.h, line 494)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2199,7 +2205,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 499)
+[ Extern  ] Froms (file share/libc/stdio.h, line 500)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2213,7 +2219,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 505)
+[ Extern  ] Froms (file share/libc/stdio.h, line 506)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2231,14 +2237,14 @@
               (\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧
                is_open_pipe(\result))
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 532)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 533)
             assigns \result, __fc_fopen[0 ..];
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 532)
+[ Extern  ] Froms (file share/libc/stdio.h, line 533)
             assigns \result
               \from (indirect: *command), (indirect: *type), __fc_p_fopen;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 534)
+[ Extern  ] Froms (file share/libc/stdio.h, line 535)
             assigns __fc_fopen[0 ..]
               \from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
             Unverifiable but considered Valid.
@@ -2256,7 +2262,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 546)
+[ Extern  ] Froms (file share/libc/stdio.h, line 547)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -4048,7 +4054,7 @@
 --------------------------------------------------------------------------------
    179 Completely validated
     16 Locally validated
-   483 Considered valid
+   484 Considered valid
     56 To be validated
-   734 Total
+   735 Total
 --------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index e74f363d781..ed172048f4c 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/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);
 
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index 9070087e4f6..2cf4947a7f1 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -193,14 +193,14 @@
 
 [ Extern  ] Post-condition 'result_string_or_null'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 108)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 109)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 108)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 110)
+[ Extern  ] Froms (file share/libc/stdio.h, line 109)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 111)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 112)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -212,7 +212,7 @@
             Unverifiable but considered Valid.
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 120)
+[ Extern  ] Froms (file share/libc/stdio.h, line 121)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -223,26 +223,26 @@
 
 [ Extern  ] Post-condition 'result_zero_or_EOF'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 129)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 130)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'flush_all' (file share/libc/stdio.h, line 136)
+[ Extern  ] Assigns for 'flush_all' (file share/libc/stdio.h, line 137)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'flush_stream' (file share/libc/stdio.h, line 141)
+[ Extern  ] Assigns for 'flush_stream' (file share/libc/stdio.h, line 142)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 129)
+[ Extern  ] Froms (file share/libc/stdio.h, line 130)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 131)
+[ Extern  ] Froms (file share/libc/stdio.h, line 132)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 131)
+[ Extern  ] Froms (file share/libc/stdio.h, line 132)
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'flush_all' (file share/libc/stdio.h, line 136)
+[ Extern  ] Froms for 'flush_all' (file share/libc/stdio.h, line 137)
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'flush_all' (file share/libc/stdio.h, line 138)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'flush_stream' (file share/libc/stdio.h, line 141)
+[ Extern  ] Froms for 'flush_all' (file share/libc/stdio.h, line 139)
             Unverifiable but considered Valid.
 [ Extern  ] Froms for 'flush_stream' (file share/libc/stdio.h, line 142)
             Unverifiable but considered Valid.
+[ Extern  ] Froms for 'flush_stream' (file share/libc/stdio.h, line 143)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 [  Valid  ] Behavior 'flush_all'
@@ -258,7 +258,7 @@
             Unverifiable but considered Valid.
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 151)
+[ Extern  ] Froms (file share/libc/stdio.h, line 152)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -269,11 +269,11 @@
 
 [ Extern  ] Post-condition 'result_null_or_valid_fd'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 161)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 162)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 161)
+[ Extern  ] Froms (file share/libc/stdio.h, line 162)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 161)
+[ Extern  ] Froms (file share/libc/stdio.h, line 162)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -286,11 +286,11 @@
             Unverifiable but considered Valid.
 [ Extern  ] Post-condition 'stream_opened'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 173)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 174)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 173)
+[ Extern  ] Froms (file share/libc/stdio.h, line 174)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 175)
+[ Extern  ] Froms (file share/libc/stdio.h, line 176)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -299,9 +299,9 @@
 --- Properties of Function 'setbuf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 186)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 187)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 186)
+[ Extern  ] Froms (file share/libc/stdio.h, line 187)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -310,9 +310,9 @@
 --- Properties of Function 'setvbuf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 190)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 191)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 190)
+[ Extern  ] Froms (file share/libc/stdio.h, line 191)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -321,9 +321,9 @@
 --- Properties of Function 'vfprintf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 219)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 220)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 219)
+[ Extern  ] Froms (file share/libc/stdio.h, line 220)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -332,9 +332,9 @@
 --- Properties of Function 'vfscanf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 224)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 225)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 224)
+[ Extern  ] Froms (file share/libc/stdio.h, line 225)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -343,9 +343,9 @@
 --- Properties of Function 'vprintf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 230)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 231)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 230)
+[ Extern  ] Froms (file share/libc/stdio.h, line 231)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -354,9 +354,9 @@
 --- Properties of Function 'vscanf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 234)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 235)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 234)
+[ Extern  ] Froms (file share/libc/stdio.h, line 235)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -365,9 +365,9 @@
 --- Properties of Function 'vsnprintf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 239)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 240)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 239)
+[ Extern  ] Froms (file share/libc/stdio.h, line 240)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -376,9 +376,9 @@
 --- Properties of Function 'vsprintf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 245)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 246)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 245)
+[ Extern  ] Froms (file share/libc/stdio.h, line 246)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -389,12 +389,12 @@
 
 [ Extern  ] Post-condition 'result_uchar_or_eof'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 258)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 258)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 259)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 259)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 260)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -408,12 +408,12 @@
             Unverifiable but considered Valid.
 [ Extern  ] Post-condition 'terminated_string_on_success'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 267)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 267)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 268)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 268)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 269)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -421,12 +421,12 @@
 --- Properties of Function 'fputc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 281)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 281)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 282)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 282)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 283)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -434,12 +434,12 @@
 --- Properties of Function 'fputs'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 288)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 288)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 289)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 289)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 290)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -447,11 +447,11 @@
 --- Properties of Function 'getc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 296)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 297)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 296)
+[ Extern  ] Froms (file share/libc/stdio.h, line 297)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 296)
+[ Extern  ] Froms (file share/libc/stdio.h, line 297)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -460,11 +460,11 @@
 --- Properties of Function 'getchar'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 301)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 302)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 301)
+[ Extern  ] Froms (file share/libc/stdio.h, line 302)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 301)
+[ Extern  ] Froms (file share/libc/stdio.h, line 302)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -475,14 +475,14 @@
 
 [ Extern  ] Post-condition 'result_null_or_same'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 314)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 314)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 315)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 315)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 316)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 317)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -490,12 +490,12 @@
 --- Properties of Function 'putc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 323)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 323)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 324)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 324)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 325)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -503,12 +503,12 @@
 --- Properties of Function 'putchar'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 329)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 329)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 330)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 330)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 331)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -516,12 +516,12 @@
 --- Properties of Function 'puts'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 336)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 336)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 337)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 337)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 338)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -531,12 +531,12 @@
 
 [ Extern  ] Post-condition 'result_ok_or_error'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 343)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 343)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 344)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 344)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 345)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -548,11 +548,13 @@
             Unverifiable but considered Valid.
 [ Extern  ] Post-condition 'initialization'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 352)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 353)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 352)
+[ Extern  ] Froms (file share/libc/stdio.h, line 353)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 354)
+[ Extern  ] Froms (file share/libc/stdio.h, line 353)
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 355)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -563,11 +565,11 @@
 
 [ Extern  ] Post-condition 'size_written'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 365)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 366)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 365)
+[ Extern  ] Froms (file share/libc/stdio.h, line 366)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 365)
+[ Extern  ] Froms (file share/libc/stdio.h, line 366)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -576,12 +578,12 @@
 --- Properties of Function 'fgetpos'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 376)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 376)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 377)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 377)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 378)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -589,13 +591,13 @@
 --- Properties of Function 'fseek'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 385)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 385)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 386)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 386)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 386)
+[ Extern  ] Froms (file share/libc/stdio.h, line 387)
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 387)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -604,9 +606,9 @@
 --- Properties of Function 'fsetpos'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 395)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 396)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 395)
+[ Extern  ] Froms (file share/libc/stdio.h, line 396)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -617,11 +619,11 @@
 
 [ Extern  ] Post-condition 'success_or_error'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 401)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 402)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 401)
+[ Extern  ] Froms (file share/libc/stdio.h, line 402)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 401)
+[ Extern  ] Froms (file share/libc/stdio.h, line 402)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -630,9 +632,9 @@
 --- Properties of Function 'rewind'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 409)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 410)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 409)
+[ Extern  ] Froms (file share/libc/stdio.h, line 410)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -641,9 +643,9 @@
 --- Properties of Function 'clearerr'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 415)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 416)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 415)
+[ Extern  ] Froms (file share/libc/stdio.h, line 416)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -654,7 +656,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 421)
+[ Extern  ] Froms (file share/libc/stdio.h, line 422)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -665,7 +667,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 427)
+[ Extern  ] Froms (file share/libc/stdio.h, line 428)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -674,9 +676,9 @@
 --- Properties of Function 'flockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 433)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 434)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 433)
+[ Extern  ] Froms (file share/libc/stdio.h, line 434)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -685,9 +687,9 @@
 --- Properties of Function 'funlockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 439)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 440)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 439)
+[ Extern  ] Froms (file share/libc/stdio.h, line 440)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -696,11 +698,11 @@
 --- Properties of Function 'ftrylockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 445)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 446)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 445)
+[ Extern  ] Froms (file share/libc/stdio.h, line 446)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 445)
+[ Extern  ] Froms (file share/libc/stdio.h, line 446)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -711,7 +713,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 451)
+[ Extern  ] Froms (file share/libc/stdio.h, line 452)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -720,9 +722,9 @@
 --- Properties of Function 'perror'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 457)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 458)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 457)
+[ Extern  ] Froms (file share/libc/stdio.h, line 458)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -731,11 +733,11 @@
 --- Properties of Function 'getc_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 463)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 464)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 463)
+[ Extern  ] Froms (file share/libc/stdio.h, line 464)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 463)
+[ Extern  ] Froms (file share/libc/stdio.h, line 464)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -746,7 +748,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 468)
+[ Extern  ] Froms (file share/libc/stdio.h, line 469)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -755,12 +757,12 @@
 --- Properties of Function 'putc_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 474)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 474)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 475)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 475)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 476)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -768,12 +770,12 @@
 --- Properties of Function 'putchar_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 480)
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 480)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 481)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 481)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 482)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -781,9 +783,9 @@
 --- Properties of Function 'clearerr_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 487)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 488)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 487)
+[ Extern  ] Froms (file share/libc/stdio.h, line 488)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -794,7 +796,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 493)
+[ Extern  ] Froms (file share/libc/stdio.h, line 494)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -805,7 +807,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 499)
+[ Extern  ] Froms (file share/libc/stdio.h, line 500)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -816,7 +818,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 505)
+[ Extern  ] Froms (file share/libc/stdio.h, line 506)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -827,11 +829,11 @@
 
 [ Extern  ] Post-condition 'result_error_or_valid_open_pipe'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 532)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 533)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 532)
+[ Extern  ] Froms (file share/libc/stdio.h, line 533)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 534)
+[ Extern  ] Froms (file share/libc/stdio.h, line 535)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -844,7 +846,7 @@
             Unverifiable but considered Valid.
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 546)
+[ Extern  ] Froms (file share/libc/stdio.h, line 547)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -864,7 +866,7 @@
 --- Status Report Summary
 --------------------------------------------------------------------------------
     72 Completely validated
-   197 Considered valid
+   198 Considered valid
      1 To be validated
-   270 Total
+   271 Total
 --------------------------------------------------------------------------------
-- 
GitLab