diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index 65d1f22f8ad121593f5c671f9bcf1867b31ef9e7..b263a58338e9bb57547a2630879347e9ea04e8d1 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -914,6 +914,23 @@ void *memchr(void const *s, int c, size_t n);
  */
 void *memcpy(void * restrict dest, void const * restrict src, size_t n);
 
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_next_byte: \result ≡ \old(dest) + \old(n);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest, n;
+ */
+void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
+
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
     ensures
diff --git a/tests/stl/oracle/stl_bool.res.oracle b/tests/stl/oracle/stl_bool.res.oracle
index e1745080bc1154053906d610f9d6a7a35f8a61e8..352d0113dcbd7a53595267285733e2374b4fccb7 100644
--- a/tests/stl/oracle/stl_bool.res.oracle
+++ b/tests/stl/oracle/stl_bool.res.oracle
@@ -564,6 +564,23 @@ void *memchr(void const *s, int c, size_t n);
  */
 void *memcpy(void * restrict dest, void const * restrict src, size_t n);
 
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_next_byte: \result ≡ \old(dest) + \old(n);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest, n;
+ */
+void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
+
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
     ensures
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index 49404941377b8d9d9d3546371c07d8d9b399bc92..5fd49181f49089c9d460dd5ef502b9f144a6eca1 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -730,6 +730,23 @@ void *memchr(void const *s, int c, size_t n);
  */
 void *memcpy(void * restrict dest, void const * restrict src, size_t n);
 
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_next_byte: \result ≡ \old(dest) + \old(n);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest, n;
+ */
+void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
+
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
     ensures
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index e6798f27237e423a4b7a5659b0e61e8fa5364e35..27898b6f81bb286cb274d6569ca7050512de3061 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -741,6 +741,23 @@ void *memchr(void const *s, int c, size_t n);
  */
 void *memcpy(void * restrict dest, void const * restrict src, size_t n);
 
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_next_byte: \result ≡ \old(dest) + \old(n);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest, n;
+ */
+void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
+
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
     ensures
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index 89440d26f372d869076444cf2e66316b12311b6f..4ac0ce1844c978728332c6a11810b76c98368e43 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -745,6 +745,23 @@ void *memchr(void const *s, int c, size_t n);
  */
 void *memcpy(void * restrict dest, void const * restrict src, size_t n);
 
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_next_byte: \result ≡ \old(dest) + \old(n);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest, n;
+ */
+void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
+
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
     ensures
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 287273ccad155ad909df7c314571062232aa0dab..b1ec9d37f81ad621fe7f1b8b57b49d4a40eca2e9 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -726,6 +726,23 @@ void *memchr(void const *s, int c, size_t n);
  */
 void *memcpy(void * restrict dest, void const * restrict src, size_t n);
 
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_next_byte: \result ≡ \old(dest) + \old(n);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest, n;
+ */
+void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
+
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
     ensures
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 4a6edf4c1b97b1ad1e009836bde3edeb5f6ca4f2..483c14a02f40c93e376d8cc6efdd571d945a8749 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -727,6 +727,23 @@ void *memchr(void const *s, int c, size_t n);
  */
 void *memcpy(void * restrict dest, void const * restrict src, size_t n);
 
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_next_byte: \result ≡ \old(dest) + \old(n);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest, n;
+ */
+void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
+
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
     ensures
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index 7f8d545dc270c4e7a275e2b798498695aa8c7040..04d8410ed46f178dac7e12860ee5ecc948054cc4 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -641,6 +641,23 @@ void *memchr(void const *s, int c, size_t n);
  */
 void *memcpy(void * restrict dest, void const * restrict src, size_t n);
 
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_next_byte: \result ≡ \old(dest) + \old(n);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest, n;
+ */
+void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
+
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
     ensures
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index 38b9851932e52deeb23dbd5886a2cae278db856d..aff148bb0dfa62aef219ec170d1586e46bfa2ed7 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -501,6 +501,23 @@ void *memchr(void const *s, int c, size_t n);
  */
 void *memcpy(void * restrict dest, void const * restrict src, size_t n);
 
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_next_byte: \result ≡ \old(dest) + \old(n);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest, n;
+ */
+void *mempcpy(void * restrict dest, void const * restrict src, size_t n);
+
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
     ensures