From 742450a6cb00098e32503d90f79c9144e1762686 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 18 Jun 2020 16:53:17 +0200
Subject: [PATCH] [tests] update oracles
---
tests/stl/oracle/stl_algorithm.res.oracle | 12 +++++++++++-
tests/stl/oracle/stl_functional.res.oracle | 12 +++++++++++-
tests/stl/oracle/stl_memory.res.oracle | 12 +++++++++++-
tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle | 12 +++++++++++-
tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle | 12 +++++++++++-
tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle | 12 +++++++++++-
tests/stl/oracle/stl_system_error.err.oracle | 2 +-
tests/stl/oracle/stl_system_error.res.oracle | 12 +++++++++++-
tests/stl/oracle/stl_typeinfo.res.oracle | 12 +++++++++++-
9 files changed, 89 insertions(+), 9 deletions(-)
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index e9f59a74..22f01d33 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -1149,7 +1149,8 @@ int strcoll(char const *s1, char const *s2);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
- assigns \result \from s, *(s + (0 ..)), c;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
@@ -1173,6 +1174,15 @@ int strcoll(char const *s1, char const *s2);
*/
char *strchr(char const *s, int c);
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures
+ result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+ */
+char *strchrnul(char const *s, int c);
+
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index 834f4bcf..8abe1c09 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -878,7 +878,8 @@ int strcoll(char const *s1, char const *s2);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
- assigns \result \from s, *(s + (0 ..)), c;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
@@ -902,6 +903,15 @@ int strcoll(char const *s1, char const *s2);
*/
char *strchr(char const *s, int c);
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures
+ result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+ */
+char *strchrnul(char const *s, int c);
+
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index a28010d7..8b5a0ab0 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -881,7 +881,8 @@ int strcoll(char const *s1, char const *s2);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
- assigns \result \from s, *(s + (0 ..)), c;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
@@ -905,6 +906,15 @@ int strcoll(char const *s1, char const *s2);
*/
char *strchr(char const *s, int c);
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures
+ result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+ */
+char *strchrnul(char const *s, int c);
+
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index d44adcde..f02c0bd0 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -878,7 +878,8 @@ int strcoll(char const *s1, char const *s2);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
- assigns \result \from s, *(s + (0 ..)), c;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
@@ -902,6 +903,15 @@ int strcoll(char const *s1, char const *s2);
*/
char *strchr(char const *s, int c);
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures
+ result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+ */
+char *strchrnul(char const *s, int c);
+
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index e979a9ec..f1e95a07 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -859,7 +859,8 @@ int strcoll(char const *s1, char const *s2);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
- assigns \result \from s, *(s + (0 ..)), c;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
@@ -883,6 +884,15 @@ int strcoll(char const *s1, char const *s2);
*/
char *strchr(char const *s, int c);
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures
+ result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+ */
+char *strchrnul(char const *s, int c);
+
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index b3e59ee2..0e7e54f8 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -860,7 +860,8 @@ int strcoll(char const *s1, char const *s2);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
- assigns \result \from s, *(s + (0 ..)), c;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
@@ -884,6 +885,15 @@ int strcoll(char const *s1, char const *s2);
*/
char *strchr(char const *s, int c);
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures
+ result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+ */
+char *strchrnul(char const *s, int c);
+
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_system_error.err.oracle b/tests/stl/oracle/stl_system_error.err.oracle
index 9712de6c..d8af1fa6 100644
--- a/tests/stl/oracle/stl_system_error.err.oracle
+++ b/tests/stl/oracle/stl_system_error.err.oracle
@@ -1,4 +1,4 @@
-FRAMAC_SHARE/libc/signal.h:223:28: Expecting ';' after requires clause
+FRAMAC_SHARE/libc/signal.h:227:28: Expecting ';' after requires clause
FRAMAC_SHARE/libc/wchar.h:55:5: No suitable candidate found for function valid_read_or_empty.
FRAMAC_SHARE/libc/wchar.h:69:74: No suitable candidate found for function valid_read_or_empty.
FRAMAC_SHARE/libc/wchar.h:80:73: No suitable candidate found for function valid_or_empty.
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index b2169e75..94668511 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -734,7 +734,8 @@ int strcoll(char const *s1, char const *s2);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
- assigns \result \from s, *(s + (0 ..)), c;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
@@ -758,6 +759,15 @@ int strcoll(char const *s1, char const *s2);
*/
char *strchr(char const *s, int c);
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures
+ result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+ */
+char *strchrnul(char const *s, int c);
+
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result \from s, *(s + (0 ..)), c;
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index a5b1a5d1..1b39f2c2 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -569,7 +569,8 @@ int strcoll(char const *s1, char const *s2);
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
- assigns \result \from s, *(s + (0 ..)), c;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
@@ -593,6 +594,15 @@ int strcoll(char const *s1, char const *s2);
*/
char *strchr(char const *s, int c);
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures
+ result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+ */
+char *strchrnul(char const *s, int c);
+
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result \from s, *(s + (0 ..)), c;
--
GitLab