diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index 832567d64f6290b9c371111691b52b65e7c1926c..c33a599cc6a5be7e989d98a9fb6268d50fe6d072 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
@@ -12,7 +12,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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 95d6cf5297f29e539893f37b6ec3b2469440b761..cf2ce359ad051f41fb7a8144456c48f3ba162a7f 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:195: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:265: 
   Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:197: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:267: 
   Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:199: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:269: 
   Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:202: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
   Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:204: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
   Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:206: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
   Declaration of variadic function swscanf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:165: 
   Declaration of variadic function fprintf.
@@ -24,7 +24,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   Declaration of variadic function dprintf.
 [variadic] tests/known/printf.c:37: 
   Translating call to printf to a call to the specialized version printf_va_1.
@@ -162,6 +162,8 @@
 #include "stdio.c"
 #include "stdio.h"
 #include "stdlib.h"
+#include "string.h"
+#include "strings.h"
 #include "time.h"
 #include "wchar.h"
 /*@ requires valid_read_string(format);
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 d322a92f77e082966e1f3ba31a4096c403113f6b..96287d6d468ea3815206a73c3e4595685e794299 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
@@ -12,7 +12,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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 12097cda98fa628de6c3431143db25fd7544f16c..1830a1983da84f82418e69a71b2efb0c3d288aea 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
@@ -12,7 +12,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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 40db9d7dbbf143e9c8ced207fd7ac8ac2ebe8d23..5e1783c24206b61b139ddbdf83738a710f416f66 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
@@ -12,7 +12,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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.
@@ -424,7 +424,7 @@ int main(void)
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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 22a8fdf1bb42bb62dcd300c2b8a68f3e8d281426..c17cd35b1db426762475e22683b67d5642322df7 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
@@ -12,7 +12,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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 0a7a3cb2f389a34ab022bcfa82d62fb3908882ef..dc4f5f5056b7a506d36065e972d4bae7f15b2bed 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
@@ -12,7 +12,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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 0ad1522b6520cd7aa591efda0f9f72657c9162b1..01d07d14edca771660ecc911e471607621e0a323 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
@@ -12,7 +12,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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 cf8814488a75dd118d8e8abac81f3bab09ad9baa..b5123404c1c521e1cdb3c842124c7f6be08fdacc 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -12,7 +12,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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 41f785ff02c2f035754f6d27cb48445c435a0f04..f6082cc06eddc1ec8fd7e81cbb3d66be38349fad 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -12,7 +12,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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 23148c803852e714e6e6460bbb3584c014a6662f..7d4b64672ebf65221f4cbcffeca8202eceb82b9f 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -12,7 +12,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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 f4694f2f3632e5e0d4fdbcdf9ef2ef527a077e69..ff34f6beb5cfd87e523c1f71f5c2e697af1685eb 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:195: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:265: 
   Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:197: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:267: 
   Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:199: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:269: 
   Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:202: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
   Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:204: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
   Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:206: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
   Declaration of variadic function swscanf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:165: 
   Declaration of variadic function fprintf.
@@ -24,7 +24,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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.
@@ -57,6 +57,8 @@
 #include "signal.h"
 #include "stdarg.h"
 #include "stdio.h"
+#include "string.h"
+#include "strings.h"
 #include "time.h"
 #include "wchar.h"
 int volatile nondet;
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index a5376947d85456fcb47acfbcc4979db23dd1eb7a..ad8320c3cca852be30d2b0ff8fe5a13e1a3e0a98 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:195: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:265: 
   Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:197: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:267: 
   Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:199: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:269: 
   Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:202: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
   Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:204: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
   Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:206: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
   Declaration of variadic function swscanf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:165: 
   Declaration of variadic function fprintf.
@@ -24,7 +24,7 @@
   Declaration of variadic function sprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:175: 
   Declaration of variadic function sscanf.
-[variadic] FRAMAC_SHARE/libc/stdio.h:369: 
+[variadic] FRAMAC_SHARE/libc/stdio.h:439: 
   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.
@@ -86,6 +86,8 @@
 #include "signal.h"
 #include "stdarg.h"
 #include "stdio.h"
+#include "string.h"
+#include "strings.h"
 #include "time.h"
 #include "wchar.h"
 /*@ requires valid_read_wstring(format);
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 630d2219ba4794e3763ba8e70b88cedb13ad48b3..9deb0bc5e01c04aaea0bbf5178f55316e8f09166 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -1055,6 +1055,8 @@
             Unverifiable but considered Valid.
 [ Extern  ] Axiom 'wcsncmp_zero'
             Unverifiable but considered Valid.
+[ Extern  ] Axiom 'wmemchr_def'
+            Unverifiable but considered Valid.
 [  Valid  ] Axiomatic 'MemChr'
             by Frama-C kernel.
 [  Valid  ] Axiomatic 'MemCmp'
@@ -1069,6 +1071,8 @@
             by Frama-C kernel.
 [  Valid  ] Axiomatic 'StrNCmp'
             by Frama-C kernel.
+[  Valid  ] Axiomatic 'WMemChr'
+            by Frama-C kernel.
 [  Valid  ] Axiomatic 'WcsChr'
             by Frama-C kernel.
 [  Valid  ] Axiomatic 'WcsCmp'
@@ -2216,9 +2220,9 @@
 --------------------------------------------------------------------------------
 --- Status Report Summary
 --------------------------------------------------------------------------------
-   161 Completely validated
-   238 Considered valid
+   162 Completely validated
+   239 Considered valid
     29 To be validated
      4 Alarms emitted
-   432 Total
+   434 Total
 --------------------------------------------------------------------------------
diff --git a/tests/builtins/oracle/wcslen.res.oracle b/tests/builtins/oracle/wcslen.res.oracle
index 95f2548751afd2e5be3566ba103027f089417ec5..f5a97cc85744af051d76551bd0250596ac7f074f 100644
--- a/tests/builtins/oracle/wcslen.res.oracle
+++ b/tests/builtins/oracle/wcslen.res.oracle
@@ -618,7 +618,7 @@
 [inout] Inputs for function misc:
     Frama_C_entropy_source; static_str; zero_str; tab_str[0..11];
     unterminated_string[0..11]; nondet; L"Hello World\n"[bits 0 to 415];
-    L"abc\000\000\000abc"[bits 0 to 319]; L""; L"a"[bits 0 to 63];
+    L"abc\000\000\000abc"[bits 0 to 127]; L""; L"a"[bits 0 to 63];
     L"aa"[bits 0 to 95]; L"aaa"[bits 0 to 127]; L"aaaa"[bits 0 to 159];
     L"aaaaa"[bits 0 to 191]; L"aaaaaa"[bits 0 to 223];
     L"aaaaaaaaa"[bits 0 to 319]; L"aaaaaaaaaa"[bits 0 to 351];
@@ -662,7 +662,7 @@
 [inout] Inputs for function main:
     Frama_C_entropy_source; static_str; zero_str; tab_str[0..11];
     unterminated_string[0..11]; nondet; L"Hello World\n"[bits 0 to 415];
-    L"abc\000\000\000abc"[bits 0 to 319]; L""; L"a"[bits 0 to 63];
+    L"abc\000\000\000abc"[bits 0 to 127]; L""; L"a"[bits 0 to 63];
     L"aa"[bits 0 to 95]; L"aaa"[bits 0 to 127]; L"aaaa"[bits 0 to 159];
     L"aaaaa"[bits 0 to 191]; L"aaaaaa"[bits 0 to 223];
     L"aaaaaaaaa"[bits 0 to 319]; L"aaaaaaaaaa"[bits 0 to 351];
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 56319e5d1845473862f9cb775b4515dc3ab93f09..7dff010c2ccf5ba38a23b37e5d80e80143973836 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1223,6 +1223,12 @@
 [ Extern  ] Axiom 'wcsncmp_zero'
             axiom wcsncmp_zero
             Unverifiable but considered Valid.
+[ Extern  ] Axiom 'wmemchr_def'
+            axiom wmemchr_def
+            Unverifiable but considered Valid.
+[  Valid  ] Axiomatic 'GetsLength'
+            axiomatic GetsLength
+            by Frama-C kernel.
 [  Valid  ] Axiomatic 'MemChr'
             axiomatic MemChr
             by Frama-C kernel.
@@ -1244,6 +1250,9 @@
 [  Valid  ] Axiomatic 'StrNCmp'
             axiomatic StrNCmp
             by Frama-C kernel.
+[  Valid  ] Axiomatic 'WMemChr'
+            axiomatic WMemChr
+            by Frama-C kernel.
 [  Valid  ] Axiomatic 'WcsChr'
             axiomatic WcsChr
             by Frama-C kernel.
@@ -1577,19 +1586,24 @@
             ensures
             result_null_or_same: \result ≡ \null ∨ \result ≡ \old(s)
             Unverifiable but considered Valid.
+[ Extern  ] Post-condition 'initialization,at_least_one'
+            ensures
+            initialization: at_least_one:
+              \result ≢ \null ⇒ \initialized(\old(s) + 0)
+            Unverifiable but considered Valid.
 [ Extern  ] Post-condition 'terminated_string_on_success'
             ensures
             terminated_string_on_success:
               \result ≢ \null ⇒ valid_string(\old(s))
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 225)
-            assigns *(s + (0 .. size)), \result;
+[ Extern  ] Assigns (file share/libc/stdio.h, line 226)
+            assigns *(s + (0 .. size - 1)), \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 225)
-            assigns *(s + (0 .. size))
+[ Extern  ] Froms (file share/libc/stdio.h, line 226)
+            assigns *(s + (0 .. size - 1))
               \from (indirect: size), (indirect: *stream);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 226)
+[ Extern  ] Froms (file share/libc/stdio.h, line 227)
             assigns \result \from s, (indirect: size), (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1600,7 +1614,7 @@
 --- Properties of Function 'fputc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 234)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 238)
             assigns *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1611,10 +1625,10 @@
 --- Properties of Function 'fputs'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 237)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 241)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 237)
+[ Extern  ] Froms (file share/libc/stdio.h, line 241)
             assigns *stream \from *(s + (..));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1625,13 +1639,13 @@
 --- Properties of Function 'getc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 241)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 245)
             assigns \result, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 241)
+[ Extern  ] Froms (file share/libc/stdio.h, line 245)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 241)
+[ Extern  ] Froms (file share/libc/stdio.h, line 245)
             assigns *stream \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1645,7 +1659,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 244)
+[ Extern  ] Froms (file share/libc/stdio.h, line 248)
             assigns \result \from *__fc_stdin;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1660,14 +1674,17 @@
             ensures
             result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 248)
-            assigns *(s + (..)), \result;
+[ Extern  ] Assigns (file share/libc/stdio.h, line 260)
+            assigns *(s + (0 .. gets_length{Old})), \result, *__fc_stdin;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 248)
-            assigns *(s + (..)) \from *__fc_stdin;
+[ Extern  ] Froms (file share/libc/stdio.h, line 260)
+            assigns *(s + (0 .. gets_length{Old})) \from *__fc_stdin;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 261)
+            assigns \result \from s, *__fc_stdin;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 249)
-            assigns \result \from s, __fc_stdin;
+[ Extern  ] Froms (file share/libc/stdio.h, line 262)
+            assigns *__fc_stdin \from *__fc_stdin;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             default behavior
@@ -1677,10 +1694,10 @@
 --- Properties of Function 'putc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 254)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 269)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 254)
+[ Extern  ] Froms (file share/libc/stdio.h, line 269)
             assigns *stream \from c;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1691,10 +1708,10 @@
 --- Properties of Function 'putchar'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 257)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 273)
             assigns *__fc_stdout;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 257)
+[ Extern  ] Froms (file share/libc/stdio.h, line 273)
             assigns *__fc_stdout \from c;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1705,10 +1722,10 @@
 --- Properties of Function 'puts'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 260)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 276)
             assigns *__fc_stdout;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 260)
+[ Extern  ] Froms (file share/libc/stdio.h, line 276)
             assigns *__fc_stdout \from *(s + (..));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1719,10 +1736,10 @@
 --- Properties of Function 'ungetc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 263)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 281)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 263)
+[ Extern  ] Froms (file share/libc/stdio.h, line 281)
             assigns *stream \from c;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1742,14 +1759,14 @@
               \initialized((char *)\old(ptr) +
                            (0 .. \result * \old(size) - 1))
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 269)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 288)
             assigns *((char *)ptr + (0 .. nmemb * size - 1)), \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 269)
+[ Extern  ] Froms (file share/libc/stdio.h, line 288)
             assigns *((char *)ptr + (0 .. nmemb * size - 1))
               \from size, nmemb, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 270)
+[ Extern  ] Froms (file share/libc/stdio.h, line 289)
             assigns \result \from size, *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1763,13 +1780,13 @@
 [ Extern  ] Post-condition 'size_written'
             ensures size_written: \result ≤ \old(nmemb)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 282)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 301)
             assigns *stream, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 282)
+[ Extern  ] Froms (file share/libc/stdio.h, line 301)
             assigns *stream \from *((char *)ptr + (0 .. nmemb * size - 1));
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 282)
+[ Extern  ] Froms (file share/libc/stdio.h, line 301)
             assigns \result \from *((char *)ptr + (0 .. nmemb * size - 1));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1780,10 +1797,10 @@
 --- Properties of Function 'fgetpos'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 290)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 309)
             assigns *pos;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 290)
+[ Extern  ] Froms (file share/libc/stdio.h, line 309)
             assigns *pos \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1794,19 +1811,19 @@
 --- Properties of Function 'fseek'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 297)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 316)
             assigns *stream, \result, __fc_errno;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 297)
+[ Extern  ] Froms (file share/libc/stdio.h, line 316)
             assigns *stream
               \from *stream, (indirect: offset), (indirect: whence);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 298)
+[ Extern  ] Froms (file share/libc/stdio.h, line 317)
             assigns \result
               \from (indirect: *stream), (indirect: offset),
                     (indirect: whence);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 298)
+[ Extern  ] Froms (file share/libc/stdio.h, line 317)
             assigns __fc_errno
               \from (indirect: *stream), (indirect: offset),
                     (indirect: whence);
@@ -1819,10 +1836,10 @@
 --- Properties of Function 'fsetpos'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 303)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 322)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 303)
+[ Extern  ] Froms (file share/libc/stdio.h, line 322)
             assigns *stream \from *pos;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1839,13 +1856,13 @@
               \result ≡ -1 ∨
               (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno))
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 308)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 327)
             assigns \result, __fc_errno;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 308)
+[ Extern  ] Froms (file share/libc/stdio.h, line 327)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 308)
+[ Extern  ] Froms (file share/libc/stdio.h, line 327)
             assigns __fc_errno \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1856,10 +1873,10 @@
 --- Properties of Function 'rewind'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 314)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 335)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 314)
+[ Extern  ] Froms (file share/libc/stdio.h, line 335)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1870,10 +1887,10 @@
 --- Properties of Function 'clearerr'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 317)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 341)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 317)
+[ Extern  ] Froms (file share/libc/stdio.h, line 341)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1887,7 +1904,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 320)
+[ Extern  ] Froms (file share/libc/stdio.h, line 347)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1901,7 +1918,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 323)
+[ Extern  ] Froms (file share/libc/stdio.h, line 353)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1912,10 +1929,10 @@
 --- Properties of Function 'flockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 326)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 359)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 326)
+[ Extern  ] Froms (file share/libc/stdio.h, line 359)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1926,10 +1943,10 @@
 --- Properties of Function 'funlockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 329)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 365)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 329)
+[ Extern  ] Froms (file share/libc/stdio.h, line 365)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1940,13 +1957,13 @@
 --- Properties of Function 'ftrylockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 332)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 371)
             assigns \result, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 332)
+[ Extern  ] Froms (file share/libc/stdio.h, line 371)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 332)
+[ Extern  ] Froms (file share/libc/stdio.h, line 371)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1960,7 +1977,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 335)
+[ Extern  ] Froms (file share/libc/stdio.h, line 377)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1971,10 +1988,10 @@
 --- Properties of Function 'perror'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 338)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 383)
             assigns __fc_stdout;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 338)
+[ Extern  ] Froms (file share/libc/stdio.h, line 383)
             assigns __fc_stdout \from __fc_errno, *(s + (..));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -1985,13 +2002,13 @@
 --- Properties of Function 'getc_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 341)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 389)
             assigns \result, *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 341)
+[ Extern  ] Froms (file share/libc/stdio.h, line 389)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 341)
+[ Extern  ] Froms (file share/libc/stdio.h, line 389)
             assigns *stream \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2005,7 +2022,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 343)
+[ Extern  ] Froms (file share/libc/stdio.h, line 392)
             assigns \result \from *__fc_stdin;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2016,10 +2033,10 @@
 --- Properties of Function 'putc_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 345)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 397)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 345)
+[ Extern  ] Froms (file share/libc/stdio.h, line 397)
             assigns *stream \from c;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2030,10 +2047,10 @@
 --- Properties of Function 'putchar_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 347)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 401)
             assigns *__fc_stdout;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 347)
+[ Extern  ] Froms (file share/libc/stdio.h, line 401)
             assigns *__fc_stdout \from c;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2044,10 +2061,10 @@
 --- Properties of Function 'clearerr_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 350)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 406)
             assigns *stream;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 350)
+[ Extern  ] Froms (file share/libc/stdio.h, line 406)
             assigns *stream \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2061,7 +2078,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 352)
+[ Extern  ] Froms (file share/libc/stdio.h, line 412)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2075,7 +2092,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 354)
+[ Extern  ] Froms (file share/libc/stdio.h, line 418)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2089,7 +2106,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 356)
+[ Extern  ] Froms (file share/libc/stdio.h, line 424)
             assigns \result \from *stream;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2107,14 +2124,14 @@
               (\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧
                is_open_pipe(\result))
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 381)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 451)
             assigns \result, __fc_fopen[0 ..];
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 381)
+[ Extern  ] Froms (file share/libc/stdio.h, line 451)
             assigns \result
               \from (indirect: *command), (indirect: *type), __fc_p_fopen;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 383)
+[ Extern  ] Froms (file share/libc/stdio.h, line 453)
             assigns __fc_fopen[0 ..]
               \from (indirect: *command), (indirect: *type), __fc_fopen[0 ..];
             Unverifiable but considered Valid.
@@ -2132,7 +2149,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 395)
+[ Extern  ] Froms (file share/libc/stdio.h, line 465)
             assigns \result \from (indirect: *stream);
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3922,9 +3939,9 @@
 --------------------------------------------------------------------------------
 --- Status Report Summary
 --------------------------------------------------------------------------------
-   175 Completely validated
+   177 Completely validated
     16 Locally validated
-   454 Considered valid
+   457 Considered valid
     56 To be validated
-   701 Total
+   706 Total
 --------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index b85450e07ee183420637f89e3cd128f4c31ce19d..095e99c773245339d34cddb59769a1c3cfff0488 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1308,6 +1308,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(wchar_t *s, wchar_t c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(wchar_t *s, wchar_t c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ wchar_t *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≡ \true ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
@@ -4583,12 +4600,17 @@ extern int vsprintf(char * __restrict s, char const * __restrict format,
 extern int fgetc(FILE *stream);
 
 /*@ requires valid_stream: \valid(stream);
+    requires room_s: \valid(s + (0 .. size - 1));
     ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(s);
+    ensures
+      initialization: at_least_one:
+        \result ≢ \null ⇒ \initialized(\old(s) + 0);
     ensures
       terminated_string_on_success:
         \result ≢ \null ⇒ valid_string(\old(s));
-    assigns *(s + (0 .. size)), \result;
-    assigns *(s + (0 .. size)) \from (indirect: size), (indirect: *stream);
+    assigns *(s + (0 .. size - 1)), \result;
+    assigns *(s + (0 .. size - 1))
+      \from (indirect: size), (indirect: *stream);
     assigns \result \from s, (indirect: size), (indirect: *stream);
  */
 extern char *fgets(char * __restrict s, int size, FILE * __restrict stream);
