diff --git a/tests/basic/oracle/aggregate.res.oracle b/tests/basic/oracle/aggregate.res.oracle
index 09fb0cd80c82ac3ff80569aec7085038f46c5dff..159a4fd18197753d46736564862e98ada2b53816 100644
--- a/tests/basic/oracle/aggregate.res.oracle
+++ b/tests/basic/oracle/aggregate.res.oracle
@@ -108,10 +108,18 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
    .number_of_base_classes = 0,
    .pvmt = (struct _frama_c_vmt *)0};
+void B::Dtor(struct B const *this);
+
 struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
 struct _frama_c_vmt_content _frama_c_vmt[1];
+/*@ requires \valid_read(this); */
+void B::Dtor(struct B const *this)
+{
+  return;
+}
+
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "B",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index 8499f5341bb63b3aeb215a3abcc4246b4aba8ec8..d47b5e1f7ba30149b9a18edf5f4952d4d7015f0b 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -270,6 +270,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(int *s) 
     reads *(s + (0 ..));
@@ -827,10 +844,6 @@ void *calloc(size_t nmemb, size_t size);
  */
 void *realloc(void *ptr, size_t size);
 
-/*@ ensures never_terminates: \false;
-    assigns \nothing; */
-void abort(void);
-
 /*@ assigns \result;
     assigns \result \from \nothing; */
 int atexit(void (*func)(void));
@@ -839,10 +852,6 @@ int atexit(void (*func)(void));
     assigns \result \from \nothing; */
 int at_quick_exit(void (*func)(void));
 
-/*@ ensures never_terminates: \false;
-    assigns \nothing; */
-void exit(int status);
-
 /*@ ensures never_terminates: \false;
     assigns \nothing; */
 void _Exit(int status);
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index 2478a686c29ae90162e1b695caea5cc0e4cdb9b3..b0e3e6886d6cf469b5928ae283a7ea709cda43d6 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -239,6 +239,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(int *s) 
     reads *(s + (0 ..));
@@ -796,10 +813,6 @@ void *calloc(size_t nmemb, size_t size);
  */
 void *realloc(void *ptr, size_t size);
 
-/*@ ensures never_terminates: \false;
-    assigns \nothing; */
-void abort(void);
-
 /*@ assigns \result;
     assigns \result \from \nothing; */
 int atexit(void (*func)(void));
@@ -808,10 +821,6 @@ int atexit(void (*func)(void));
     assigns \result \from \nothing; */
 int at_quick_exit(void (*func)(void));
 
-/*@ ensures never_terminates: \false;
-    assigns \nothing; */
-void exit(int status);
-
 /*@ ensures never_terminates: \false;
     assigns \nothing; */
 void _Exit(int status);
diff --git a/tests/basic/oracle/ptr_array_decls.res.oracle b/tests/basic/oracle/ptr_array_decls.res.oracle
index b81974baace76487f555d643d858b1da425ee199..d63d204f80a2c687e87e4bef153c5b8aefab318c 100644
--- a/tests/basic/oracle/ptr_array_decls.res.oracle
+++ b/tests/basic/oracle/ptr_array_decls.res.oracle
@@ -26,10 +26,18 @@ struct S0 {
    int f0 ;
    int f1 ;
 };
+void S0::Dtor(struct S0 const *this);
+
 struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
 struct _frama_c_vmt_content _frama_c_vmt[1];
+/*@ requires \valid_read(this); */
+void S0::Dtor(struct S0 const *this)
+{
+  return;
+}
+
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "S0",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
diff --git a/tests/basic/oracle/static_1.res.oracle b/tests/basic/oracle/static_1.res.oracle
index 16deb3df71fcc29c21306983ef841e8d6a671f6a..f6602e9e1d54c96dc7c08c408cd0c32ddfb64f0e 100644
--- a/tests/basic/oracle/static_1.res.oracle
+++ b/tests/basic/oracle/static_1.res.oracle
@@ -50,7 +50,8 @@ int Sm_get(void);
 static int x;
 /*@ assigns \result;
     assigns \result
-      \from (indirect: *(__frama_c_arg_0 + (0 ..))), param1, param0;
+      \from (indirect: *(__frama_c_arg_0 + (0 ..))), (indirect: param1),
+            (indirect: param0);
  */
 int printf_va_1(char const *__frama_c_arg_0, int param0, int param1);
 
