diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index 5b5391f926d2ac3ccdda976609d83e09d86f5956..7404de4d8ea2e13942a395ef7afe0e23289f221b 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -440,7 +440,7 @@ long atol(char const *nptr);
  */
 long long atoll(char const *nptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -456,7 +456,7 @@ long long atoll(char const *nptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -468,7 +468,7 @@ long long atoll(char const *nptr);
  */
 double strtod(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -484,7 +484,7 @@ double strtod(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -496,7 +496,7 @@ double strtod(char const * restrict nptr, char ** restrict endptr);
  */
 float strtof(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -512,7 +512,7 @@ float strtof(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -524,7 +524,7 @@ float strtof(char const * restrict nptr, char ** restrict endptr);
  */
 long double strtold(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -545,7 +545,7 @@ long double strtold(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -560,7 +560,7 @@ long double strtold(char const * restrict nptr, char ** restrict endptr);
  */
 long strtol(char const * restrict nptr, char ** restrict endptr, int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -581,7 +581,7 @@ long strtol(char const * restrict nptr, char ** restrict endptr, int base);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -597,7 +597,7 @@ long strtol(char const * restrict nptr, char ** restrict endptr, int base);
 long long strtoll(char const * restrict nptr, char ** restrict endptr,
                   int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -618,7 +618,7 @@ long long strtoll(char const * restrict nptr, char ** restrict endptr,
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -634,7 +634,7 @@ long long strtoll(char const * restrict nptr, char ** restrict endptr,
 unsigned long strtoul(char const * restrict nptr, char ** restrict endptr,
                       int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -655,7 +655,7 @@ unsigned long strtoul(char const * restrict nptr, char ** restrict endptr,
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index b37143d6da28997f54420bc4f7652beac23bbdba..a12fa44c50c296a6e43f0884f0f45048e14df710 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -409,7 +409,7 @@ long atol(char const *nptr);
  */
 long long atoll(char const *nptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -425,7 +425,7 @@ long long atoll(char const *nptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -437,7 +437,7 @@ long long atoll(char const *nptr);
  */
 double strtod(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -453,7 +453,7 @@ double strtod(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -465,7 +465,7 @@ double strtod(char const * restrict nptr, char ** restrict endptr);
  */
 float strtof(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -481,7 +481,7 @@ float strtof(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -493,7 +493,7 @@ float strtof(char const * restrict nptr, char ** restrict endptr);
  */
 long double strtold(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -514,7 +514,7 @@ long double strtold(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -529,7 +529,7 @@ long double strtold(char const * restrict nptr, char ** restrict endptr);
  */
 long strtol(char const * restrict nptr, char ** restrict endptr, int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -550,7 +550,7 @@ long strtol(char const * restrict nptr, char ** restrict endptr, int base);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -566,7 +566,7 @@ long strtol(char const * restrict nptr, char ** restrict endptr, int base);
 long long strtoll(char const * restrict nptr, char ** restrict endptr,
                   int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -587,7 +587,7 @@ long long strtoll(char const * restrict nptr, char ** restrict endptr,
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -603,7 +603,7 @@ long long strtoll(char const * restrict nptr, char ** restrict endptr,
 unsigned long strtoul(char const * restrict nptr, char ** restrict endptr,
                       int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -624,7 +624,7 @@ unsigned long strtoul(char const * restrict nptr, char ** restrict endptr,
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index 549101c305029623478eadfd5dd5579084929e2f..3aed66ca369e67ddf9554386637eb9d445456280 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -2536,7 +2536,7 @@ long atol(char const *nptr);
  */
 long long atoll(char const *nptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2552,7 +2552,7 @@ long long atoll(char const *nptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2564,7 +2564,7 @@ long long atoll(char const *nptr);
  */
 double strtod(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2580,7 +2580,7 @@ double strtod(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2592,7 +2592,7 @@ double strtod(char const * restrict nptr, char ** restrict endptr);
  */
 float strtof(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2608,7 +2608,7 @@ float strtof(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2620,7 +2620,7 @@ float strtof(char const * restrict nptr, char ** restrict endptr);
  */
 long double strtold(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2641,7 +2641,7 @@ long double strtold(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -2656,7 +2656,7 @@ long double strtold(char const * restrict nptr, char ** restrict endptr);
  */
 long strtol(char const * restrict nptr, char ** restrict endptr, int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2677,7 +2677,7 @@ long strtol(char const * restrict nptr, char ** restrict endptr, int base);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -2693,7 +2693,7 @@ long strtol(char const * restrict nptr, char ** restrict endptr, int base);
 long long strtoll(char const * restrict nptr, char ** restrict endptr,
                   int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2714,7 +2714,7 @@ long long strtoll(char const * restrict nptr, char ** restrict endptr,
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -2730,7 +2730,7 @@ long long strtoll(char const * restrict nptr, char ** restrict endptr,
 unsigned long strtoul(char const * restrict nptr, char ** restrict endptr,
                       int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2751,7 +2751,7 @@ unsigned long strtoul(char const * restrict nptr, char ** restrict endptr,
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 44ad7e2421a5779e85ad859a249778954aca988a..93272875fe11dee726682a4633df56775edb13b3 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -2315,7 +2315,7 @@ long atol(char const *nptr);
  */
 long long atoll(char const *nptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2331,7 +2331,7 @@ long long atoll(char const *nptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2343,7 +2343,7 @@ long long atoll(char const *nptr);
  */
 double strtod(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2359,7 +2359,7 @@ double strtod(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2371,7 +2371,7 @@ double strtod(char const * restrict nptr, char ** restrict endptr);
  */
 float strtof(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2387,7 +2387,7 @@ float strtof(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2399,7 +2399,7 @@ float strtof(char const * restrict nptr, char ** restrict endptr);
  */
 long double strtold(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2420,7 +2420,7 @@ long double strtold(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -2435,7 +2435,7 @@ long double strtold(char const * restrict nptr, char ** restrict endptr);
  */
 long strtol(char const * restrict nptr, char ** restrict endptr, int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2456,7 +2456,7 @@ long strtol(char const * restrict nptr, char ** restrict endptr, int base);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -2472,7 +2472,7 @@ long strtol(char const * restrict nptr, char ** restrict endptr, int base);
 long long strtoll(char const * restrict nptr, char ** restrict endptr,
                   int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2493,7 +2493,7 @@ long long strtoll(char const * restrict nptr, char ** restrict endptr,
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -2509,7 +2509,7 @@ long long strtoll(char const * restrict nptr, char ** restrict endptr,
 unsigned long strtoul(char const * restrict nptr, char ** restrict endptr,
                       int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2530,7 +2530,7 @@ unsigned long strtoul(char const * restrict nptr, char ** restrict endptr,
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index ceaa7dba43c03ad5f1bb2765e1ebe5308ff76298..31e6f7e6cf06a2c6eda81e4715b264cadf34ece8 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -2321,7 +2321,7 @@ long atol(char const *nptr);
  */
 long long atoll(char const *nptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2337,7 +2337,7 @@ long long atoll(char const *nptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2349,7 +2349,7 @@ long long atoll(char const *nptr);
  */
 double strtod(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2365,7 +2365,7 @@ double strtod(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2377,7 +2377,7 @@ double strtod(char const * restrict nptr, char ** restrict endptr);
  */
 float strtof(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     assigns \result, *endptr;
     assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2393,7 +2393,7 @@ float strtof(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -2405,7 +2405,7 @@ float strtof(char const * restrict nptr, char ** restrict endptr);
  */
 long double strtold(char const * restrict nptr, char ** restrict endptr);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2426,7 +2426,7 @@ long double strtold(char const * restrict nptr, char ** restrict endptr);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -2441,7 +2441,7 @@ long double strtold(char const * restrict nptr, char ** restrict endptr);
  */
 long strtol(char const * restrict nptr, char ** restrict endptr, int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2462,7 +2462,7 @@ long strtol(char const * restrict nptr, char ** restrict endptr, int base);
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -2478,7 +2478,7 @@ long strtol(char const * restrict nptr, char ** restrict endptr, int base);
 long long strtoll(char const * restrict nptr, char ** restrict endptr,
                   int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2499,7 +2499,7 @@ long long strtoll(char const * restrict nptr, char ** restrict endptr,
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result
@@ -2515,7 +2515,7 @@ long long strtoll(char const * restrict nptr, char ** restrict endptr,
 unsigned long strtoul(char const * restrict nptr, char ** restrict endptr,
                       int base);
 
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
     requires separation: \separated(nptr, endptr);
     requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
     assigns \result, *endptr;
@@ -2536,7 +2536,7 @@ unsigned long strtoul(char const * restrict nptr, char ** restrict endptr,
       assumes nonnull_endptr: endptr ≢ \null;
       requires valid_endptr: \valid(endptr);
       ensures initialization: \initialized(\old(endptr));
-      ensures valid_endptr: \valid_read(\old(endptr));
+      ensures valid_endptr_content: \valid_read(*\old(endptr));
       ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
       assigns \result, *endptr;
       assigns \result