From 1285fbdf90c585b5e78c1cf599252ec5710c1ae6 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 11 Mar 2020 19:27:49 +0100
Subject: [PATCH] [tests] update oracles wrt kernel changes
---
tests/stl/oracle/stl_algorithm.res.oracle | 11 ++++++-----
tests/stl/oracle/stl_functional.res.oracle | 11 ++++++-----
tests/stl/oracle/stl_memory.res.oracle | 11 ++++++-----
tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle | 11 ++++++-----
tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle | 11 ++++++-----
tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle | 11 ++++++-----
tests/stl/oracle/stl_system_error.res.oracle | 11 ++++++-----
tests/stl/oracle/stl_typeinfo.res.oracle | 11 ++++++-----
8 files changed, 48 insertions(+), 40 deletions(-)
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index e58389aa..e9f59a74 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -997,8 +997,8 @@ axiomatic dynamic_allocation {
}
*/
/*@
-predicate non_escaping{L}(void *s, size_t n) =
- ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+ ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
*/
/*@
predicate empty_block{L}(void *s) =
@@ -1056,7 +1056,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
∀ ℤ i;
(0 ≤ i < \old(n) ⇒
*((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
- \result ≤ \old(s) + i;
+ (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1413,7 +1413,7 @@ char *strerror(int errnum);
*/
char *strcpy(char * __restrict dest, char const * __restrict src);
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires room_nstring: \valid(dest + (0 .. n - 1));
requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
@@ -1578,7 +1578,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
*/
char *strdup(char const *s);
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index b6003ee9..834f4bcf 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -726,8 +726,8 @@ axiomatic dynamic_allocation {
}
*/
/*@
-predicate non_escaping{L}(void *s, size_t n) =
- ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+ ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
*/
/*@
predicate empty_block{L}(void *s) =
@@ -785,7 +785,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
∀ ℤ i;
(0 ≤ i < \old(n) ⇒
*((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
- \result ≤ \old(s) + i;
+ (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1142,7 +1142,7 @@ char *strerror(int errnum);
*/
char *strcpy(char * __restrict dest, char const * __restrict src);
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires room_nstring: \valid(dest + (0 .. n - 1));
requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
@@ -1307,7 +1307,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
*/
char *strdup(char const *s);
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index 6b9236e1..a28010d7 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -729,8 +729,8 @@ axiomatic dynamic_allocation {
}
*/
/*@
-predicate non_escaping{L}(void *s, size_t n) =
- ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+ ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
*/
/*@
predicate empty_block{L}(void *s) =
@@ -788,7 +788,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
∀ ℤ i;
(0 ≤ i < \old(n) ⇒
*((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
- \result ≤ \old(s) + i;
+ (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1145,7 +1145,7 @@ char *strerror(int errnum);
*/
char *strcpy(char * __restrict dest, char const * __restrict src);
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires room_nstring: \valid(dest + (0 .. n - 1));
requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
@@ -1310,7 +1310,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
*/
char *strdup(char const *s);
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index 4c001446..d44adcde 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -726,8 +726,8 @@ axiomatic dynamic_allocation {
void *malloc(size_t size);
/*@
-predicate non_escaping{L}(void *s, size_t n) =
- ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+ ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
*/
/*@
predicate empty_block{L}(void *s) =
@@ -785,7 +785,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
∀ ℤ i;
(0 ≤ i < \old(n) ⇒
*((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
- \result ≤ \old(s) + i;
+ (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1142,7 +1142,7 @@ char *strerror(int errnum);
*/
char *strcpy(char * __restrict dest, char const * __restrict src);
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires room_nstring: \valid(dest + (0 .. n - 1));
requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
@@ -1307,7 +1307,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
*/
char *strdup(char const *s);
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 7fd8b8b8..e979a9ec 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -707,8 +707,8 @@ axiomatic dynamic_allocation {
void *malloc(size_t size);
/*@
-predicate non_escaping{L}(void *s, size_t n) =
- ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+ ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
*/
/*@
predicate empty_block{L}(void *s) =
@@ -766,7 +766,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
∀ ℤ i;
(0 ≤ i < \old(n) ⇒
*((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
- \result ≤ \old(s) + i;
+ (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1123,7 +1123,7 @@ char *strerror(int errnum);
*/
char *strcpy(char * __restrict dest, char const * __restrict src);
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires room_nstring: \valid(dest + (0 .. n - 1));
requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
@@ -1288,7 +1288,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
*/
char *strdup(char const *s);
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index b078461f..b3e59ee2 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -708,8 +708,8 @@ axiomatic dynamic_allocation {
void *malloc(size_t size);
/*@
-predicate non_escaping{L}(void *s, size_t n) =
- ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+ ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
*/
/*@
predicate empty_block{L}(void *s) =
@@ -767,7 +767,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
∀ ℤ i;
(0 ≤ i < \old(n) ⇒
*((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
- \result ≤ \old(s) + i;
+ (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1124,7 +1124,7 @@ char *strerror(int errnum);
*/
char *strcpy(char * __restrict dest, char const * __restrict src);
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires room_nstring: \valid(dest + (0 .. n - 1));
requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
@@ -1289,7 +1289,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
*/
char *strdup(char const *s);
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index 1755439f..b2169e75 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -583,8 +583,8 @@ axiomatic dynamic_allocation {
}
*/
/*@
-predicate non_escaping{L}(void *s, size_t n) =
- ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+ ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
*/
/*@
predicate empty_block{L}(void *s) =
@@ -641,7 +641,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
∀ ℤ i;
(0 ≤ i < \old(n) ⇒
*((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
- \result ≤ \old(s) + i;
+ (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -998,7 +998,7 @@ char *strerror(int errnum);
*/
char *strcpy(char * __restrict dest, char const * __restrict src);
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires room_nstring: \valid(dest + (0 .. n - 1));
requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
@@ -1163,7 +1163,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
*/
char *strdup(char const *s);
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index f0fc168c..a5b1a5d1 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -418,8 +418,8 @@ axiomatic dynamic_allocation {
}
*/
/*@
-predicate non_escaping{L}(void *s, size_t n) =
- ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+ ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
*/
/*@
predicate empty_block{L}(void *s) =
@@ -476,7 +476,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
∀ ℤ i;
(0 ≤ i < \old(n) ⇒
*((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
- \result ≤ \old(s) + i;
+ (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -833,7 +833,7 @@ char *strerror(int errnum);
*/
char *strcpy(char * __restrict dest, char const * __restrict src);
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
requires room_nstring: \valid(dest + (0 .. n - 1));
requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
@@ -998,7 +998,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
*/
char *strdup(char const *s);
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
(indirect: __fc_heap_status);
--
GitLab