diff --git a/tests/bugs/oracle/issue11.res.oracle b/tests/bugs/oracle/issue11.res.oracle
index ad84c99eb9025f3fed969dd44d4af5eafd6b693b..4aea35528b7fd3009e061b7f14020eb92c1f7e8b 100644
--- a/tests/bugs/oracle/issue11.res.oracle
+++ b/tests/bugs/oracle/issue11.res.oracle
@@ -5,6 +5,7 @@ Now output intermediate result
 [wp] 2 goals scheduled
 [wp] [Qed] Goal typed___fc_init_ZN1aE1d_call__ZN1a1bIcEEC1v_ZN1a1bIcEEC1v_requires : Valid
 [wp] [Qed] Goal typed___fc_init_ZN1aE1c_call__ZN1a1bIvEEC1v_ZN1a1bIvEEC1v_requires : Valid
+[wp] [Cache] not used
 [wp] Proved goals:    2 / 2
   Qed:             2
 /* Generated by Frama-C */
diff --git a/tests/bugs/oracle/issue23.res.oracle b/tests/bugs/oracle/issue23.res.oracle
index 8d7efd4fd7dffe99612c6917c8c342a025639e1d..fe474be8bfa4f1c87a677020433294cab84ce90a 100644
--- a/tests/bugs/oracle/issue23.res.oracle
+++ b/tests/bugs/oracle/issue23.res.oracle
@@ -5,6 +5,7 @@ Now output intermediate result
 [wp] 2 goals scheduled
 [wp] [Qed] Goal typed_Z1m_assert_2 : Valid
 [wp] [Qed] Goal typed_Z1m_assert : Valid
+[wp] [Cache] not used
 [wp] Proved goals:    2 / 2
   Qed:             2
 /* Generated by Frama-C */
diff --git a/tests/bugs/oracle/issue24.res.oracle b/tests/bugs/oracle/issue24.res.oracle
index 2104e5f6a16333cbf9233399fbe943fc17d9af41..8ea826cb0780c57de410a3a1bf55a6b737398b40 100644
--- a/tests/bugs/oracle/issue24.res.oracle
+++ b/tests/bugs/oracle/issue24.res.oracle
@@ -5,10 +5,11 @@ Now output intermediate result
 [wp] 6 goals scheduled
 [wp] [Qed] Goal typed_Z1m_assert_4 : Valid
 [wp] [Qed] Goal typed_Z1m_assert_5 : Valid
