From a6fd927e3b9589617d6c6b0c34c39994e6da6b76 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 18 Sep 2024 19:32:03 +0200
Subject: [PATCH] [libc] Update tests oracles
---
tests/basic/oracle/placement_new.res.oracle | 33 +++++++++
tests/basic/oracle/placement_newb.res.oracle | 33 +++++++++
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 +++++
.../stl_shared_ptr_mistake10.res.oracle | 50 +++++++++++++
.../oracle/stl_shared_ptr_mistake5.res.oracle | 50 +++++++++++++
.../oracle/stl_shared_ptr_mistake6.res.oracle | 50 +++++++++++++
tests/stl/oracle/stl_system_error.res.oracle | 72 +++++++++++++++++++
tests/stl/oracle/stl_typeinfo.res.oracle | 17 +++++
tests/stl/oracle/stl_unique_ptr.res.oracle | 17 +++++
12 files changed, 390 insertions(+)
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index 52d46f48..c0a55022 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -977,6 +977,18 @@ char *__fc_env[4096];
*/
char *getenv(char const *name);
+/*@ requires valid_name: valid_read_string(name);
+ ensures
+ null_or_valid_result:
+ \result ≡ \null ∨
+ (\valid(\result) ∧ valid_read_string(\result));
+ assigns \result;
+ assigns \result
+ \from __fc_env[0 ..], (indirect: name),
+ (indirect: *(name + (0 .. strlen{Old}(name))));
+ */
+char *secure_getenv(char const *name);
+
/*@ requires valid_string: valid_read_string(string);
assigns __fc_env[0 ..], \result;
assigns __fc_env[0 ..] \from __fc_env[0 ..], string;
@@ -1283,6 +1295,16 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
int mkstemp(char *templat);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+int mkostemp(char *templat, int flags);
+
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6 + suffixlen;
requires non_negative_suffixlen: suffixlen ≥ 0;
@@ -1294,6 +1316,17 @@ int mkstemp(char *templat);
*/
int mkstemps(char *templat, int suffixlen);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6 + suffixlen;
+ requires non_negative_suffixlen: suffixlen ≥ 0;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+int mkostemps(char *templat, int suffixlen, int flags);
+
/*@ requires
valid_file_name_or_null:
file_name ≡ \null ∨ valid_read_string(file_name);
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index 6d9ce932..60c099f1 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -946,6 +946,18 @@ char *__fc_env[4096];
*/
char *getenv(char const *name);
+/*@ requires valid_name: valid_read_string(name);
+ ensures
+ null_or_valid_result:
+ \result ≡ \null ∨
+ (\valid(\result) ∧ valid_read_string(\result));
+ assigns \result;
+ assigns \result
+ \from __fc_env[0 ..], (indirect: name),
+ (indirect: *(name + (0 .. strlen{Old}(name))));
+ */
+char *secure_getenv(char const *name);
+
/*@ requires valid_string: valid_read_string(string);
assigns __fc_env[0 ..], \result;
assigns __fc_env[0 ..] \from __fc_env[0 ..], string;
@@ -1252,6 +1264,16 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
int mkstemp(char *templat);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+int mkostemp(char *templat, int flags);
+
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6 + suffixlen;
requires non_negative_suffixlen: suffixlen ≥ 0;
@@ -1263,6 +1285,17 @@ int mkstemp(char *templat);
*/
int mkstemps(char *templat, int suffixlen);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6 + suffixlen;
+ requires non_negative_suffixlen: suffixlen ≥ 0;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+int mkostemps(char *templat, int suffixlen, int flags);
+
/*@ requires
valid_file_name_or_null:
file_name ≡ \null ∨ valid_read_string(file_name);
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index e284b217..59625dd7 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -918,6 +918,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memrchr(void const *s, int c, size_t n);
+/*@ requires c_in_s: memchr((char *)s, c, \block_length(s) - 1) ≡ \true;
+ requires
+ valid: s:
+ \valid_read((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ requires
+ initialization: s:
+ \initialized((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ ensures result_valid_read: \valid_read((char *)\result);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: c), (indirect: *((unsigned char *)s + (0 ..)));
+ */
+void *rawmemchr(void const *s, int c);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
diff --git a/tests/stl/oracle/stl_bool.res.oracle b/tests/stl/oracle/stl_bool.res.oracle
index 4af3c386..829261aa 100644
--- a/tests/stl/oracle/stl_bool.res.oracle
+++ b/tests/stl/oracle/stl_bool.res.oracle
@@ -566,6 +566,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memrchr(void const *s, int c, size_t n);
+/*@ requires c_in_s: memchr((char *)s, c, \block_length(s) - 1) ≡ \true;
+ requires
+ valid: s:
+ \valid_read((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ requires
+ initialization: s:
+ \initialized((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ ensures result_valid_read: \valid_read((char *)\result);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: c), (indirect: *((unsigned char *)s + (0 ..)));
+ */
+void *rawmemchr(void const *s, int c);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index 99cabc73..1c2137f4 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -726,6 +726,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memrchr(void const *s, int c, size_t n);
+/*@ requires c_in_s: memchr((char *)s, c, \block_length(s) - 1) ≡ \true;
+ requires
+ valid: s:
+ \valid_read((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ requires
+ initialization: s:
+ \initialized((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ ensures result_valid_read: \valid_read((char *)\result);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: c), (indirect: *((unsigned char *)s + (0 ..)));
+ */
+void *rawmemchr(void const *s, int c);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index 4f6cffd8..c415a960 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -732,6 +732,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memrchr(void const *s, int c, size_t n);
+/*@ requires c_in_s: memchr((char *)s, c, \block_length(s) - 1) ≡ \true;
+ requires
+ valid: s:
+ \valid_read((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ requires
+ initialization: s:
+ \initialized((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ ensures result_valid_read: \valid_read((char *)\result);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: c), (indirect: *((unsigned char *)s + (0 ..)));
+ */
+void *rawmemchr(void const *s, int c);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index 7678d4c0..ba1f6ee9 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -747,6 +747,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memrchr(void const *s, int c, size_t n);
+/*@ requires c_in_s: memchr((char *)s, c, \block_length(s) - 1) ≡ \true;
+ requires
+ valid: s:
+ \valid_read((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ requires
+ initialization: s:
+ \initialized((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ ensures result_valid_read: \valid_read((char *)\result);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: c), (indirect: *((unsigned char *)s + (0 ..)));
+ */
+void *rawmemchr(void const *s, int c);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
@@ -3233,6 +3250,18 @@ char *__fc_env[4096];
*/
char *getenv(char const *name);
+/*@ requires valid_name: valid_read_string(name);
+ ensures
+ null_or_valid_result:
+ \result ≡ \null ∨
+ (\valid(\result) ∧ valid_read_string(\result));
+ assigns \result;
+ assigns \result
+ \from __fc_env[0 ..], (indirect: name),
+ (indirect: *(name + (0 .. strlen{Old}(name))));
+ */
+char *secure_getenv(char const *name);
+
/*@ requires valid_string: valid_read_string(string);
assigns __fc_env[0 ..], \result;
assigns __fc_env[0 ..] \from __fc_env[0 ..], string;
@@ -3539,6 +3568,16 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
int mkstemp(char *templat);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+int mkostemp(char *templat, int flags);
+
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6 + suffixlen;
requires non_negative_suffixlen: suffixlen ≥ 0;
@@ -3550,6 +3589,17 @@ int mkstemp(char *templat);
*/
int mkstemps(char *templat, int suffixlen);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6 + suffixlen;
+ requires non_negative_suffixlen: suffixlen ≥ 0;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+int mkostemps(char *templat, int suffixlen, int flags);
+
/*@ requires
valid_file_name_or_null:
file_name ≡ \null ∨ valid_read_string(file_name);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index cbcdd2f4..dafb7e18 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -728,6 +728,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memrchr(void const *s, int c, size_t n);
+/*@ requires c_in_s: memchr((char *)s, c, \block_length(s) - 1) ≡ \true;
+ requires
+ valid: s:
+ \valid_read((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ requires
+ initialization: s:
+ \initialized((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ ensures result_valid_read: \valid_read((char *)\result);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: c), (indirect: *((unsigned char *)s + (0 ..)));
+ */
+void *rawmemchr(void const *s, int c);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
@@ -3012,6 +3029,18 @@ char *__fc_env[4096];
*/
char *getenv(char const *name);
+/*@ requires valid_name: valid_read_string(name);
+ ensures
+ null_or_valid_result:
+ \result ≡ \null ∨
+ (\valid(\result) ∧ valid_read_string(\result));
+ assigns \result;
+ assigns \result
+ \from __fc_env[0 ..], (indirect: name),
+ (indirect: *(name + (0 .. strlen{Old}(name))));
+ */
+char *secure_getenv(char const *name);
+
/*@ requires valid_string: valid_read_string(string);
assigns __fc_env[0 ..], \result;
assigns __fc_env[0 ..] \from __fc_env[0 ..], string;
@@ -3318,6 +3347,16 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
int mkstemp(char *templat);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+int mkostemp(char *templat, int flags);
+
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6 + suffixlen;
requires non_negative_suffixlen: suffixlen ≥ 0;
@@ -3329,6 +3368,17 @@ int mkstemp(char *templat);
*/
int mkstemps(char *templat, int suffixlen);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6 + suffixlen;
+ requires non_negative_suffixlen: suffixlen ≥ 0;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+int mkostemps(char *templat, int suffixlen, int flags);
+
/*@ requires
valid_file_name_or_null:
file_name ≡ \null ∨ valid_read_string(file_name);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 95e22c3c..efead2b1 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -729,6 +729,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memrchr(void const *s, int c, size_t n);
+/*@ requires c_in_s: memchr((char *)s, c, \block_length(s) - 1) ≡ \true;
+ requires
+ valid: s:
+ \valid_read((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ requires
+ initialization: s:
+ \initialized((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ ensures result_valid_read: \valid_read((char *)\result);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: c), (indirect: *((unsigned char *)s + (0 ..)));
+ */
+void *rawmemchr(void const *s, int c);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
@@ -3018,6 +3035,18 @@ char *__fc_env[4096];
*/
char *getenv(char const *name);
+/*@ requires valid_name: valid_read_string(name);
+ ensures
+ null_or_valid_result:
+ \result ≡ \null ∨
+ (\valid(\result) ∧ valid_read_string(\result));
+ assigns \result;
+ assigns \result
+ \from __fc_env[0 ..], (indirect: name),
+ (indirect: *(name + (0 .. strlen{Old}(name))));
+ */
+char *secure_getenv(char const *name);
+
/*@ requires valid_string: valid_read_string(string);
assigns __fc_env[0 ..], \result;
assigns __fc_env[0 ..] \from __fc_env[0 ..], string;
@@ -3324,6 +3353,16 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
int mkstemp(char *templat);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+int mkostemp(char *templat, int flags);
+
/*@ requires valid_template: valid_string(templat);
requires template_len: strlen(templat) ≥ 6 + suffixlen;
requires non_negative_suffixlen: suffixlen ≥ 0;
@@ -3335,6 +3374,17 @@ int mkstemp(char *templat);
*/
int mkstemps(char *templat, int suffixlen);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6 + suffixlen;
+ requires non_negative_suffixlen: suffixlen ≥ 0;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+int mkostemps(char *templat, int suffixlen, int flags);
+
/*@ requires
valid_file_name_or_null:
file_name ≡ \null ∨ valid_read_string(file_name);
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index 577d46bc..7f858371 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -54,6 +54,11 @@ typedef void *exception_ptr;
struct nested_exception {
struct _frama_c_vmt *pvmt ;
};
+struct __fc_mbstate_t {
+ int __count ;
+ char __value[4] ;
+};
+typedef struct __fc_mbstate_t mbstate_t;
typedef unsigned int uid_t;
typedef long time_t;
struct __fc_FILE {
@@ -102,6 +107,8 @@ struct tm {
int tm_wday ;
int tm_yday ;
int tm_isdst ;
+ long tm_gmtoff ;
+ char const *tm_zone ;
};
typedef char char_type;
typedef wchar_t char_type;
@@ -643,6 +650,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memrchr(void const *s, int c, size_t n);
+/*@ requires c_in_s: memchr((char *)s, c, \block_length(s) - 1) ≡ \true;
+ requires
+ valid: s:
+ \valid_read((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ requires
+ initialization: s:
+ \initialized((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ ensures result_valid_read: \valid_read((char *)\result);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: c), (indirect: *((unsigned char *)s + (0 ..)));
+ */
+void *rawmemchr(void const *s, int c);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
@@ -1852,6 +1876,24 @@ int sigaction(int signum, struct sigaction const * restrict act,
int sigprocmask(int how, sigset_t const * restrict set,
sigset_t * restrict oldset);
+/*@ requires valid_set_or_null: set ≡ \null ∨ \valid_read(set);
+ requires valid_how: set ≢ \null ⇒ how ∈ {0, 2, 1};
+ requires valid_oldset_or_null: oldset ≡ \null ∨ \valid(oldset);
+ requires
+ separation: (set ≡ oldset ≡ \null) ∨ \separated(set, oldset);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ ensures
+ initialization: oldset_initialized:
+ \old(oldset) ≢ \null ∧ \result ≡ 0 ⇒
+ \initialized(\old(oldset));
+ assigns \result, *oldset;
+ assigns \result
+ \from (indirect: how), (indirect: set), (indirect: oldset);
+ assigns *oldset \from (indirect: how), (indirect: oldset);
+ */
+int pthread_sigmask(int how, sigset_t const * restrict set,
+ sigset_t * restrict oldset);
+
/*@ requires valid_mask_or_null: sigmask ≡ \null ∨ \valid_read(sigmask);
ensures result_means_interrupted: \result ≡ -1;
ensures errno_set: __fc_errno ≡ 4;
@@ -1970,6 +2012,16 @@ struct tm *gmtime(time_t const *timer);
*/
struct tm *localtime(time_t const *timer);
+/*@ requires valid_tm: \valid(tm);
+ ensures result_err_or_valid: \result ≡ -1 ∨ \result ≥ 0;
+ ensures
+ maybe_error: __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 75;
+ assigns \result, *tm;
+ assigns \result \from *tm;
+ assigns *tm \from *tm;
+ */
+time_t timegm(struct tm *tm);
+
/*@ requires dst_has_room: \valid(s + (0 .. max - 1));
requires valid_format: valid_read_string(format);
requires valid_tm: \valid_read(tm);
@@ -2499,6 +2551,26 @@ int wcscasecmp(wchar_t const *ws1, wchar_t const *ws2);
*/
wchar_t *wcsdup(wchar_t const *ws);
+/*@ requires
+ valid_mbstate: initialization:
+ ps ≡ \null ∨ (\valid_read(ps) ∧ \initialized(ps));
+ ensures ok_or_error: \result ≥ 0;
+ assigns \result;
+ assigns \result \from (indirect: ps), (indirect: *ps);
+ */
+int mbsinit(mbstate_t const *ps);
+
+/*@ assigns \result, *pwc, *ps;
+ assigns \result
+ \from (indirect: *(s + (0 .. n))), (indirect: n), (indirect: ps);
+ assigns *pwc
+ \from (indirect: *(s + (0 .. n))), (indirect: n), (indirect: ps);
+ assigns *ps
+ \from (indirect: *(s + (0 .. n))), (indirect: n), (indirect: ps);
+ */
+size_t mbrtowc(wchar_t * restrict pwc, char const * restrict s, size_t n,
+ mbstate_t * restrict ps);
+
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid_read(c2);
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index 89634c84..8017c62c 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 *memrchr(void const *s, int c, size_t n);
+/*@ requires c_in_s: memchr((char *)s, c, \block_length(s) - 1) ≡ \true;
+ requires
+ valid: s:
+ \valid_read((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ requires
+ initialization: s:
+ \initialized((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ ensures result_valid_read: \valid_read((char *)\result);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: c), (indirect: *((unsigned char *)s + (0 ..)));
+ */
+void *rawmemchr(void const *s, int c);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
diff --git a/tests/stl/oracle/stl_unique_ptr.res.oracle b/tests/stl/oracle/stl_unique_ptr.res.oracle
index e4a66590..042d9388 100644
--- a/tests/stl/oracle/stl_unique_ptr.res.oracle
+++ b/tests/stl/oracle/stl_unique_ptr.res.oracle
@@ -1225,6 +1225,23 @@ void *memchr(void const *s, int c, size_t n);
*/
void *memrchr(void const *s, int c, size_t n);
+/*@ requires c_in_s: memchr((char *)s, c, \block_length(s) - 1) ≡ \true;
+ requires
+ valid: s:
+ \valid_read((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ requires
+ initialization: s:
+ \initialized((unsigned char *)s +
+ (0 .. memchr_off((char *)s, c, \block_length(s) - 1)));
+ ensures result_valid_read: \valid_read((char *)\result);
+ ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: c), (indirect: *((unsigned char *)s + (0 ..)));
+ */
+void *rawmemchr(void const *s, int c);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
--
GitLab