@@ -4610,15 +4632,26 @@ extern int getc(FILE *stream);
     assigns \result \from *__fc_stdin; */
 extern int getchar(void);
 
-/*@ ensures result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null;
-    assigns *(s + (..)), \result;
-    assigns *(s + (..)) \from *__fc_stdin;
-    assigns \result \from s, __fc_stdin;
+/*@ axiomatic GetsLength {
+      logic size_t gets_length{L}
+        reads *__fc_stdin;
+      
+      }
+
+*/
+/*@ requires room_s: \valid(s + (0 .. gets_length));
+    ensures result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null;
+    assigns *(s + (0 .. gets_length{Old})), \result, *__fc_stdin;
+    assigns *(s + (0 .. gets_length{Old})) \from *__fc_stdin;
+    assigns \result \from s, *__fc_stdin;
+    assigns *__fc_stdin \from *__fc_stdin;
  */
 extern char *gets(char *s);
 
-/*@ assigns *stream;
-    assigns *stream \from c; */
+/*@ requires valid_stream: \valid(stream);
+    assigns *stream;
+    assigns *stream \from c;
+ */
 extern int putc(int c, FILE *stream);
 
 /*@ assigns *__fc_stdout;
@@ -4629,8 +4662,10 @@ extern int putchar(int c);
     assigns *__fc_stdout \from *(s + (..)); */
 extern int puts(char const *s);
 