-[wp] [Alt-Ergo] Goal typed_Z1m_assert_3 : Valid
-[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid
-[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid
-[wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_3 : Valid (5)
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid (4)
+[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid (3)
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid (6)
+[wp] [Cache] updated:4
 [wp] Proved goals:    6 / 6
   Qed:               2 
   Alt-Ergo:    4  (6)
diff --git a/tests/bugs/oracle/issue27-pred.res.oracle b/tests/bugs/oracle/issue27-pred.res.oracle
index 10a0fb31ed77d6240c162bc9e2ece814d9ed764d..1ab770b4e10ae6d150288a42a89d5f498c746a69 100644
--- a/tests/bugs/oracle/issue27-pred.res.oracle
+++ b/tests/bugs/oracle/issue27-pred.res.oracle
@@ -3,8 +3,9 @@ Now output intermediate result
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid
 [wp] [Alt-Ergo] Goal typed_Z3posi_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid (7)
+[wp] [Cache] updated:1
 [wp] Proved goals:    2 / 2
   Qed:               0 
   Alt-Ergo:    2  (7)
diff --git a/tests/bugs/oracle/logiccast.res.oracle b/tests/bugs/oracle/logiccast.res.oracle
index 55da24612f9dba71c1017b24a765c1212b65158e..565d61b3af0619633e4dc232fb1569e3b3d4261d 100644
--- a/tests/bugs/oracle/logiccast.res.oracle
+++ b/tests/bugs/oracle/logiccast.res.oracle
@@ -3,15 +3,16 @@ Now output intermediate result
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unknown
 [wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Unknown
+[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unknown
+[wp] [Cache] updated:2
 [wp] Proved goals:    0 / 2
   Alt-Ergo:    0  (unknown: 2)
 [wp] Warning: Memory model hypotheses for function '_Z1mPv':
-  /*@ behavior typed: requires \separated(&base,r); */
+  /*@ behavior typed: requires \separated(&base,r+(..)); */
   void _Z1mPv(void *r);
 [wp] Warning: Memory model hypotheses for function '_Z1nPc':
-  /*@ behavior typed: requires \separated(&base,r); */
+  /*@ behavior typed: requires \separated(&base,r+(..)); */
   void _Z1nPc(char *r);
 /* Generated by Frama-C */
 char *base;
diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle
index a3d27a6d1e75ae51b2de8892a0a42eaf111d94cd..4c75afb853de8203fc3b6052579d3475cd22d6b1 100644
--- a/tests/bugs/oracle/term.res.oracle
+++ b/tests/bugs/oracle/term.res.oracle
@@ -9,6 +9,7 @@ Now output intermediate result
 [wp] [Qed] Goal typed_Z3m3a_c_ensures : Valid
 [wp] [Qed] Goal typed_Z2m3_c_ensures : Valid
 [wp] [Qed] Goal typed_Z2m2_ensures : Valid
+[wp] [Cache] not used
 [wp] Proved goals:    3 / 3
   Qed:             3
 /* Generated by Frama-C */
diff --git a/tests/class/oracle/array_object_bts1739.res.oracle b/tests/class/oracle/array_object_bts1739.res.oracle
index 3a103a88917dc27f458aa0c875b3ac41d57d3f9e..68271bb0abd4b81f6a3f5b5711861aa3db23b07c 100644
--- a/tests/class/oracle/array_object_bts1739.res.oracle
+++ b/tests/class/oracle/array_object_bts1739.res.oracle
@@ -33,6 +33,8 @@ void vector::Ctor(struct vector const *this,
 
 void vector::Ctor(struct vector const *this, struct vector *__frama_c_arg_0);
 
+void vector::Dtor(struct vector const *this);
+
 struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
@@ -62,6 +64,12 @@ void vector::Ctor(struct vector const *this, struct vector *__frama_c_arg_0)
   return;
 }
 
+/*@ requires \valid_read(this); */
+void vector::Dtor(struct vector const *this)
+{
+  return;
+}
+
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "vector",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
diff --git a/tests/ppwp/oracle/expand.res.oracle b/tests/ppwp/oracle/expand.res.oracle
index 51e6b1b00aa4f235431a697e18b5956a7131af05..258b33c6b30c31890252e512ec8fb6d6704812c6 100644
--- a/tests/ppwp/oracle/expand.res.oracle
+++ b/tests/ppwp/oracle/expand.res.oracle
@@ -4,6 +4,7 @@ Now output intermediate result
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_Z1m_ensures : Valid
+[wp] [Cache] not used
 [wp] Proved goals:    1 / 1
   Qed:             1
 /* Generated by Frama-C */
diff --git a/tests/ppwp/oracle/expandf.res.oracle b/tests/ppwp/oracle/expandf.res.oracle
index b3239b7f2fa8b4d62398b67070ba5c85c08f1fba..69cf5301ef8f115b94f1e01fc10ce94a71130ef7 100644
--- a/tests/ppwp/oracle/expandf.res.oracle
+++ b/tests/ppwp/oracle/expandf.res.oracle
@@ -4,6 +4,7 @@ Now output intermediate result
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_Z1m_ensures : Valid
+[wp] [Cache] not used
 [wp] Proved goals:    1 / 1
   Qed:             1
 /* Generated by Frama-C */
diff --git a/tests/ppwp/oracle/simple.res.oracle b/tests/ppwp/oracle/simple.res.oracle
index 80373643d6d335127dec6d90bfba47ce147d4198..6812a5e83bc3307887c3923e97533b2992f8bdcb 100644
--- a/tests/ppwp/oracle/simple.res.oracle
+++ b/tests/ppwp/oracle/simple.res.oracle
@@ -4,6 +4,7 @@ Now output intermediate result
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_Z1m_ensures : Valid
+[wp] [Cache] not used
 [wp] Proved goals:    1 / 1
   Qed:             1
 /* Generated by Frama-C */
diff --git a/tests/ppwp/oracle/z.res.oracle b/tests/ppwp/oracle/z.res.oracle
index fbc8797c38e03de54890cabd9c7f985afe9c7af9..36b867051bc631f062ee3acabac8d98edc0d1e57 100644
--- a/tests/ppwp/oracle/z.res.oracle
+++ b/tests/ppwp/oracle/z.res.oracle
@@ -4,6 +4,7 @@ Now output intermediate result
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_Z1m_ensures : Valid
+[wp] [Cache] not used
 [wp] Proved goals:    1 / 1
   Qed:             1
 /* Generated by Frama-C */
diff --git a/tests/specs/oracle/wp_empty_struct.res.oracle b/tests/specs/oracle/wp_empty_struct.res.oracle
index 43a2493d9748c6e2f4cf3df84b6fcb8c981f7e08..1bb44f5331b1cf57217fc927509b0ae3a4255f93 100644
--- a/tests/specs/oracle/wp_empty_struct.res.oracle
+++ b/tests/specs/oracle/wp_empty_struct.res.oracle
@@ -5,5 +5,6 @@ Now output intermediate result
 [wp] 2 goals scheduled
 [wp] [Qed] Goal typed_ZN6Point2E3foo_ensures_2 : Valid
 [wp] [Qed] Goal typed_ZN6Point2E3foo_ensures : Valid
+[wp] [Cache] not used
 [wp] Proved goals:    2 / 2
   Qed:             2
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index 0cfb55d0fce4df625a67b9b2ac71574d66f670de..e58389aab7ece10dcc4c09b551401a652b27463b 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -840,6 +840,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(int *s) 
     reads *(s + (0 ..));
@@ -2681,8 +2698,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .number_of_base_classes = 0,
    .pvmt = (struct _frama_c_vmt *)0};
 /*@ requires \valid_read(pred); */
-struct unary_negate<bool*,<abst>> not1<bool*,<abst>>(_Bool (* const *pred)(
-                                                     int ))
+struct unary_negate<bool*,<abst>> not1<bool*,<abst>>(_Bool (* const *pred)
+                                                     (int ))
 {
   struct unary_negate<bool*,<abst>> __fc_tmp_2;
   unary_negate<bool*,<abst>>::Ctor(& __fc_tmp_2,pred);
@@ -2690,8 +2707,8 @@ struct unary_negate<bool*,<abst>> not1<bool*,<abst>>(_Bool (* const *pred)(
 }
 
 /*@ requires \valid_read(pred); */
-struct unary_negate<std::reference_wrapper<bool&,<abst>>> not1<std::reference_wrapper<bool&,<abst>>>(
-struct reference_wrapper<bool&,<abst>> const *pred)
+struct unary_negate<std::reference_wrapper<bool&,<abst>>> not1<std::reference_wrapper<bool&,<abst>>>
+(struct reference_wrapper<bool&,<abst>> const *pred)
 {
   struct unary_negate<std::reference_wrapper<bool&,<abst>>> __fc_tmp_3;
   unary_negate<std::reference_wrapper<bool&,<abst>>>::Ctor(& __fc_tmp_3,pred);
@@ -2946,8 +2963,8 @@ _Bool none_of<int*,bool*,<abst>>(int *first, int *last, _Bool (*pred)(int ))
   return tmp_0;
 }
 
-void (*for_each<int*,void*,<abst>>(int *first, int *last, void (*f)(int )))(
-int )
+void (*for_each<int*,void*,<abst>>(int *first, int *last, void (*f)(int )))
+(int )
 {
   void (*__retres)(int );
   type *tmp_0;
@@ -2997,9 +3014,9 @@ int *find_if<int*,bool&,<abst>>(int *first, int *last, _Bool (*pred)(int ))
   return_label: return __retres;
 }
 
-int *find_if<int*,std::unary_negate<std::reference_wrapper<bool&,<abst>>>>(
-int *first, int *last,
-struct unary_negate<std::reference_wrapper<bool&,<abst>>> pred)
+int *find_if<int*,std::unary_negate<std::reference_wrapper<bool&,<abst>>>>
+(int *first, int *last,
+ struct unary_negate<std::reference_wrapper<bool&,<abst>>> pred)
 {
   int *__retres;
   int **it = & first;
@@ -3324,11 +3341,11 @@ _Bool is_permutation<int*,int*>(int *first1, int *last1, int *first2)
   return_label: return __retres;
 }
 
-void UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE__cons(
-struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_ const *__fc_closure,
-_Bool (*__fc_func)(struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_ const *,
-                   value_type ),
-struct equal_to<int> pred, int *it1)
+void UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE__cons
+(struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_ const *__fc_closure,
+ _Bool (*__fc_func)(struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_ const *,
+                    value_type ),
+ struct equal_to<int> pred, int *it1)
 {
   __fc_closure->__fc_lambda_apply = __fc_func;
   equal_to<int>::Ctor(& __fc_closure->pred,
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index 8d2d725bdcb44674bda20ec401b0052e6ea8c9c5..b6003ee97c8797af15c78d4e060f2a18b1e803f7 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -569,6 +569,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(int *s) 
     reads *(s + (0 ..));
diff --git a/tests/stl/oracle/stl_iterator.res.oracle b/tests/stl/oracle/stl_iterator.res.oracle
index 386632085c977ed077a5874df39c3098cbcde4e9..71da5239e9d9f9d83d6f56639766282580e1f0a5 100644
--- a/tests/stl/oracle/stl_iterator.res.oracle
+++ b/tests/stl/oracle/stl_iterator.res.oracle
@@ -377,27 +377,27 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
    .number_of_base_classes = 0,
    .pvmt = (struct _frama_c_vmt *)0};
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0);
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0);
 
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0);
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0);
 
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this);
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this);
 
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0);
+struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0);
 
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0);
+struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0);
 
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this);
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this);
 
 struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
