synchronize with frama-c/frama-c!3257

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

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

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

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

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

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

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

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

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