-/*@ assigns *stream;
-    assigns *stream \from c; */
+/*@ requires valid_stream: \valid(stream);
+    assigns *stream;
+    assigns *stream \from c;
+ */
 extern int ungetc(int c, FILE *stream);
 
 /*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1));
@@ -4688,46 +4723,63 @@ extern int fsetpos(FILE *stream, fpos_t const *pos);
  */
 extern long ftell(FILE *stream);
 
-/*@ assigns *stream;
-    assigns *stream \from \nothing; */
+/*@ requires valid_stream: \valid(stream);
+    assigns *stream;
+    assigns *stream \from \nothing;
+ */
 extern void rewind(FILE *stream);
 
-/*@ assigns *stream;
-    assigns *stream \from \nothing; */
+/*@ requires valid_stream: \valid(stream);
+    assigns *stream;
+    assigns *stream \from \nothing;
+ */
 extern void clearerr(FILE *stream);
 
-/*@ assigns \result;
-    assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+    assigns \result;
+    assigns \result \from *stream;
+ */
 extern int feof(FILE *stream);
 
-/*@ assigns \result;
-    assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+    assigns \result;
+    assigns \result \from *stream;
+ */
 extern int fileno(FILE *stream);
 
-/*@ assigns *stream;
-    assigns *stream \from \nothing; */
+/*@ requires valid_stream: \valid(stream);
+    assigns *stream;
+    assigns *stream \from \nothing;
+ */
 extern void flockfile(FILE *stream);
 
-/*@ assigns *stream;
-    assigns *stream \from \nothing; */
+/*@ requires valid_stream: \valid(stream);
+    assigns *stream;
+    assigns *stream \from \nothing;
+ */
 extern void funlockfile(FILE *stream);
 
-/*@ assigns \result, *stream;
+/*@ requires valid_stream: \valid(stream);
+    assigns \result, *stream;
     assigns \result \from \nothing;
     assigns *stream \from \nothing;
  */
 extern int ftrylockfile(FILE *stream);
 
-/*@ assigns \result;
-    assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+    assigns \result;
+    assigns \result \from *stream;
+ */
 extern int ferror(FILE *stream);
 
-/*@ assigns __fc_stdout;
+/*@ requires valid_string_s: valid_read_string(s);
+    assigns __fc_stdout;
     assigns __fc_stdout \from __fc_errno, *(s + (..));
  */
 extern void perror(char const *s);
 
-/*@ assigns \result, *stream;
+/*@ requires valid_stream: \valid(stream);
+    assigns \result, *stream;
     assigns \result \from *stream;
     assigns *stream \from *stream;
  */
@@ -4737,28 +4789,38 @@ extern int getc_unlocked(FILE *stream);
     assigns \result \from *__fc_stdin; */
 extern int getchar_unlocked(void);
 
-/*@ assigns *stream;
-    assigns *stream \from c; */
+/*@ requires valid_stream: \valid(stream);
+    assigns *stream;
+    assigns *stream \from c;
+ */
 extern int putc_unlocked(int c, FILE *stream);
 
 /*@ assigns *__fc_stdout;
     assigns *__fc_stdout \from c; */
 extern int putchar_unlocked(int c);
 
-/*@ assigns *stream;
-    assigns *stream \from \nothing; */
+/*@ requires valid_stream: \valid(stream);
+    assigns *stream;
+    assigns *stream \from \nothing;
+ */
 extern void clearerr_unlocked(FILE *stream);
 
-/*@ assigns \result;
-    assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+    assigns \result;
+    assigns \result \from *stream;
+ */
 extern int feof_unlocked(FILE *stream);
 
-/*@ assigns \result;
-    assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+    assigns \result;
+    assigns \result \from *stream;
+ */
 extern int ferror_unlocked(FILE *stream);
 
-/*@ assigns \result;
-    assigns \result \from *stream; */
+/*@ requires valid_stream: \valid(stream);
+    assigns \result;
+    assigns \result \from *stream;
+ */
 extern int fileno_unlocked(FILE *stream);
 
 /*@ axiomatic pipe_streams {
@@ -6321,7 +6383,21 @@ extern char *tzname[2];
  */
 extern void tzset(void);
 
-/*@ ensures
+/*@ requires
+      valid:
+        valid_read_or_empty((void *)s, (unsigned int)(sizeof(wchar_t) * n)) ∨
+        \valid_read((unsigned char *)s + (0 .. wmemchr_off(s, c, n)));
+    requires
+      initialization:
+        \initialized(s + (0 .. n - 1)) ∨
+        \initialized(s + (0 .. wmemchr_off(s, c, n)));
+    requires
+      danglingness:
+        non_escaping((void *)s, (unsigned int)(sizeof(wchar_t) * n)) ∨
+        non_escaping((void *)s,
+                    (unsigned int)(sizeof(wchar_t) *
+                                   (wmemchr_off(s, c, n) + 1)));
+    ensures
       result_null_or_inside_s:
         \result ≡ \null ∨ \subset(\result, \old(s) + (0 .. \old(n) - 1));
     assigns \result;
@@ -6330,7 +6406,21 @@ extern void tzset(void);
  */
 extern wchar_t *wmemchr(wchar_t const *s, wchar_t c, size_t n);
 
-/*@ assigns \result;
+/*@ requires
+      valid_s1:
+        valid_read_or_empty((void *)s1, (unsigned int)(sizeof(wchar_t) * n));
+    requires
+      valid_s2:
+        valid_read_or_empty((void *)s2, (unsigned int)(sizeof(wchar_t) * n));
+    requires initialization: s1: \initialized(s1 + (0 .. n - 1));
+    requires initialization: s2: \initialized(s2 + (0 .. n - 1));
+    requires
+      danglingness: s1:
+        non_escaping((void *)s1, (unsigned int)(sizeof(wchar_t) * n));
+    requires
+      danglingness: s2:
+        non_escaping((void *)s2, (unsigned int)(sizeof(wchar_t) * n));
+    assigns \result;
     assigns \result
       \from (indirect: *(s1 + (0 .. n - 1))),
             (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
@@ -6339,7 +6429,9 @@ extern int wmemcmp(wchar_t const *s1, wchar_t const *s2, size_t n);
 
 wchar_t *wmemcpy(wchar_t *dest, wchar_t const *src, size_t n);
 
-/*@ ensures result_ptr: \result ≡ \old(dest);
+/*@ requires valid_src: \valid_read(src + (0 .. n - 1));
+    requires valid_dest: \valid(dest + (0 .. n - 1));
+    ensures result_ptr: \result ≡ \old(dest);
     assigns *(dest + (0 .. n - 1)), \result;
     assigns *(dest + (0 .. n - 1))
       \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
@@ -6360,7 +6452,9 @@ wchar_t *wcscat(wchar_t *dest, wchar_t const *src);
  */
 extern wchar_t *wcschr(wchar_t const *wcs, wchar_t wc);
 
-/*@ assigns \result;
+/*@ requires valid_wstring_s1: valid_read_wstring(s1);
+    requires valid_wstring_s2: valid_read_wstring(s2);
+    assigns \result;
     assigns \result
       \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
  */
@@ -6368,13 +6462,25 @@ extern int wcscmp(wchar_t const *s1, wchar_t const *s2);
 
 wchar_t *wcscpy(wchar_t *dest, wchar_t const *src);
 
-/*@ assigns \result;
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+    requires valid_wstring_accept: valid_read_wstring(accept);
+    assigns \result;
     assigns \result
       \from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
  */
 extern size_t wcscspn(wchar_t const *wcs, wchar_t const *accept);
 