@@ -407,9 +407,9 @@ struct _frama_c_vmt_content _frama_c_vmt[1];
     requires \valid_read(this);
     requires \valid_read(__frama_c_arg_0);
  */
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0)
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0)
 {
   return;
 }
@@ -418,16 +418,16 @@ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__fram
     requires \valid_read(this);
     requires \valid(__frama_c_arg_0);
  */
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0)
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0)
 {
   return;
 }
 
 /*@ requires \valid_read(this); */
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
 {
   return;
 }
@@ -436,9 +436,9 @@ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
     requires \valid_read(__frama_c_arg_0);
     ensures \valid(\result);
  */
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0)
+struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0)
 {
   return this;
 }
@@ -447,16 +447,16 @@ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__fram
     requires \valid(__frama_c_arg_0);
     ensures \valid(\result);
  */
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0)
+struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0)
 {
   return this;
 }
 
 /*@ requires \valid_read(this); */
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
 {
   return;
 }
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index bc416e89bcff748f5cfbf9bb6a4b3801194f6b94..6b9236e1c1611a8bbb8e818e0076fdafd6d15f7d 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -341,8 +341,8 @@ void swap<std::default_delete<int>>(struct default_delete<int> *a,
 
 /*@ requires \valid(t);
     ensures \valid(\result); */
-struct unique_ptr<int[],std::default_delete<int[]>> *forward<std::unique_ptr<int[],std::default_delete<int[]>>>(
-type *t);
+struct unique_ptr<int[],std::default_delete<int[]>> *forward<std::unique_ptr<int[],std::default_delete<int[]>>>
+(type *t);
 
 /*@ requires \valid(t);
     ensures \valid(\result); */
@@ -572,6 +572,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(int *s) 
     reads *(s + (0 ..));
@@ -2468,8 +2485,8 @@ void swap(struct unique_ptr<int[],std::default_delete<int[]>> *this,
 
 /*@ requires \valid(t);
     ensures \valid(\result); */
-struct unique_ptr<int[],std::default_delete<int[]>> *forward<std::unique_ptr<int[],std::default_delete<int[]>>>(
-type *t)
+struct unique_ptr<int[],std::default_delete<int[]>> *forward<std::unique_ptr<int[],std::default_delete<int[]>>>
+(type *t)
 {
   return t;
 }
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index db40de8ce325d02c81ab392233997194076be210..6c28ec2940a3d7d75ac17729daa080b73734705a 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -522,6 +522,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(int *s) 
     reads *(s + (0 ..));
@@ -3287,10 +3304,6 @@ void *calloc(size_t nmemb, size_t size);
  */
 void *realloc(void *ptr, size_t size);
 
-/*@ ensures never_terminates: \false;
-    assigns \nothing; */
-void abort(void);
-
 /*@ assigns \result;
     assigns \result \from \nothing; */
 int atexit(void (*func)(void));
@@ -3299,10 +3312,6 @@ int atexit(void (*func)(void));
     assigns \result \from \nothing; */
 int at_quick_exit(void (*func)(void));
 
-/*@ ensures never_terminates: \false;
-    assigns \nothing; */
-void exit(int status);
-
 /*@ ensures never_terminates: \false;
     assigns \nothing; */
 void _Exit(int status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index f0e6d9a167281622921d84052f05e3ac711cdbb8..1c2574f4743b589c03d858bdaa70302345d37561 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -503,6 +503,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(int *s) 
     reads *(s + (0 ..));
@@ -3040,10 +3057,6 @@ void *calloc(size_t nmemb, size_t size);
  */
 void *realloc(void *ptr, size_t size);
 
-/*@ ensures never_terminates: \false;
-    assigns \nothing; */
-void abort(void);
-
 /*@ assigns \result;
     assigns \result \from \nothing; */
 int atexit(void (*func)(void));
@@ -3052,10 +3065,6 @@ int atexit(void (*func)(void));
     assigns \result \from \nothing; */
 int at_quick_exit(void (*func)(void));
 
-/*@ ensures never_terminates: \false;
-    assigns \nothing; */
-void exit(int status);
-
 /*@ ensures never_terminates: \false;
     assigns \nothing; */
 void _Exit(int status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 1c13d168dd5c190f446d50e5f33c76e6451031a3..4fda65f9c232d75e7daa429a8f6a6534559a96df 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -504,6 +504,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(int *s) 
     reads *(s + (0 ..));
@@ -3046,10 +3063,6 @@ void *calloc(size_t nmemb, size_t size);
  */
 void *realloc(void *ptr, size_t size);
 
-/*@ ensures never_terminates: \false;
-    assigns \nothing; */
-void abort(void);
-
 /*@ assigns \result;
     assigns \result \from \nothing; */
 int atexit(void (*func)(void));
@@ -3058,10 +3071,6 @@ int atexit(void (*func)(void));
     assigns \result \from \nothing; */
 int at_quick_exit(void (*func)(void));
 
-/*@ ensures never_terminates: \false;
-    assigns \nothing; */
-void exit(int status);
-
 /*@ ensures never_terminates: \false;
     assigns \nothing; */
 void _Exit(int status);
diff --git a/tests/stl/oracle/stl_system_error.err.oracle b/tests/stl/oracle/stl_system_error.err.oracle
index cf4d03f07070fc35f70272227415c9d6abc2f6d1..9712de6c53dd066847788a0481c40a1c6e9681f1 100644
--- a/tests/stl/oracle/stl_system_error.err.oracle
+++ b/tests/stl/oracle/stl_system_error.err.oracle
@@ -1,4 +1,4 @@
-FRAMAC_SHARE/libc/signal.h:208:47: types are not convertible
 FRAMAC_SHARE/libc/signal.h:223:28: Expecting ';' after requires clause
-FRAMAC_SHARE/libc/time.h:219:45: types are not convertible
-FRAMAC_SHARE/libc/time.h:266:43: types are not convertible
+FRAMAC_SHARE/libc/wchar.h:55:5: No suitable candidate found for function valid_read_or_empty.
+FRAMAC_SHARE/libc/wchar.h:69:74: No suitable candidate found for function valid_read_or_empty.
+FRAMAC_SHARE/libc/wchar.h:80:73: No suitable candidate found for function valid_or_empty.
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index ec1639e83fddd834f5e39efda63c0c73cb8b8cfa..1755439f0fafe1291823fc02855e9c5c9e5457e7 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -426,6 +426,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(int *s) 
     reads *(s + (0 ..));
@@ -1630,6 +1647,21 @@ struct sigaction *__fc_p_sigaction = __fc_sigaction;
     requires valid_oldact_or_null: oldact ≡ \null ∨ \valid(oldact);
     requires valid_read_act_or_null: act ≡ \null ∨ \valid_read(act);
     requires separated_acts: separation: \separated(act, oldact);
+    ensures
+      act_changed:
+        \old(act) ≡ \null ∨
+        \subset(*(__fc_p_sigaction + \old(signum)), *\old(act));
+    ensures
+      oldact_assigned:
+        \old(oldact) ≡ \null ∨
+        *\old(oldact) ∈ *(__fc_p_sigaction + \old(signum));
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns *oldact, *(__fc_p_sigaction + signum), \result;
+    assigns *oldact \from __fc_p_sigaction;
+    assigns *(__fc_p_sigaction + signum) \from *act;
+    assigns \result
+      \from (indirect: signum), (indirect: act), (indirect: *act),
+            (indirect: oldact), (indirect: *oldact);
  */
 int sigaction(int signum, struct sigaction const * __restrict act,
               struct sigaction * __restrict oldact);
@@ -1661,9 +1693,10 @@ clock_t clock(void);
     assigns \result \from time1, time0; */
 double difftime(time_t time1, time_t time0);
 
-/*@ assigns *timeptr, \result;
+/*@ requires valid_timeptr: \valid(timeptr);
+    assigns *timeptr, \result;
     assigns *timeptr \from *timeptr;
-    assigns \result \from *timeptr;
+    assigns \result \from (indirect: *timeptr);
  */
 time_t mktime(struct tm *timeptr);
 
@@ -1712,7 +1745,8 @@ void __fc_init__fc_time_tm(void)
 }
 
 struct tm * const __fc_p_time_tm = & __fc_time_tm;
-/*@ ensures
+/*@ requires valid_timer: \valid_read(timer);
+    ensures
       result_null_or_internal_tm:
         \result ≡ &__fc_time_tm ∨ \result ≡ \null;
     assigns \result, __fc_time_tm;
@@ -1721,7 +1755,8 @@ struct tm * const __fc_p_time_tm = & __fc_time_tm;
  */
 struct tm *gmtime(time_t const *timer);
 
-/*@ ensures
+/*@ requires valid_timer: \valid_read(timer);
+    ensures
       result_null_or_internal_tm:
         \result ≡ &__fc_time_tm ∨ \result ≡ \null;
     assigns \result, __fc_time_tm;
@@ -1813,10 +1848,56 @@ axiomatic nanosleep_predicates {
       assumes relative_time: (flags & 1) ≡ 0;
       assumes interrupted: __fc_interrupted ≢ 0;
       assumes no_einval: valid_clock_id(clock_id);
+      ensures result_interrupted: \result ≡ 4;
+      ensures
+        interrupted_remaining: initialization:
+          \old(rmtp) ≢ \null ⇒
+          \initialized(&\old(rmtp)->tv_sec) ∧
+          \initialized(&\old(rmtp)->tv_nsec);
+      ensures
+        interrupted_remaining_decreases:
+          \old(rmtp) ≢ \null ⇒
+          \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
+          \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
+      ensures
+        remaining_valid:
+          \old(rmtp) ≢ \null ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
+      assigns \result, *rmtp;
+      assigns \result
+        \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
+              (indirect: *rqtp);
+      assigns *rmtp
+        \from __fc_time, (indirect: clock_id), (indirect: rqtp),
+              (indirect: *rqtp), (indirect: rmtp);
+    
+    behavior relative_no_error:
+      assumes relative_time: (flags & 1) ≡ 0;
+      assumes not_interrupted: __fc_interrupted ≡ 0;
+      assumes no_einval: valid_clock_id(clock_id);
+      ensures result_ok: \result ≡ 0;
       assigns \result;
       assigns \result
         \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
               (indirect: *rqtp);
+    
+    behavior relative_invalid_clock_id:
+      assumes relative_time: (flags & 1) ≡ 0;
+      assumes not_interrupted: __fc_interrupted ≡ 0;
+      assumes einval: ¬valid_clock_id(clock_id);
+      ensures result_einval: \result ≡ 22;
+      assigns \result;
+      assigns \result
+        \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
+              (indirect: *rqtp);
+    
+    complete behaviors relative_invalid_clock_id,
+                       relative_no_error,
+                       relative_interrupted,
+                       absolute;
+    disjoint behaviors relative_invalid_clock_id,
+                       relative_no_error,
+                       relative_interrupted,
+                       absolute;
  */
 int clock_nanosleep(clockid_t clock_id, int flags,
                     struct timespec const *rqtp, struct timespec *rmtp);
@@ -1827,14 +1908,30 @@ int clock_nanosleep(clockid_t clock_id, int flags,
         \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
     requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
     requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
-    assigns \result;
+    ensures result_elapsed_or_interrupted: \result ≡ 0 ∨ \result ≡ -1;
+    ensures
+      interrupted_remaining: initialization:
+        \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
+        \initialized(&\old(rmtp)->tv_sec) ∧
+        \initialized(&\old(rmtp)->tv_nsec);
+    ensures
+      interrupted_remaining_decreases:
+        \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
+        \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
+        \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
+    ensures
+      interrupted_remaining_valid:
+        \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
+        0 ≤ \old(rmtp)->tv_nsec < 1000000000;
+    assigns \result, *rmtp;
     assigns \result
       \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp);
+    assigns *rmtp
+      \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp),
+            (indirect: rmtp);
  */
 int nanosleep(struct timespec const *rqtp, struct timespec *rmtp);
 
-void tzset(void);
-
 int daylight;
 long timezone;
 char *tzname[2];
@@ -1843,42 +1940,18 @@ char *tzname[2];
  */
 void tzset(void);
 
-/*@ ensures
-      result_null_or_inside_s:
-        \result ≡ \null ∨ \subset(\result, \old(s) + (0 .. \old(n) - 1));
-    assigns \result;
-    assigns \result
-      \from s, (indirect: *(s + (0 .. n - 1))), (indirect: c), (indirect: n);
- */
-int *wmemchr(int const *s, int c, size_t n);
-
-/*@ assigns \result;
-    assigns \result
-      \from (indirect: *(s1 + (0 .. n - 1))),
-            (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
- */
-int wmemcmp(int const *s1, int const *s2, size_t n);
-
-/*@ requires
-      src: dest: separation:
-        \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
+/*@ 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);
     assigns \result \from dest;
  */
-int *wmemcpy(int * __restrict dest, int const * __restrict src, size_t n);
-
-/*@ 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);
-    assigns \result \from dest;
- */
 int *wmemmove(int *dest, int const *src, size_t n);
 
-/*@ ensures result_ptr: \result ≡ \old(wcs);
+/*@ requires valid_wcs: \valid(wcs + (0 .. n - 1));
+    ensures result_ptr: \result ≡ \old(wcs);
     ensures
       wcs: initialization: \initialized(\old(wcs) + (0 .. \old(n) - 1));
     ensures
@@ -1889,7 +1962,17 @@ int *wmemmove(int *dest, int const *src, size_t n);
  */
 int *wmemset(int *wcs, int wc, size_t n);
 
-/*@ 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 ..)),
@@ -1907,28 +1990,46 @@ int *wcscat(int * __restrict dest, int const * __restrict src);
  */
 int *wcschr(int const *wcs, int 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 ..)));
  */
 int wcscmp(int const *s1, int const *s2);
 
