From 57b10a76de56ea17ab99181f90d4db034a21058d Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 25 Jun 2021 18:53:21 +0200
Subject: [PATCH] synchronize with frama-c/frama-c!3257

---
 tests/stl/oracle/stl_algorithm.res.oracle       | 17 +++++++++++++++++
 tests/stl/oracle/stl_bool.res.oracle            | 17 +++++++++++++++++
 tests/stl/oracle/stl_functional.res.oracle      | 17 +++++++++++++++++
 tests/stl/oracle/stl_memory.res.oracle          | 17 +++++++++++++++++
 .../oracle/stl_shared_ptr_mistake10.res.oracle  | 17 +++++++++++++++++
 .../oracle/stl_shared_ptr_mistake5.res.oracle   | 17 +++++++++++++++++
 .../oracle/stl_shared_ptr_mistake6.res.oracle   | 17 +++++++++++++++++
 tests/stl/oracle/stl_system_error.res.oracle    | 17 +++++++++++++++++
 tests/stl/oracle/stl_typeinfo.res.oracle        | 17 +++++++++++++++++
 9 files changed, 153 insertions(+)

diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index 65d1f22f..b263a583 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 e1745080..352d0113 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 49404941..5fd49181 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 e6798f27..27898b6f 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 89440d26..4ac0ce18 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 287273cc..b1ec9d37 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 4a6edf4c..483c14a0 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 7f8d545d..04d8410e 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 38b98519..aff148bb 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
-- 
GitLab