-/*@ assigns *(dest + (0 ..)), \result;
+/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
+    requires valid_wstring_dest: valid_wstring(dest);
+    requires
+      room_for_concatenation:
+        \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
+    requires
+      separation:
+        \separated(
+          dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
+          );
+    assigns *(dest + (0 ..)), \result;
     assigns *(dest + (0 ..))
       \from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
             (indirect: src), (indirect: n);
@@ -6385,7 +6491,9 @@ extern size_t wcscspn(wchar_t const *wcs, wchar_t const *accept);
 extern size_t wcslcat(wchar_t * __restrict dest,
                       wchar_t const * __restrict src, size_t n);
 
-/*@ requires
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+    requires room_nwstring: \valid(dest + (0 .. n));
+    requires
       separation: dest: src:
         \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     assigns *(dest + (0 .. n - 1)), \result;
@@ -6401,7 +6509,9 @@ size_t wcslen(wchar_t const *str);
 
 wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n);
 
-/*@ assigns \result;
+/*@ requires valid_wstring_s1: valid_read_wstring(s1);
+    requires valid_wstring_s2: valid_read_wstring(s2);
+    assigns \result;
     assigns \result
       \from (indirect: *(s1 + (0 .. n - 1))),
             (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
@@ -6410,7 +6520,9 @@ extern int wcsncmp(wchar_t const *s1, wchar_t const *s2, size_t n);
 
 wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n);
 
-/*@ ensures
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+    requires valid_wstring_accept: valid_read_wstring(accept);
+    ensures
       result_null_or_inside_wcs:
         \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
     assigns \result;
@@ -6419,21 +6531,28 @@ wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n);
  */
 extern wchar_t *wcspbrk(wchar_t const *wcs, wchar_t const *accept);
 
-/*@ ensures
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+    ensures
       result_null_or_inside_wcs:
         \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
     assigns \result;
-    assigns \result \from wcs, (indirect: *(wcs + (0 ..))), (indirect: wc);
+    assigns \result
+      \from wcs, (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))), (indirect: wc);
  */
 extern wchar_t *wcsrchr(wchar_t const *wcs, wchar_t wc);
 
-/*@ assigns \result;
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+    requires valid_wstring_accept: valid_read_wstring(accept);
+    assigns \result;
     assigns \result
-      \from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
+      \from (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))),
+            (indirect: *(accept + (0 .. wcslen{Old}(accept))));
  */
 extern size_t wcsspn(wchar_t const *wcs, wchar_t const *accept);
 
-/*@ ensures
+/*@ requires valid_wstring_haystack: valid_read_wstring(haystack);
+    requires valid_wstring_needle: valid_read_wstring(needle);
+    ensures
       result_null_or_inside_haystack:
         \result ≡ \null ∨ \subset(\result, \old(haystack) + (0 ..));
     assigns \result;
@@ -6443,13 +6562,14 @@ extern size_t wcsspn(wchar_t const *wcs, wchar_t const *accept);
  */
 extern wchar_t *wcsstr(wchar_t const *haystack, wchar_t const *needle);
 