-/*@ 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;
  */
 int *wcscpy(int * __restrict dest, int const * __restrict 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 ..)));
  */
 size_t wcscspn(int const *wcs, int 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);
@@ -1938,7 +2039,9 @@ size_t wcscspn(int const *wcs, int const *accept);
  */
 size_t wcslcat(int * __restrict dest, int const * __restrict src, size_t n);
 
-/*@ requires
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+    requires room_nwstring: \valid(dest + (0 .. n));
+    requires
       src: dest: separation:
         \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     assigns *(dest + (0 .. n - 1)), \result;
@@ -1951,12 +2054,23 @@ size_t wcslcat(int * __restrict dest, int const * __restrict src, size_t n);
 size_t wcslcpy(int *dest, int const *src, size_t n);
 
 /*@ requires valid_string_s: valid_read_wstring(s);
+    ensures result_is_length: \result ≡ wcslen(\old(s));
     assigns \result;
-    assigns \result \from (indirect: *(s + (0 ..)));
+    assigns \result \from (indirect: *(s + (0 .. wcslen{Old}(s))));
  */
 size_t wcslen(int const *s);
 
-/*@ 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)),
@@ -1965,17 +2079,22 @@ size_t wcslen(int const *s);
  */
 int *wcsncat(int * __restrict dest, int const * __restrict 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);
  */
 int wcsncmp(int const *s1, int const *s2, size_t n);
 