-/*@ requires valid_stream: \valid(stream);
+/*@ requires room_nwstring: \valid(ws + (0 .. n - 1));
+    requires valid_stream: \valid(stream);
     ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(ws);
     ensures
       terminated_string_on_success:
         \result ≢ \null ⇒ valid_wstring(\old(ws));
-    assigns *(ws + (0 .. n)), \result;
-    assigns *(ws + (0 .. n)) \from (indirect: n), (indirect: *stream);
+    assigns *(ws + (0 .. n - 1)), \result;
+    assigns *(ws + (0 .. n - 1)) \from (indirect: n), (indirect: *stream);
     assigns \result \from ws, (indirect: n), (indirect: *stream);
  */
 extern wchar_t *fgetws(wchar_t * __restrict ws, int n,
@@ -6462,6 +6582,12 @@ extern wchar_t *fgetws(wchar_t * __restrict ws, int n,
 
 */
 /*@ requires
+      valid_dest:
+        valid_or_empty((void *)dest, (unsigned int)(sizeof(wchar_t) * n));
+    requires
+      valid_src:
+        valid_read_or_empty((void *)src, (unsigned int)(sizeof(wchar_t) * n));
+    requires
       separation: dest: src:
         \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
@@ -6482,7 +6608,8 @@ wchar_t *wmemcpy(wchar_t *dest, wchar_t const *src, size_t n)
   return dest;
 }
 
-/*@ ensures result_ptr: \result ≡ \old(dest);
+/*@ requires valid_wcs: \valid(dest + (0 .. len - 1));
+    ensures result_ptr: \result ≡ \old(dest);
     ensures
       initialization: wcs: \initialized(\old(dest) + (0 .. \old(len) - 1));
     ensures
@@ -6504,11 +6631,15 @@ wchar_t *wmemset(wchar_t *dest, wchar_t val, size_t len)
   return dest;
 }
 
-/*@ ensures result_ptr: \result ≡ \old(dest);
-    assigns *(dest + (0 ..)), \result;
-    assigns *(dest + (0 ..))
-      \from *(src + (0 ..)), (indirect: src), *(dest + (0 ..)),
-            (indirect: dest);
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+    requires room_wstring: \valid(dest + (0 .. wcslen(src)));
+    requires
+      separation:
+        \separated(dest + (0 .. wcslen(src)), src + (0 .. wcslen(src)));
+    ensures result_ptr: \result ≡ \old(dest);
+    assigns *(dest + (0 .. wcslen{Old}(src))), \result;
+    assigns *(dest + (0 .. wcslen{Old}(src)))
+      \from *(src + (0 .. wcslen{Old}(src))), (indirect: src);
     assigns \result \from dest;
  */
 wchar_t *wcscpy(wchar_t *dest, wchar_t const *src)
@@ -6524,8 +6655,9 @@ wchar_t *wcscpy(wchar_t *dest, wchar_t const *src)
 }
 
 /*@ requires valid_string_s: valid_read_wstring(str);
+    ensures result_is_length: \result ≡ wcslen(\old(str));
     assigns \result;
-    assigns \result \from (indirect: *(str + (0 ..)));
+    assigns \result \from (indirect: *(str + (0 .. wcslen{Old}(str))));
  */
 size_t wcslen(wchar_t const *str)
 {
@@ -6535,10 +6667,13 @@ size_t wcslen(wchar_t const *str)
   return i;
 }
 
-/*@ requires
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+    requires room_nwstring: \valid(dest + (0 .. n - 1));
+    requires
       separation: dest: src:
         \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
+    ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
     assigns *(dest + (0 .. n - 1)), \result;
     assigns *(dest + (0 .. n - 1))
       \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
@@ -6560,7 +6695,17 @@ wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n)
   return dest;
 }
 
-/*@ ensures result_ptr: \result ≡ \old(dest);
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+    requires valid_wstring_dest: valid_wstring(dest);
+    requires
+      room_for_concatenation:
+        \valid(dest + (wcslen(dest) .. wcslen(dest) + wcslen(src)));
+    requires
+      separation:
+        \separated(
+          dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
+          );
+    ensures result_ptr: \result ≡ \old(dest);
     assigns *(dest + (0 ..)), \result;
     assigns *(dest + (0 ..))
       \from *(dest + (0 ..)), (indirect: dest), *(src + (0 ..)),
@@ -6580,7 +6725,17 @@ wchar_t *wcscat(wchar_t *dest, wchar_t const *src)
   return dest;
 }
 
-/*@ ensures result_ptr: \result ≡ \old(dest);
+/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
+    requires valid_wstring_dest: valid_wstring(dest);
+    requires
+      room_for_concatenation:
+        \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
+    requires
+      separation:
+        \separated(
+          dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
+          );
+    ensures result_ptr: \result ≡ \old(dest);
     assigns *(dest + (0 ..)), \result;
     assigns *(dest + (0 ..))
       \from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
diff --git a/tests/libc/oracle/poll.res.oracle b/tests/libc/oracle/poll.res.oracle
index 11b20253b1a0df727f0356e029ddf671fa985eb0..311b9eca83445d6938754f8aefda746f0ba0efbb 100644
--- a/tests/libc/oracle/poll.res.oracle
+++ b/tests/libc/oracle/poll.res.oracle
@@ -13,6 +13,8 @@
 [eva] computing for function perror <- main.
   Called from tests/libc/poll.c:12.
 [eva] using specification for function perror
+[eva] tests/libc/poll.c:12: 
+  function perror: precondition 'valid_string_s' got status valid.
 [eva] Done for function perror
 [eva] Recording results for main
 [eva] done for function main
diff --git a/tests/libc/oracle/stdio_c.res.oracle b/tests/libc/oracle/stdio_c.res.oracle
index 40428842717797ef2180c0447d600f308ff4e75b..06ba2405258b9311bfeb5ca4f73196a063806ca0 100644
--- a/tests/libc/oracle/stdio_c.res.oracle
+++ b/tests/libc/oracle/stdio_c.res.oracle
@@ -17,18 +17,26 @@
 [eva] computing for function ferror <- getline <- main.
   Called from share/libc/stdio.c:46.
 [eva] using specification for function ferror
+[eva] share/libc/stdio.c:46: 
+  function ferror: precondition 'valid_stream' got status valid.
 [eva] Done for function ferror
 [eva] computing for function feof <- getline <- main.
   Called from share/libc/stdio.c:46.
 [eva] using specification for function feof
+[eva] share/libc/stdio.c:46: 
+  function feof: precondition 'valid_stream' got status valid.
 [eva] Done for function feof
 [eva] share/libc/stdio.c:51: Call to builtin malloc
 [eva] share/libc/stdio.c:51: allocating variable __malloc_getline_l51
 [eva] computing for function ferror <- getline <- main.
   Called from share/libc/stdio.c:60.
+[eva] share/libc/stdio.c:60: 
+  function ferror: precondition 'valid_stream' got status valid.
 [eva] Done for function ferror
 [eva] computing for function feof <- getline <- main.
   Called from share/libc/stdio.c:60.
+[eva] share/libc/stdio.c:60: 
+  function feof: precondition 'valid_stream' got status valid.
 [eva] Done for function feof
 [eva] computing for function fgetc <- getline <- main.
   Called from share/libc/stdio.c:62.
diff --git a/tests/libc/oracle/stdio_h.res.oracle b/tests/libc/oracle/stdio_h.res.oracle
index 267bfa3fb5cd00eb5c67fec3ee3113d8729ae044..8262aa6c408e46edf0fd8bb728cb16edf61af046 100644
--- a/tests/libc/oracle/stdio_h.res.oracle
+++ b/tests/libc/oracle/stdio_h.res.oracle
@@ -78,6 +78,22 @@
 [eva] tests/libc/stdio_h.c:31: 
   function fclose: precondition 'valid_stream' got status valid.
 [eva] Done for function fclose
+[eva] computing for function fgets <- main.
+  Called from tests/libc/stdio_h.c:34.
+[eva] using specification for function fgets
+[eva] tests/libc/stdio_h.c:34: 
+  function fgets: precondition 'valid_stream' got status valid.
+[eva] tests/libc/stdio_h.c:34: 
+  function fgets: precondition 'room_s' got status valid.
+[eva] Done for function fgets
+[eva:alarm] tests/libc/stdio_h.c:36: Warning: check got status unknown.
+[eva] computing for function fgets <- main.
+  Called from tests/libc/stdio_h.c:38.
+[eva] tests/libc/stdio_h.c:38: 
+  function fgets: precondition 'valid_stream' got status valid.
+[eva:alarm] tests/libc/stdio_h.c:38: Warning: 
+  function fgets: precondition 'room_s' got status invalid.
+[eva] Done for function fgets
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -89,5 +105,7 @@
   r ∈ [--..--]
   tmp_2 ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
   redirected ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
+  fgets_buf0[0] ∈ [--..--] or UNINITIALIZED
+  fgets_res ∈ {{ NULL ; &fgets_buf0[0] }}
   __retres ∈ {0; 1; 2; 3}
   S___fc_stdout[0..1] ∈ [--..--]
diff --git a/tests/libc/oracle/wchar_c_h.0.res.oracle b/tests/libc/oracle/wchar_c_h.0.res.oracle
index 67067c92b5680061e15983d06f22d8dd457234f0..8e6c444ee9de224d23eb1b8e1040a87196b79489 100644
--- a/tests/libc/oracle/wchar_c_h.0.res.oracle
+++ b/tests/libc/oracle/wchar_c_h.0.res.oracle
@@ -8,9 +8,30 @@
   t ∈ {0}
   nondet ∈ [--..--]
 [eva] tests/libc/wchar_c_h.c:31: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:31: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva] share/libc/wchar.h:58: 
+  Cannot evaluate range bound wmemchr_off(s, c, n)
+  (unsupported ACSL construct: logic function wmemchr_off). Approximating
+[eva] tests/libc/wchar_c_h.c:31: 
+  function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:31: 
+  function wmemchr: precondition 'danglingness' got status valid.
 [eva] computing for function wmemcmp <- main.
   Called from tests/libc/wchar_c_h.c:32.
 [eva] using specification for function wmemcmp
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'valid_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'valid_s2' got status valid.
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'initialization,s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'initialization,s2' got status valid.
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'danglingness,s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'danglingness,s2' got status valid.
 [eva] Done for function wmemcmp
 [eva] computing for function wmemcpy <- main.
   Called from tests/libc/wchar_c_h.c:33.
@@ -19,6 +40,10 @@
 [eva] computing for function wmemmove <- main.
   Called from tests/libc/wchar_c_h.c:34.
 [eva] using specification for function wmemmove
+[eva] tests/libc/wchar_c_h.c:34: 
+  function wmemmove: precondition 'valid_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:34: 
+  function wmemmove: precondition 'valid_dest' got status valid.
 [eva] Done for function wmemmove
 [eva] computing for function wmemset <- main.
   Called from tests/libc/wchar_c_h.c:35.
@@ -30,6 +55,10 @@
 [eva] computing for function wcscmp <- main.
   Called from tests/libc/wchar_c_h.c:37.
 [eva] using specification for function wcscmp
+[eva] tests/libc/wchar_c_h.c:37: 
+  function wcscmp: precondition 'valid_wstring_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:37: 
+  function wcscmp: precondition 'valid_wstring_s2' got status valid.
 [eva] Done for function wcscmp
 [eva] computing for function wcscpy <- main.
   Called from tests/libc/wchar_c_h.c:38.
@@ -38,14 +67,30 @@
 [eva] computing for function wcscspn <- main.
   Called from tests/libc/wchar_c_h.c:39.
 [eva] using specification for function wcscspn
+[eva] tests/libc/wchar_c_h.c:39: 
+  function wcscspn: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:39: 
+  function wcscspn: precondition 'valid_wstring_accept' got status valid.
 [eva] Done for function wcscspn
 [eva] computing for function wcslcat <- main.
   Called from tests/libc/wchar_c_h.c:40.
 [eva] using specification for function wcslcat
+[eva] tests/libc/wchar_c_h.c:40: 
+  function wcslcat: precondition 'valid_nwstring_src' got status valid.
+[eva:alarm] tests/libc/wchar_c_h.c:40: Warning: 
+  function wcslcat: precondition 'valid_wstring_dest' got status invalid.
+[eva] tests/libc/wchar_c_h.c:40: 
+  function wcslcat: no state left, precondition 'room_for_concatenation' got status valid.
+[eva] tests/libc/wchar_c_h.c:40: 
+  function wcslcat: no state left, precondition 'separation' got status valid.
 [eva] Done for function wcslcat
 [eva] computing for function wcslcpy <- main.
   Called from tests/libc/wchar_c_h.c:41.
 [eva] using specification for function wcslcpy
+[eva] tests/libc/wchar_c_h.c:41: 
+  function wcslcpy: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:41: 
+  function wcslcpy: precondition 'room_nwstring' got status valid.
 [eva] tests/libc/wchar_c_h.c:41: 
   function wcslcpy: precondition 'separation,dest,src' got status valid.
 [eva] Done for function wcslcpy
@@ -55,6 +100,10 @@
 [eva] computing for function wcsncmp <- main.
   Called from tests/libc/wchar_c_h.c:43.
 [eva] using specification for function wcsncmp
+[eva] tests/libc/wchar_c_h.c:43: 
+  function wcsncmp: precondition 'valid_wstring_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:43: 
+  function wcsncmp: precondition 'valid_wstring_s2' got status valid.
 [eva] Done for function wcsncmp
 [eva] computing for function wcsncpy <- main.
   Called from tests/libc/wchar_c_h.c:44.
@@ -63,18 +112,32 @@
 [eva] computing for function wcspbrk <- main.
   Called from tests/libc/wchar_c_h.c:45.
 [eva] using specification for function wcspbrk
+[eva] tests/libc/wchar_c_h.c:45: 
+  function wcspbrk: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:45: 
+  function wcspbrk: precondition 'valid_wstring_accept' got status valid.
 [eva] Done for function wcspbrk
 [eva] computing for function wcsrchr <- main.
   Called from tests/libc/wchar_c_h.c:46.
 [eva] using specification for function wcsrchr
+[eva] tests/libc/wchar_c_h.c:46: 
+  function wcsrchr: precondition 'valid_wstring_wcs' got status valid.
 [eva] Done for function wcsrchr
 [eva] computing for function wcsspn <- main.
   Called from tests/libc/wchar_c_h.c:47.
 [eva] using specification for function wcsspn
+[eva] tests/libc/wchar_c_h.c:47: 
+  function wcsspn: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:47: 
+  function wcsspn: precondition 'valid_wstring_accept' got status valid.
 [eva] Done for function wcsspn
 [eva] computing for function wcsstr <- main.
   Called from tests/libc/wchar_c_h.c:48.
 [eva] using specification for function wcsstr
+[eva] tests/libc/wchar_c_h.c:48: 
+  function wcsstr: precondition 'valid_wstring_haystack' got status valid.
+[eva] tests/libc/wchar_c_h.c:48: 
+  function wcsstr: precondition 'valid_wstring_needle' got status valid.
 [eva] Done for function wcsstr
 [eva] computing for function wcscat <- main.
   Called from tests/libc/wchar_c_h.c:52.
@@ -112,7 +175,19 @@
 [eva] tests/libc/wchar_c_h.c:68: 
   function wcschr: precondition 'valid_wstring_src' got status valid.
 [eva] tests/libc/wchar_c_h.c:69: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:69: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_c_h.c:69: 
+  function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:69: 
+  function wmemchr: precondition 'danglingness' got status valid.
 [eva] tests/libc/wchar_c_h.c:70: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:70: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_c_h.c:70: 
+  function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:70: 
+  function wmemchr: precondition 'danglingness' got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -174,7 +249,17 @@
 [eva:final-states] Values at end of function main:
   sc1 ∈ {{ L"Needle" }}
   sc2 ∈ {{ L"Haystack" }}
-  buf[0..19] ∈ [--..--] or UNINITIALIZED
+  buf[0..4] ∈ [--..--] or UNINITIALIZED
+     [5] ∈ {0; 72; 97; 115; 116; 121} or UNINITIALIZED
+     [6] ∈ {0; 97; 99; 115; 116; 121} or UNINITIALIZED
+     [7] ∈ {0; 97; 99; 107; 115; 116; 121} or UNINITIALIZED
+     [8] ∈ {0; 97; 99; 107; 115; 116} or UNINITIALIZED
+     [9] ∈ {0; 97; 99; 107; 116} or UNINITIALIZED
+     [10] ∈ {0; 97; 99; 107} or UNINITIALIZED
+     [11] ∈ {0; 99; 107} or UNINITIALIZED
+     [12] ∈ {0; 107} or UNINITIALIZED
+     [13] ∈ {0} or UNINITIALIZED
+     [14..19] ∈ UNINITIALIZED
   c ∈ [--..--]
   n ∈ {5}
   r ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/wchar_c_h.1.res.oracle b/tests/libc/oracle/wchar_c_h.1.res.oracle
index d90fa422c1726b48744c12ed9f5c4b199b9edb7b..8a8b446879fbfa8b923ba6416bbab050564219f2 100644
--- a/tests/libc/oracle/wchar_c_h.1.res.oracle
+++ b/tests/libc/oracle/wchar_c_h.1.res.oracle
@@ -8,23 +8,54 @@
   t ∈ {0}
   nondet ∈ [--..--]
 [eva] tests/libc/wchar_c_h.c:31: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:31: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva] share/libc/wchar.h:58: 
+  Cannot evaluate range bound wmemchr_off(s, c, n)
+  (unsupported ACSL construct: logic function wmemchr_off). Approximating
+[eva] tests/libc/wchar_c_h.c:31: 
+  function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:31: 
+  function wmemchr: precondition 'danglingness' got status valid.
 [eva] computing for function wmemcmp <- main.
   Called from tests/libc/wchar_c_h.c:32.
 [eva] using specification for function wmemcmp
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'valid_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'valid_s2' got status valid.
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'initialization,s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'initialization,s2' got status valid.
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'danglingness,s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:32: 
+  function wmemcmp: precondition 'danglingness,s2' got status valid.
 [eva] Done for function wmemcmp
 [eva] computing for function wmemcpy <- main.
   Called from tests/libc/wchar_c_h.c:33.
 [eva] using specification for function wmemcpy
+[eva] tests/libc/wchar_c_h.c:33: 
+  function wmemcpy: precondition 'valid_dest' got status valid.
+[eva] tests/libc/wchar_c_h.c:33: 
+  function wmemcpy: precondition 'valid_src' got status valid.
 [eva] tests/libc/wchar_c_h.c:33: 
   function wmemcpy: precondition 'separation,dest,src' got status valid.
 [eva] Done for function wmemcpy
 [eva] computing for function wmemmove <- main.
   Called from tests/libc/wchar_c_h.c:34.
 [eva] using specification for function wmemmove
+[eva] tests/libc/wchar_c_h.c:34: 
+  function wmemmove: precondition 'valid_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:34: 
+  function wmemmove: precondition 'valid_dest' got status valid.
 [eva] Done for function wmemmove
 [eva] computing for function wmemset <- main.
   Called from tests/libc/wchar_c_h.c:35.
 [eva] using specification for function wmemset
+[eva] tests/libc/wchar_c_h.c:35: 
+  function wmemset: precondition 'valid_wcs' got status valid.
 [eva] Done for function wmemset
 [eva] tests/libc/wchar_c_h.c:36: Call to builtin wcschr
 [eva] tests/libc/wchar_c_h.c:36: 
@@ -32,22 +63,48 @@
 [eva] computing for function wcscmp <- main.
   Called from tests/libc/wchar_c_h.c:37.
 [eva] using specification for function wcscmp
+[eva] tests/libc/wchar_c_h.c:37: 
+  function wcscmp: precondition 'valid_wstring_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:37: 
+  function wcscmp: precondition 'valid_wstring_s2' got status valid.
 [eva] Done for function wcscmp
 [eva] computing for function wcscpy <- main.
   Called from tests/libc/wchar_c_h.c:38.
 [eva] using specification for function wcscpy
+[eva] tests/libc/wchar_c_h.c:38: 
+  function wcscpy: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:38: 
+  function wcscpy: precondition 'room_wstring' got status valid.
+[eva] tests/libc/wchar_c_h.c:38: 
+  function wcscpy: precondition 'separation' got status valid.
 [eva] Done for function wcscpy
 [eva] computing for function wcscspn <- main.
   Called from tests/libc/wchar_c_h.c:39.
 [eva] using specification for function wcscspn
+[eva] tests/libc/wchar_c_h.c:39: 
+  function wcscspn: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:39: 
+  function wcscspn: precondition 'valid_wstring_accept' got status valid.
 [eva] Done for function wcscspn
 [eva] computing for function wcslcat <- main.
   Called from tests/libc/wchar_c_h.c:40.
 [eva] using specification for function wcslcat
+[eva] tests/libc/wchar_c_h.c:40: 
+  function wcslcat: precondition 'valid_nwstring_src' got status valid.
+[eva:alarm] tests/libc/wchar_c_h.c:40: Warning: 
+  function wcslcat: precondition 'valid_wstring_dest' got status invalid.
+[eva] tests/libc/wchar_c_h.c:40: 
+  function wcslcat: no state left, precondition 'room_for_concatenation' got status valid.
+[eva] tests/libc/wchar_c_h.c:40: 
+  function wcslcat: no state left, precondition 'separation' got status valid.
 [eva] Done for function wcslcat
 [eva] computing for function wcslcpy <- main.
   Called from tests/libc/wchar_c_h.c:41.
 [eva] using specification for function wcslcpy
+[eva] tests/libc/wchar_c_h.c:41: 
+  function wcslcpy: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:41: 
+  function wcslcpy: precondition 'room_nwstring' got status valid.
 [eva] tests/libc/wchar_c_h.c:41: 
   function wcslcpy: precondition 'separation,dest,src' got status valid.
 [eva] Done for function wcslcpy
@@ -57,36 +114,74 @@
 [eva] computing for function wcsncmp <- main.
   Called from tests/libc/wchar_c_h.c:43.
 [eva] using specification for function wcsncmp
+[eva] tests/libc/wchar_c_h.c:43: 
+  function wcsncmp: precondition 'valid_wstring_s1' got status valid.
+[eva] tests/libc/wchar_c_h.c:43: 
+  function wcsncmp: precondition 'valid_wstring_s2' got status valid.
 [eva] Done for function wcsncmp
 [eva] computing for function wcsncpy <- main.
   Called from tests/libc/wchar_c_h.c:44.
 [eva] using specification for function wcsncpy
+[eva] tests/libc/wchar_c_h.c:44: 
+  function wcsncpy: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:44: 
+  function wcsncpy: precondition 'room_nwstring' got status valid.
 [eva] tests/libc/wchar_c_h.c:44: 
   function wcsncpy: precondition 'separation,dest,src' got status valid.
 [eva] Done for function wcsncpy
 [eva] computing for function wcspbrk <- main.
   Called from tests/libc/wchar_c_h.c:45.
 [eva] using specification for function wcspbrk
+[eva] tests/libc/wchar_c_h.c:45: 
+  function wcspbrk: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:45: 
+  function wcspbrk: precondition 'valid_wstring_accept' got status valid.
 [eva] Done for function wcspbrk
 [eva] computing for function wcsrchr <- main.
   Called from tests/libc/wchar_c_h.c:46.
 [eva] using specification for function wcsrchr
+[eva] tests/libc/wchar_c_h.c:46: 
+  function wcsrchr: precondition 'valid_wstring_wcs' got status valid.
 [eva] Done for function wcsrchr
 [eva] computing for function wcsspn <- main.
   Called from tests/libc/wchar_c_h.c:47.
 [eva] using specification for function wcsspn
+[eva] tests/libc/wchar_c_h.c:47: 
+  function wcsspn: precondition 'valid_wstring_wcs' got status valid.
+[eva] tests/libc/wchar_c_h.c:47: 
+  function wcsspn: precondition 'valid_wstring_accept' got status valid.
 [eva] Done for function wcsspn
 [eva] computing for function wcsstr <- main.
   Called from tests/libc/wchar_c_h.c:48.
 [eva] using specification for function wcsstr
+[eva] tests/libc/wchar_c_h.c:48: 
+  function wcsstr: precondition 'valid_wstring_haystack' got status valid.
+[eva] tests/libc/wchar_c_h.c:48: 
+  function wcsstr: precondition 'valid_wstring_needle' got status valid.
 [eva] Done for function wcsstr
 [eva] computing for function wcscat <- main.
   Called from tests/libc/wchar_c_h.c:52.
 [eva] using specification for function wcscat
+[eva] tests/libc/wchar_c_h.c:52: 
+  function wcscat: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:52: 
+  function wcscat: precondition 'valid_wstring_dest' got status valid.
+[eva] tests/libc/wchar_c_h.c:52: 
+  function wcscat: precondition 'room_for_concatenation' got status valid.
+[eva] tests/libc/wchar_c_h.c:52: 
+  function wcscat: precondition 'separation' got status valid.
 [eva] Done for function wcscat
 [eva] computing for function wcsncat <- main.
   Called from tests/libc/wchar_c_h.c:54.
 [eva] using specification for function wcsncat
+[eva] tests/libc/wchar_c_h.c:54: 
+  function wcsncat: precondition 'valid_nwstring_src' got status valid.
+[eva] tests/libc/wchar_c_h.c:54: 
+  function wcsncat: precondition 'valid_wstring_dest' got status valid.
+[eva] tests/libc/wchar_c_h.c:54: 
+  function wcsncat: precondition 'room_for_concatenation' got status valid.
+[eva] tests/libc/wchar_c_h.c:54: 
+  function wcsncat: precondition 'separation' got status valid.
 [eva] Done for function wcsncat
 [eva] tests/libc/wchar_c_h.c:57: Call to builtin wcslen
 [eva:alarm] tests/libc/wchar_c_h.c:57: Warning: 
@@ -110,7 +205,19 @@
 [eva] tests/libc/wchar_c_h.c:68: 
   function wcschr: precondition 'valid_wstring_src' got status valid.
 [eva] tests/libc/wchar_c_h.c:69: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:69: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_c_h.c:69: 
+  function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:69: 
+  function wmemchr: precondition 'danglingness' got status valid.
 [eva] tests/libc/wchar_c_h.c:70: Call to builtin wmemchr
+[eva] tests/libc/wchar_c_h.c:70: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_c_h.c:70: 
+  function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_c_h.c:70: 
+  function wmemchr: precondition 'danglingness' got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/wchar_h.res.oracle b/tests/libc/oracle/wchar_h.res.oracle
index e1161566c7fd14a4c7f27edfa0bad2ff7818e2b3..2ffbd071fc836e2895f3dcf5ae60d6a8f06b29ec 100644
--- a/tests/libc/oracle/wchar_h.res.oracle
+++ b/tests/libc/oracle/wchar_h.res.oracle
@@ -3,7 +3,7 @@
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  
+  v ∈ [--..--]
 [eva] computing for function fopen <- main.
   Called from tests/libc/wchar_h.c:5.
 [eva] using specification for function fopen
@@ -15,15 +15,196 @@
 [eva] computing for function fgetws <- main.
   Called from tests/libc/wchar_h.c:8.
 [eva] using specification for function fgetws
+[eva] tests/libc/wchar_h.c:8: 
+  function fgetws: precondition 'room_nwstring' got status valid.
 [eva] tests/libc/wchar_h.c:8: 
   function fgetws: precondition 'valid_stream' got status valid.
 [eva] Done for function fgetws
 [eva] tests/libc/wchar_h.c:10: assertion got status valid.
+[eva] tests/libc/wchar_h.c:13: Call to builtin wmemchr
+[eva] tests/libc/wchar_h.c:13: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva] share/libc/wchar.h:58: 
+  Cannot evaluate range bound wmemchr_off(s, c, n)
+  (unsupported ACSL construct: logic function wmemchr_off). Approximating
+[eva:alarm] tests/libc/wchar_h.c:13: Warning: 
+  function wmemchr: precondition 'initialization' got status unknown.
+[eva] tests/libc/wchar_h.c:13: 
+  function wmemchr: precondition 'danglingness' got status valid.
+[eva] tests/libc/wchar_h.c:14: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:15: Call to builtin wmemchr
+[eva] share/libc/wchar.h:55: 
+  Cannot evaluate range bound wmemchr_off(s, c, n)
+  (unsupported ACSL construct: logic function wmemchr_off). Approximating
+[eva:alarm] tests/libc/wchar_h.c:15: Warning: 
+  function wmemchr: precondition 'valid' got status unknown.
+[eva] tests/libc/wchar_h.c:15: 
+  function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_h.c:15: 
+  function wmemchr: precondition 'danglingness' got status valid.
+[eva] tests/libc/wchar_h.c:16: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:18: Call to builtin wmemchr
+[eva] tests/libc/wchar_h.c:18: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:18: Warning: 
+  function wmemchr: precondition 'initialization' got status unknown.
+[eva] tests/libc/wchar_h.c:18: 
+  function wmemchr: precondition 'danglingness' got status valid.
+[eva] tests/libc/wchar_h.c:21: Call to builtin wmemchr
+[eva:alarm] tests/libc/wchar_h.c:21: Warning: 
+  function wmemchr: precondition 'valid' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:21: Warning: 
+  function wmemchr: precondition 'initialization' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:21: Warning: 
+  function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:22: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:24: Call to builtin wmemchr
+[eva:alarm] tests/libc/wchar_h.c:24: Warning: 
+  function wmemchr: precondition 'valid' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:24: Warning: 
+  function wmemchr: precondition 'initialization' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:24: Warning: 
+  function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:25: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:26: Call to builtin wmemchr
+[eva:alarm] tests/libc/wchar_h.c:26: Warning: 
+  function wmemchr: precondition 'valid' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:26: Warning: 
+  function wmemchr: precondition 'initialization' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:26: Warning: 
+  function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:27: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:29: Call to builtin wmemchr
+[eva:alarm] tests/libc/wchar_h.c:29: Warning: 
+  function wmemchr: precondition 'valid' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:29: Warning: 
+  function wmemchr: precondition 'initialization' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:29: Warning: 
+  function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:30: check 'ok' got status valid.
+[eva] computing for function wcsncpy <- main.
+  Called from tests/libc/wchar_h.c:33.
+[eva] using specification for function wcsncpy
+[eva] tests/libc/wchar_h.c:33: 
+  function wcsncpy: precondition 'valid_wstring_src' got status valid.
+[eva] tests/libc/wchar_h.c:33: 
+  function wcsncpy: precondition 'room_nwstring' got status valid.
+[eva] tests/libc/wchar_h.c:33: 
+  function wcsncpy: precondition 'separation,dest,src' got status valid.
+[eva] Done for function wcsncpy
+[eva] tests/libc/wchar_h.c:34: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:35: check 'ok' got status valid.
+[eva] tests/libc/wchar_h.c:37: Call to builtin wcslen
+[eva] tests/libc/wchar_h.c:37: 
+  function wcslen: precondition 'valid_string_s' got status valid.
+[eva] computing for function wcsncpy <- main.
+  Called from tests/libc/wchar_h.c:37.
+[eva] tests/libc/wchar_h.c:37: 
+  function wcsncpy: precondition 'valid_wstring_src' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:37: Warning: 
+  function wcsncpy: precondition 'room_nwstring' got status invalid.
+[eva] tests/libc/wchar_h.c:37: 
+  function wcsncpy: no state left, precondition 'separation,dest,src' got status valid.
+[eva] Done for function wcsncpy
+[eva] computing for function wcsncpy <- main.
+  Called from tests/libc/wchar_h.c:41.
+[eva:alarm] tests/libc/wchar_h.c:41: Warning: 
+  function wcsncpy: precondition 'valid_wstring_src' got status unknown.
+[eva] tests/libc/wchar_h.c:41: 
+  function wcsncpy: precondition 'room_nwstring' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:41: Warning: 
+  function wcsncpy: precondition 'separation,dest,src' got status invalid.
+[eva] Done for function wcsncpy
+[eva] computing for function wcsncpy <- main.
+  Called from tests/libc/wchar_h.c:45.
+[eva] tests/libc/wchar_h.c:45: 
+  function wcsncpy: precondition 'valid_wstring_src' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:45: Warning: 
+  function wcsncpy: precondition 'room_nwstring' got status invalid.
+[eva] tests/libc/wchar_h.c:45: 
+  function wcsncpy: no state left, precondition 'separation,dest,src' got status valid.
+[eva] Done for function wcsncpy
+[eva] computing for function wcsncpy <- main.
+  Called from tests/libc/wchar_h.c:49.
+[eva:alarm] tests/libc/wchar_h.c:49: Warning: 
+  function wcsncpy: precondition 'valid_wstring_src' got status invalid.
+[eva] tests/libc/wchar_h.c:49: 
+  function wcsncpy: no state left, precondition 'room_nwstring' got status valid.
+[eva] tests/libc/wchar_h.c:49: 
+  function wcsncpy: no state left, precondition 'separation,dest,src' got status valid.
+[eva] Done for function wcsncpy
+[eva] computing for function wcsncpy <- main.
+  Called from tests/libc/wchar_h.c:53.
+[eva:alarm] tests/libc/wchar_h.c:53: Warning: 
+  function wcsncpy: precondition 'valid_wstring_src' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:53: Warning: 
+  function wcsncpy: precondition 'room_nwstring' got status invalid.
+[eva] tests/libc/wchar_h.c:53: 
+  function wcsncpy: no state left, precondition 'separation,dest,src' got status valid.
+[eva] Done for function wcsncpy
+[eva] computing for function wcsncmp <- main.
+  Called from tests/libc/wchar_h.c:56.
+[eva] using specification for function wcsncmp
+[eva] tests/libc/wchar_h.c:56: 
+  function wcsncmp: precondition 'valid_wstring_s1' got status valid.
+[eva] tests/libc/wchar_h.c:56: 
+  function wcsncmp: precondition 'valid_wstring_s2' got status valid.
+[eva] Done for function wcsncmp
+[eva] computing for function wcsncmp <- main.
+  Called from tests/libc/wchar_h.c:57.
+[eva] tests/libc/wchar_h.c:57: 
+  function wcsncmp: precondition 'valid_wstring_s1' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:57: Warning: 
+  function wcsncmp: precondition 'valid_wstring_s2' got status unknown.
+[eva] Done for function wcsncmp
+[eva] computing for function wcsncat <- main.
+  Called from tests/libc/wchar_h.c:59.
+[eva] using specification for function wcsncat
+[eva] tests/libc/wchar_h.c:59: 
+  function wcsncat: precondition 'valid_nwstring_src' got status valid.
+[eva] tests/libc/wchar_h.c:59: 
+  function wcsncat: precondition 'valid_wstring_dest' got status valid.
+[eva] tests/libc/wchar_h.c:59: 
+  function wcsncat: precondition 'room_for_concatenation' got status valid.
+[eva] tests/libc/wchar_h.c:59: 
+  function wcsncat: precondition 'separation' got status valid.
+[eva] Done for function wcsncat
+[eva] computing for function wcsncat <- main.
+  Called from tests/libc/wchar_h.c:60.
+[eva] tests/libc/wchar_h.c:60: 
+  function wcsncat: precondition 'valid_nwstring_src' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:60: Warning: 
+  function wcsncat: precondition 'valid_wstring_dest' got status unknown.
+[eva:alarm] tests/libc/wchar_h.c:60: Warning: 
+  function wcsncat: precondition 'room_for_concatenation' got status unknown.
+[eva] tests/libc/wchar_h.c:60: 
+  function wcsncat: precondition 'separation' got status valid.
+[eva] Done for function wcsncat
+[eva] computing for function wcsncat <- main.
+  Called from tests/libc/wchar_h.c:66.
+[eva] tests/libc/wchar_h.c:66: 
+  function wcsncat: precondition 'valid_nwstring_src' got status valid.
+[eva] tests/libc/wchar_h.c:66: 
+  function wcsncat: precondition 'valid_wstring_dest' got status valid.
+[eva:alarm] tests/libc/wchar_h.c:66: Warning: 
+  function wcsncat: precondition 'room_for_concatenation' got status invalid.
+[eva] tests/libc/wchar_h.c:66: 
+  function wcsncat: no state left, precondition 'separation' got status valid.
+[eva] Done for function wcsncat
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   fd ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
-  buf[0..29] ∈ [--..--] or UNINITIALIZED
+  buf[0..28] ∈ [--..--] or UNINITIALIZED
+     [29] ∈ UNINITIALIZED
   res ∈ {{ NULL ; &buf[0] }}
+  buf2[0] ∈ {97} or UNINITIALIZED
+      [1] ∈ {98} or UNINITIALIZED
+  r ∈ {{ &wdst[0] }}
+  wsrc ∈ {{ L"wide thing" }}
+  wdst[0..9] ∈ [--..--] or UNINITIALIZED
+  wdst2[0..9] ∈ {65}
+       [10] ∈ {0}
+       [11..19] ∈ [--..--]
   __retres ∈ {0; 1}
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index fe5023c92a121cd742479c4988f5163e4386ec40..9c9da490751c46d4be61d72f0e1ecfdbdb85258d 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -114,6 +114,10 @@
             Unverifiable but considered Valid.
 [ Extern  ] Axiom 'wcsncmp_zero'
             Unverifiable but considered Valid.
+[ Extern  ] Axiom 'wmemchr_def'
+            Unverifiable but considered Valid.
+[  Valid  ] Axiomatic 'GetsLength'
+            by Frama-C kernel.
 [  Valid  ] Axiomatic 'MemChr'
             by Frama-C kernel.
 [  Valid  ] Axiomatic 'MemCmp'
@@ -128,6 +132,8 @@
             by Frama-C kernel.
 [  Valid  ] Axiomatic 'StrNCmp'
             by Frama-C kernel.
+[  Valid  ] Axiomatic 'WMemChr'
+            by Frama-C kernel.
 [  Valid  ] Axiomatic 'WcsChr'
             by Frama-C kernel.
 [  Valid  ] Axiomatic 'WcsCmp'
@@ -365,14 +371,16 @@
 
 [ Extern  ] Post-condition 'result_null_or_same'
             Unverifiable but considered Valid.
-[ Extern  ] Post-condition 'terminated_string_on_success'
+[ Extern  ] Post-condition 'initialization,at_least_one'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 225)
+[ Extern  ] Post-condition 'terminated_string_on_success'
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 225)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 226)
             Unverifiable but considered Valid.
 [ Extern  ] Froms (file share/libc/stdio.h, line 226)
             Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 227)
+            Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
 
@@ -380,7 +388,7 @@
 --- Properties of Function 'fputc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 234)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 238)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -389,9 +397,9 @@
 --- Properties of Function 'fputs'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 237)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 241)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 237)
+[ Extern  ] Froms (file share/libc/stdio.h, line 241)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -400,11 +408,11 @@
 --- Properties of Function 'getc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 241)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 245)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 241)
+[ Extern  ] Froms (file share/libc/stdio.h, line 245)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 241)
+[ Extern  ] Froms (file share/libc/stdio.h, line 245)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -415,7 +423,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 244)
+[ Extern  ] Froms (file share/libc/stdio.h, line 248)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -426,11 +434,13 @@
 
 [ Extern  ] Post-condition 'result_null_or_same'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 248)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 260)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 248)
+[ Extern  ] Froms (file share/libc/stdio.h, line 260)
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/stdio.h, line 261)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 249)
+[ Extern  ] Froms (file share/libc/stdio.h, line 262)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -439,9 +449,9 @@
 --- Properties of Function 'putc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 254)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 269)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 254)
+[ Extern  ] Froms (file share/libc/stdio.h, line 269)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -450,9 +460,9 @@
 --- Properties of Function 'putchar'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 257)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 273)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 257)
+[ Extern  ] Froms (file share/libc/stdio.h, line 273)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -461,9 +471,9 @@
 --- Properties of Function 'puts'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 260)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 276)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 260)
+[ Extern  ] Froms (file share/libc/stdio.h, line 276)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -472,9 +482,9 @@
 --- Properties of Function 'ungetc'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 263)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 281)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 263)
+[ Extern  ] Froms (file share/libc/stdio.h, line 281)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -487,11 +497,11 @@
             Unverifiable but considered Valid.
 [ Extern  ] Post-condition 'initialization'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 269)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 288)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 269)
+[ Extern  ] Froms (file share/libc/stdio.h, line 288)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 270)
+[ Extern  ] Froms (file share/libc/stdio.h, line 289)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -502,11 +512,11 @@
 
 [ Extern  ] Post-condition 'size_written'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 282)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 301)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 282)
+[ Extern  ] Froms (file share/libc/stdio.h, line 301)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 282)
+[ Extern  ] Froms (file share/libc/stdio.h, line 301)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -515,9 +525,9 @@
 --- Properties of Function 'fgetpos'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 290)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 309)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 290)
+[ Extern  ] Froms (file share/libc/stdio.h, line 309)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -526,13 +536,13 @@
 --- Properties of Function 'fseek'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 297)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 316)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 297)
+[ Extern  ] Froms (file share/libc/stdio.h, line 316)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 298)
+[ Extern  ] Froms (file share/libc/stdio.h, line 317)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 298)
+[ Extern  ] Froms (file share/libc/stdio.h, line 317)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -541,9 +551,9 @@
 --- Properties of Function 'fsetpos'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 303)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 322)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 303)
+[ Extern  ] Froms (file share/libc/stdio.h, line 322)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -554,11 +564,11 @@
 
 [ Extern  ] Post-condition 'success_or_error'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 308)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 327)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 308)
+[ Extern  ] Froms (file share/libc/stdio.h, line 327)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 308)
+[ Extern  ] Froms (file share/libc/stdio.h, line 327)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -567,9 +577,9 @@
 --- Properties of Function 'rewind'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 314)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 335)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 314)
+[ Extern  ] Froms (file share/libc/stdio.h, line 335)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -578,9 +588,9 @@
 --- Properties of Function 'clearerr'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 317)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 341)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 317)
+[ Extern  ] Froms (file share/libc/stdio.h, line 341)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -591,7 +601,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 320)
+[ Extern  ] Froms (file share/libc/stdio.h, line 347)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -602,7 +612,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 323)
+[ Extern  ] Froms (file share/libc/stdio.h, line 353)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -611,9 +621,9 @@
 --- Properties of Function 'flockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 326)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 359)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 326)
+[ Extern  ] Froms (file share/libc/stdio.h, line 359)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -622,9 +632,9 @@
 --- Properties of Function 'funlockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 329)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 365)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 329)
+[ Extern  ] Froms (file share/libc/stdio.h, line 365)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -633,11 +643,11 @@
 --- Properties of Function 'ftrylockfile'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 332)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 371)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 332)
+[ Extern  ] Froms (file share/libc/stdio.h, line 371)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 332)
+[ Extern  ] Froms (file share/libc/stdio.h, line 371)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -648,7 +658,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 335)
+[ Extern  ] Froms (file share/libc/stdio.h, line 377)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -657,9 +667,9 @@
 --- Properties of Function 'perror'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 338)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 383)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 338)
+[ Extern  ] Froms (file share/libc/stdio.h, line 383)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -668,11 +678,11 @@
 --- Properties of Function 'getc_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 341)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 389)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 341)
+[ Extern  ] Froms (file share/libc/stdio.h, line 389)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 341)
+[ Extern  ] Froms (file share/libc/stdio.h, line 389)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -683,7 +693,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 343)
+[ Extern  ] Froms (file share/libc/stdio.h, line 392)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -692,9 +702,9 @@
 --- Properties of Function 'putc_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 345)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 397)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 345)
+[ Extern  ] Froms (file share/libc/stdio.h, line 397)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -703,9 +713,9 @@
 --- Properties of Function 'putchar_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 347)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 401)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 347)
+[ Extern  ] Froms (file share/libc/stdio.h, line 401)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -714,9 +724,9 @@
 --- Properties of Function 'clearerr_unlocked'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Assigns (file share/libc/stdio.h, line 350)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 406)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 350)
+[ Extern  ] Froms (file share/libc/stdio.h, line 406)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -727,7 +737,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 352)
+[ Extern  ] Froms (file share/libc/stdio.h, line 412)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -738,7 +748,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 354)
+[ Extern  ] Froms (file share/libc/stdio.h, line 418)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -749,7 +759,7 @@
 
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 356)
+[ Extern  ] Froms (file share/libc/stdio.h, line 424)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -760,11 +770,11 @@
 
 [ Extern  ] Post-condition 'result_error_or_valid_open_pipe'
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/stdio.h, line 381)
+[ Extern  ] Assigns (file share/libc/stdio.h, line 451)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 381)
+[ Extern  ] Froms (file share/libc/stdio.h, line 451)
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 383)
+[ Extern  ] Froms (file share/libc/stdio.h, line 453)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -777,7 +787,7 @@
             Unverifiable but considered Valid.
 [ Extern  ] Assigns nothing
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/stdio.h, line 395)
+[ Extern  ] Froms (file share/libc/stdio.h, line 465)
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             by Frama-C kernel.
@@ -796,8 +806,8 @@
 --------------------------------------------------------------------------------
 --- Status Report Summary
 --------------------------------------------------------------------------------
-    68 Completely validated
-   168 Considered valid
+    70 Completely validated
+   171 Considered valid
      1 To be validated
-   237 Total
+   242 Total
 --------------------------------------------------------------------------------