-/*@ requires
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+    requires room_nwstring: \valid(dest + (0 .. n - 1));
+    requires
       src: dest: separation:
         \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);
@@ -1983,7 +2102,9 @@ int wcsncmp(int const *s1, int const *s2, size_t n);
  */
 int *wcsncpy(int * __restrict dest, int const * __restrict 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;
@@ -1992,21 +2113,28 @@ int *wcsncpy(int * __restrict dest, int const * __restrict src, size_t n);
  */
 int *wcspbrk(int const *wcs, int 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);
  */
 int *wcsrchr(int const *wcs, int 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))));
  */
 size_t wcsspn(int const *wcs, int 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;
@@ -2016,13 +2144,14 @@ size_t wcsspn(int const *wcs, int const *accept);
  */
 int *wcsstr(int const *haystack, int 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);
  */
 int *fgetws(int * __restrict ws, int n, FILE * __restrict stream);
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index 9c149b3e9cb9c5add1931fdb5db0a6f32e562492..f0fc168c9c4e2a027a3847e92ae596b427ca8882 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -261,6 +261,23 @@ axiomatic StrChr {
   }
  */
 /*@
+axiomatic WMemChr {
+  logic 𝔹 wmemchr{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  logic ℤ wmemchr_off{L}(int *s, int c, ℤ n) 
+    reads *(s + (0 .. n - 1));
+  
+  axiom wmemchr_def{L}:
+    ∀ int *s;
+    ∀ int c;
+    ∀ ℤ n;
+      wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+  
+  }
+ */
+/*@
 axiomatic WcsLen {
   logic ℤ wcslen{L}(int *s) 
     reads *(s + (0 ..));
diff --git a/tests/stl/oracle/stl_utility.err.oracle b/tests/stl/oracle/stl_utility.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/template/oracle/template_variadic.res.oracle b/tests/template/oracle/template_variadic.res.oracle
index 584f3fe58fce9082dd60fb997feb79ed90a6f5ab..344ad1122b0fe31f93d59e13d166484206b8fbe5 100644
--- a/tests/template/oracle/template_variadic.res.oracle
+++ b/tests/template/oracle/template_variadic.res.oracle
@@ -26,24 +26,24 @@ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> {
    
 };
 typedef struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> type;
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this);
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this);
 
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *__frama_c_arg_0);
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
+ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *__frama_c_arg_0);
 
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> *__frama_c_arg_0);
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
+ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> *__frama_c_arg_0);
 
 struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
 struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this)
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this)
 {
   return;
 }
@@ -52,9 +52,9 @@ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this
     requires \valid_read(this);
     requires \valid_read(__frama_c_arg_0);
  */
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *__frama_c_arg_0)
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
+ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *__frama_c_arg_0)
 {
   return;
 }
@@ -63,9 +63,9 @@ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *__fr
     requires \valid_read(this);
     requires \valid(__frama_c_arg_0);
  */
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> *__frama_c_arg_0)
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
+ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> *__frama_c_arg_0)
 {
   return;
 }