From 47462b73c0a969d83b518ce6098f09958d81e73b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 2 Dec 2019 15:35:43 +0100
Subject: [PATCH] [tests] update oracles
---
tests/basic/oracle/aggregate.res.oracle | 8 +
tests/basic/oracle/placement_new.res.oracle | 25 +-
tests/basic/oracle/placement_newb.res.oracle | 25 +-
tests/basic/oracle/ptr_array_decls.res.oracle | 8 +
tests/basic/oracle/static_1.res.oracle | 3 +-
tests/bugs/oracle/issue11.res.oracle | 1 +
tests/bugs/oracle/issue23.res.oracle | 1 +
tests/bugs/oracle/issue24.res.oracle | 9 +-
tests/bugs/oracle/issue27-pred.res.oracle | 3 +-
tests/bugs/oracle/logiccast.res.oracle | 7 +-
tests/bugs/oracle/term.res.oracle | 1 +
.../oracle/array_object_bts1739.res.oracle | 8 +
tests/ppwp/oracle/expand.res.oracle | 1 +
tests/ppwp/oracle/expandf.res.oracle | 1 +
tests/ppwp/oracle/simple.res.oracle | 1 +
tests/ppwp/oracle/z.res.oracle | 1 +
tests/specs/oracle/wp_empty_struct.res.oracle | 1 +
tests/stl/oracle/stl_algorithm.res.oracle | 45 +++-
tests/stl/oracle/stl_functional.res.oracle | 17 ++
tests/stl/oracle/stl_iterator.res.oracle | 64 ++---
tests/stl/oracle/stl_memory.res.oracle | 25 +-
.../stl_shared_ptr_mistake10.res.oracle | 25 +-
.../oracle/stl_shared_ptr_mistake5.res.oracle | 25 +-
.../oracle/stl_shared_ptr_mistake6.res.oracle | 25 +-
tests/stl/oracle/stl_system_error.err.oracle | 6 +-
tests/stl/oracle/stl_system_error.res.oracle | 245 +++++++++++++-----
tests/stl/oracle/stl_typeinfo.res.oracle | 17 ++
tests/stl/oracle/stl_utility.err.oracle | 0
.../oracle/template_variadic.res.oracle | 32 +--
29 files changed, 454 insertions(+), 176 deletions(-)
delete mode 100644 tests/stl/oracle/stl_utility.err.oracle
diff --git a/tests/basic/oracle/aggregate.res.oracle b/tests/basic/oracle/aggregate.res.oracle
index 09fb0cd8..159a4fd1 100644
--- a/tests/basic/oracle/aggregate.res.oracle
+++ b/tests/basic/oracle/aggregate.res.oracle
@@ -108,10 +108,18 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
+void B::Dtor(struct B const *this);
+
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
+/*@ requires \valid_read(this); */
+void B::Dtor(struct B const *this)
+{
+ return;
+}
+
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "B",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index 8499f534..d47b5e1f 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -270,6 +270,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ int *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
@@ -827,10 +844,6 @@ void *calloc(size_t nmemb, size_t size);
*/
void *realloc(void *ptr, size_t size);
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
-void abort(void);
-
/*@ assigns \result;
assigns \result \from \nothing; */
int atexit(void (*func)(void));
@@ -839,10 +852,6 @@ int atexit(void (*func)(void));
assigns \result \from \nothing; */
int at_quick_exit(void (*func)(void));
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
-void exit(int status);
-
/*@ ensures never_terminates: \false;
assigns \nothing; */
void _Exit(int status);
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index 2478a686..b0e3e688 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -239,6 +239,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ int *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
@@ -796,10 +813,6 @@ void *calloc(size_t nmemb, size_t size);
*/
void *realloc(void *ptr, size_t size);
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
-void abort(void);
-
/*@ assigns \result;
assigns \result \from \nothing; */
int atexit(void (*func)(void));
@@ -808,10 +821,6 @@ int atexit(void (*func)(void));
assigns \result \from \nothing; */
int at_quick_exit(void (*func)(void));
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
-void exit(int status);
-
/*@ ensures never_terminates: \false;
assigns \nothing; */
void _Exit(int status);
diff --git a/tests/basic/oracle/ptr_array_decls.res.oracle b/tests/basic/oracle/ptr_array_decls.res.oracle
index b81974ba..d63d204f 100644
--- a/tests/basic/oracle/ptr_array_decls.res.oracle
+++ b/tests/basic/oracle/ptr_array_decls.res.oracle
@@ -26,10 +26,18 @@ struct S0 {
int f0 ;
int f1 ;
};
+void S0::Dtor(struct S0 const *this);
+
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
+/*@ requires \valid_read(this); */
+void S0::Dtor(struct S0 const *this)
+{
+ return;
+}
+
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "S0",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
diff --git a/tests/basic/oracle/static_1.res.oracle b/tests/basic/oracle/static_1.res.oracle
index 16deb3df..f6602e9e 100644
--- a/tests/basic/oracle/static_1.res.oracle
+++ b/tests/basic/oracle/static_1.res.oracle
@@ -50,7 +50,8 @@ int Sm_get(void);
static int x;
/*@ assigns \result;
assigns \result
- \from (indirect: *(__frama_c_arg_0 + (0 ..))), param1, param0;
+ \from (indirect: *(__frama_c_arg_0 + (0 ..))), (indirect: param1),
+ (indirect: param0);
*/
int printf_va_1(char const *__frama_c_arg_0, int param0, int param1);
diff --git a/tests/bugs/oracle/issue11.res.oracle b/tests/bugs/oracle/issue11.res.oracle
index ad84c99e..4aea3552 100644
--- a/tests/bugs/oracle/issue11.res.oracle
+++ b/tests/bugs/oracle/issue11.res.oracle
@@ -5,6 +5,7 @@ Now output intermediate result
[wp] 2 goals scheduled
[wp] [Qed] Goal typed___fc_init_ZN1aE1d_call__ZN1a1bIcEEC1v_ZN1a1bIcEEC1v_requires : Valid
[wp] [Qed] Goal typed___fc_init_ZN1aE1c_call__ZN1a1bIvEEC1v_ZN1a1bIvEEC1v_requires : Valid
+[wp] [Cache] not used
[wp] Proved goals: 2 / 2
Qed: 2
/* Generated by Frama-C */
diff --git a/tests/bugs/oracle/issue23.res.oracle b/tests/bugs/oracle/issue23.res.oracle
index 8d7efd4f..fe474be8 100644
--- a/tests/bugs/oracle/issue23.res.oracle
+++ b/tests/bugs/oracle/issue23.res.oracle
@@ -5,6 +5,7 @@ Now output intermediate result
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_Z1m_assert_2 : Valid
[wp] [Qed] Goal typed_Z1m_assert : Valid
+[wp] [Cache] not used
[wp] Proved goals: 2 / 2
Qed: 2
/* Generated by Frama-C */
diff --git a/tests/bugs/oracle/issue24.res.oracle b/tests/bugs/oracle/issue24.res.oracle
index 2104e5f6..8ea826cb 100644
--- a/tests/bugs/oracle/issue24.res.oracle
+++ b/tests/bugs/oracle/issue24.res.oracle
@@ -5,10 +5,11 @@ Now output intermediate result
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_Z1m_assert_4 : Valid
[wp] [Qed] Goal typed_Z1m_assert_5 : Valid
-[wp] [Alt-Ergo] Goal typed_Z1m_assert_3 : Valid
-[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid
-[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid
-[wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_3 : Valid (5)
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_2 : Valid (4)
+[wp] [Alt-Ergo] Goal typed_Z1m_assert : Valid (3)
+[wp] [Alt-Ergo] Goal typed_Z1m_assert_6 : Valid (6)
+[wp] [Cache] updated:4
[wp] Proved goals: 6 / 6
Qed: 2
Alt-Ergo: 4 (6)
diff --git a/tests/bugs/oracle/issue27-pred.res.oracle b/tests/bugs/oracle/issue27-pred.res.oracle
index 10a0fb31..1ab770b4 100644
--- a/tests/bugs/oracle/issue27-pred.res.oracle
+++ b/tests/bugs/oracle/issue27-pred.res.oracle
@@ -3,8 +3,9 @@ Now output intermediate result
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid
[wp] [Alt-Ergo] Goal typed_Z3posi_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid (7)
+[wp] [Cache] updated:1
[wp] Proved goals: 2 / 2
Qed: 0
Alt-Ergo: 2 (7)
diff --git a/tests/bugs/oracle/logiccast.res.oracle b/tests/bugs/oracle/logiccast.res.oracle
index 55da2461..565d61b3 100644
--- a/tests/bugs/oracle/logiccast.res.oracle
+++ b/tests/bugs/oracle/logiccast.res.oracle
@@ -3,15 +3,16 @@ Now output intermediate result
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unknown
[wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Unknown
+[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unknown
+[wp] [Cache] updated:2
[wp] Proved goals: 0 / 2
Alt-Ergo: 0 (unknown: 2)
[wp] Warning: Memory model hypotheses for function '_Z1mPv':
- /*@ behavior typed: requires \separated(&base,r); */
+ /*@ behavior typed: requires \separated(&base,r+(..)); */
void _Z1mPv(void *r);
[wp] Warning: Memory model hypotheses for function '_Z1nPc':
- /*@ behavior typed: requires \separated(&base,r); */
+ /*@ behavior typed: requires \separated(&base,r+(..)); */
void _Z1nPc(char *r);
/* Generated by Frama-C */
char *base;
diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle
index a3d27a6d..4c75afb8 100644
--- a/tests/bugs/oracle/term.res.oracle
+++ b/tests/bugs/oracle/term.res.oracle
@@ -9,6 +9,7 @@ Now output intermediate result
[wp] [Qed] Goal typed_Z3m3a_c_ensures : Valid
[wp] [Qed] Goal typed_Z2m3_c_ensures : Valid
[wp] [Qed] Goal typed_Z2m2_ensures : Valid
+[wp] [Cache] not used
[wp] Proved goals: 3 / 3
Qed: 3
/* Generated by Frama-C */
diff --git a/tests/class/oracle/array_object_bts1739.res.oracle b/tests/class/oracle/array_object_bts1739.res.oracle
index 3a103a88..68271bb0 100644
--- a/tests/class/oracle/array_object_bts1739.res.oracle
+++ b/tests/class/oracle/array_object_bts1739.res.oracle
@@ -33,6 +33,8 @@ void vector::Ctor(struct vector const *this,
void vector::Ctor(struct vector const *this, struct vector *__frama_c_arg_0);
+void vector::Dtor(struct vector const *this);
+
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
@@ -62,6 +64,12 @@ void vector::Ctor(struct vector const *this, struct vector *__frama_c_arg_0)
return;
}
+/*@ requires \valid_read(this); */
+void vector::Dtor(struct vector const *this)
+{
+ return;
+}
+
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "vector",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
diff --git a/tests/ppwp/oracle/expand.res.oracle b/tests/ppwp/oracle/expand.res.oracle
index 51e6b1b0..258b33c6 100644
--- a/tests/ppwp/oracle/expand.res.oracle
+++ b/tests/ppwp/oracle/expand.res.oracle
@@ -4,6 +4,7 @@ Now output intermediate result
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_Z1m_ensures : Valid
+[wp] [Cache] not used
[wp] Proved goals: 1 / 1
Qed: 1
/* Generated by Frama-C */
diff --git a/tests/ppwp/oracle/expandf.res.oracle b/tests/ppwp/oracle/expandf.res.oracle
index b3239b7f..69cf5301 100644
--- a/tests/ppwp/oracle/expandf.res.oracle
+++ b/tests/ppwp/oracle/expandf.res.oracle
@@ -4,6 +4,7 @@ Now output intermediate result
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_Z1m_ensures : Valid
+[wp] [Cache] not used
[wp] Proved goals: 1 / 1
Qed: 1
/* Generated by Frama-C */
diff --git a/tests/ppwp/oracle/simple.res.oracle b/tests/ppwp/oracle/simple.res.oracle
index 80373643..6812a5e8 100644
--- a/tests/ppwp/oracle/simple.res.oracle
+++ b/tests/ppwp/oracle/simple.res.oracle
@@ -4,6 +4,7 @@ Now output intermediate result
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_Z1m_ensures : Valid
+[wp] [Cache] not used
[wp] Proved goals: 1 / 1
Qed: 1
/* Generated by Frama-C */
diff --git a/tests/ppwp/oracle/z.res.oracle b/tests/ppwp/oracle/z.res.oracle
index fbc8797c..36b86705 100644
--- a/tests/ppwp/oracle/z.res.oracle
+++ b/tests/ppwp/oracle/z.res.oracle
@@ -4,6 +4,7 @@ Now output intermediate result
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_Z1m_ensures : Valid
+[wp] [Cache] not used
[wp] Proved goals: 1 / 1
Qed: 1
/* Generated by Frama-C */
diff --git a/tests/specs/oracle/wp_empty_struct.res.oracle b/tests/specs/oracle/wp_empty_struct.res.oracle
index 43a2493d..1bb44f53 100644
--- a/tests/specs/oracle/wp_empty_struct.res.oracle
+++ b/tests/specs/oracle/wp_empty_struct.res.oracle
@@ -5,5 +5,6 @@ Now output intermediate result
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_ZN6Point2E3foo_ensures_2 : Valid
[wp] [Qed] Goal typed_ZN6Point2E3foo_ensures : Valid
+[wp] [Cache] not used
[wp] Proved goals: 2 / 2
Qed: 2
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index 0cfb55d0..e58389aa 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -840,6 +840,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ int *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
@@ -2681,8 +2698,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
/*@ requires \valid_read(pred); */
-struct unary_negate<bool*,<abst>> not1<bool*,<abst>>(_Bool (* const *pred)(
- int ))
+struct unary_negate<bool*,<abst>> not1<bool*,<abst>>(_Bool (* const *pred)
+ (int ))
{
struct unary_negate<bool*,<abst>> __fc_tmp_2;
unary_negate<bool*,<abst>>::Ctor(& __fc_tmp_2,pred);
@@ -2690,8 +2707,8 @@ struct unary_negate<bool*,<abst>> not1<bool*,<abst>>(_Bool (* const *pred)(
}
/*@ requires \valid_read(pred); */
-struct unary_negate<std::reference_wrapper<bool&,<abst>>> not1<std::reference_wrapper<bool&,<abst>>>(
-struct reference_wrapper<bool&,<abst>> const *pred)
+struct unary_negate<std::reference_wrapper<bool&,<abst>>> not1<std::reference_wrapper<bool&,<abst>>>
+(struct reference_wrapper<bool&,<abst>> const *pred)
{
struct unary_negate<std::reference_wrapper<bool&,<abst>>> __fc_tmp_3;
unary_negate<std::reference_wrapper<bool&,<abst>>>::Ctor(& __fc_tmp_3,pred);
@@ -2946,8 +2963,8 @@ _Bool none_of<int*,bool*,<abst>>(int *first, int *last, _Bool (*pred)(int ))
return tmp_0;
}
-void (*for_each<int*,void*,<abst>>(int *first, int *last, void (*f)(int )))(
-int )
+void (*for_each<int*,void*,<abst>>(int *first, int *last, void (*f)(int )))
+(int )
{
void (*__retres)(int );
type *tmp_0;
@@ -2997,9 +3014,9 @@ int *find_if<int*,bool&,<abst>>(int *first, int *last, _Bool (*pred)(int ))
return_label: return __retres;
}
-int *find_if<int*,std::unary_negate<std::reference_wrapper<bool&,<abst>>>>(
-int *first, int *last,
-struct unary_negate<std::reference_wrapper<bool&,<abst>>> pred)
+int *find_if<int*,std::unary_negate<std::reference_wrapper<bool&,<abst>>>>
+(int *first, int *last,
+ struct unary_negate<std::reference_wrapper<bool&,<abst>>> pred)
{
int *__retres;
int **it = & first;
@@ -3324,11 +3341,11 @@ _Bool is_permutation<int*,int*>(int *first1, int *last1, int *first2)
return_label: return __retres;
}
-void UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE__cons(
-struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_ const *__fc_closure,
-_Bool (*__fc_func)(struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_ const *,
- value_type ),
-struct equal_to<int> pred, int *it1)
+void UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE__cons
+(struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_ const *__fc_closure,
+ _Bool (*__fc_func)(struct UlN3std15iterator_traitsIPiEE10value_typeEUc4predN3stdE8equal_toIiE3it1PiE_ const *,
+ value_type ),
+ struct equal_to<int> pred, int *it1)
{
__fc_closure->__fc_lambda_apply = __fc_func;
equal_to<int>::Ctor(& __fc_closure->pred,
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index 8d2d725b..b6003ee9 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -569,6 +569,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ int *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
diff --git a/tests/stl/oracle/stl_iterator.res.oracle b/tests/stl/oracle/stl_iterator.res.oracle
index 38663208..71da5239 100644
--- a/tests/stl/oracle/stl_iterator.res.oracle
+++ b/tests/stl/oracle/stl_iterator.res.oracle
@@ -377,27 +377,27 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0);
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0);
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0);
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0);
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this);
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this);
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0);
+struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0);
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0);
+struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0);
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this);
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
@@ -407,9 +407,9 @@ struct _frama_c_vmt_content _frama_c_vmt[1];
requires \valid_read(this);
requires \valid_read(__frama_c_arg_0);
*/
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0)
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0)
{
return;
}
@@ -418,16 +418,16 @@ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__fram
requires \valid_read(this);
requires \valid(__frama_c_arg_0);
*/
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0)
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0)
{
return;
}
/*@ requires \valid_read(this); */
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
{
return;
}
@@ -436,9 +436,9 @@ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
requires \valid_read(__frama_c_arg_0);
ensures \valid(\result);
*/
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0)
+struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0)
{
return this;
}
@@ -447,16 +447,16 @@ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__fram
requires \valid(__frama_c_arg_0);
ensures \valid(\result);
*/
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0)
+struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *operator=
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *this,
+ struct iterator<std::random_access_iterator_tag,int,int,int*,int&> *__frama_c_arg_0)
{
return this;
}
/*@ requires \valid_read(this); */
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor(
-struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+(struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
{
return;
}
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index bc416e89..6b9236e1 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -341,8 +341,8 @@ void swap<std::default_delete<int>>(struct default_delete<int> *a,
/*@ requires \valid(t);
ensures \valid(\result); */
-struct unique_ptr<int[],std::default_delete<int[]>> *forward<std::unique_ptr<int[],std::default_delete<int[]>>>(
-type *t);
+struct unique_ptr<int[],std::default_delete<int[]>> *forward<std::unique_ptr<int[],std::default_delete<int[]>>>
+(type *t);
/*@ requires \valid(t);
ensures \valid(\result); */
@@ -572,6 +572,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ int *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
@@ -2468,8 +2485,8 @@ void swap(struct unique_ptr<int[],std::default_delete<int[]>> *this,
/*@ requires \valid(t);
ensures \valid(\result); */
-struct unique_ptr<int[],std::default_delete<int[]>> *forward<std::unique_ptr<int[],std::default_delete<int[]>>>(
-type *t)
+struct unique_ptr<int[],std::default_delete<int[]>> *forward<std::unique_ptr<int[],std::default_delete<int[]>>>
+(type *t)
{
return t;
}
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index db40de8c..6c28ec29 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -522,6 +522,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ int *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
@@ -3287,10 +3304,6 @@ void *calloc(size_t nmemb, size_t size);
*/
void *realloc(void *ptr, size_t size);
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
-void abort(void);
-
/*@ assigns \result;
assigns \result \from \nothing; */
int atexit(void (*func)(void));
@@ -3299,10 +3312,6 @@ int atexit(void (*func)(void));
assigns \result \from \nothing; */
int at_quick_exit(void (*func)(void));
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
-void exit(int status);
-
/*@ ensures never_terminates: \false;
assigns \nothing; */
void _Exit(int status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index f0e6d9a1..1c2574f4 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -503,6 +503,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ int *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
@@ -3040,10 +3057,6 @@ void *calloc(size_t nmemb, size_t size);
*/
void *realloc(void *ptr, size_t size);
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
-void abort(void);
-
/*@ assigns \result;
assigns \result \from \nothing; */
int atexit(void (*func)(void));
@@ -3052,10 +3065,6 @@ int atexit(void (*func)(void));
assigns \result \from \nothing; */
int at_quick_exit(void (*func)(void));
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
-void exit(int status);
-
/*@ ensures never_terminates: \false;
assigns \nothing; */
void _Exit(int status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 1c13d168..4fda65f9 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -504,6 +504,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ int *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
@@ -3046,10 +3063,6 @@ void *calloc(size_t nmemb, size_t size);
*/
void *realloc(void *ptr, size_t size);
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
-void abort(void);
-
/*@ assigns \result;
assigns \result \from \nothing; */
int atexit(void (*func)(void));
@@ -3058,10 +3071,6 @@ int atexit(void (*func)(void));
assigns \result \from \nothing; */
int at_quick_exit(void (*func)(void));
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
-void exit(int status);
-
/*@ ensures never_terminates: \false;
assigns \nothing; */
void _Exit(int status);
diff --git a/tests/stl/oracle/stl_system_error.err.oracle b/tests/stl/oracle/stl_system_error.err.oracle
index cf4d03f0..9712de6c 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:208:47: types are not convertible
FRAMAC_SHARE/libc/signal.h:223:28: Expecting ';' after requires clause
-FRAMAC_SHARE/libc/time.h:219:45: types are not convertible
-FRAMAC_SHARE/libc/time.h:266:43: types are not convertible
+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 ec1639e8..1755439f 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -426,6 +426,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ int *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
@@ -1630,6 +1647,21 @@ struct sigaction *__fc_p_sigaction = __fc_sigaction;
requires valid_oldact_or_null: oldact ≡ \null ∨ \valid(oldact);
requires valid_read_act_or_null: act ≡ \null ∨ \valid_read(act);
requires separated_acts: separation: \separated(act, oldact);
+ ensures
+ act_changed:
+ \old(act) ≡ \null ∨
+ \subset(*(__fc_p_sigaction + \old(signum)), *\old(act));
+ ensures
+ oldact_assigned:
+ \old(oldact) ≡ \null ∨
+ *\old(oldact) ∈ *(__fc_p_sigaction + \old(signum));
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns *oldact, *(__fc_p_sigaction + signum), \result;
+ assigns *oldact \from __fc_p_sigaction;
+ assigns *(__fc_p_sigaction + signum) \from *act;
+ assigns \result
+ \from (indirect: signum), (indirect: act), (indirect: *act),
+ (indirect: oldact), (indirect: *oldact);
*/
int sigaction(int signum, struct sigaction const * __restrict act,
struct sigaction * __restrict oldact);
@@ -1661,9 +1693,10 @@ clock_t clock(void);
assigns \result \from time1, time0; */
double difftime(time_t time1, time_t time0);
-/*@ assigns *timeptr, \result;
+/*@ requires valid_timeptr: \valid(timeptr);
+ assigns *timeptr, \result;
assigns *timeptr \from *timeptr;
- assigns \result \from *timeptr;
+ assigns \result \from (indirect: *timeptr);
*/
time_t mktime(struct tm *timeptr);
@@ -1712,7 +1745,8 @@ void __fc_init__fc_time_tm(void)
}
struct tm * const __fc_p_time_tm = & __fc_time_tm;
-/*@ ensures
+/*@ requires valid_timer: \valid_read(timer);
+ ensures
result_null_or_internal_tm:
\result ≡ &__fc_time_tm ∨ \result ≡ \null;
assigns \result, __fc_time_tm;
@@ -1721,7 +1755,8 @@ struct tm * const __fc_p_time_tm = & __fc_time_tm;
*/
struct tm *gmtime(time_t const *timer);
-/*@ ensures
+/*@ requires valid_timer: \valid_read(timer);
+ ensures
result_null_or_internal_tm:
\result ≡ &__fc_time_tm ∨ \result ≡ \null;
assigns \result, __fc_time_tm;
@@ -1813,10 +1848,56 @@ axiomatic nanosleep_predicates {
assumes relative_time: (flags & 1) ≡ 0;
assumes interrupted: __fc_interrupted ≢ 0;
assumes no_einval: valid_clock_id(clock_id);
+ ensures result_interrupted: \result ≡ 4;
+ ensures
+ interrupted_remaining: initialization:
+ \old(rmtp) ≢ \null ⇒
+ \initialized(&\old(rmtp)->tv_sec) ∧
+ \initialized(&\old(rmtp)->tv_nsec);
+ ensures
+ interrupted_remaining_decreases:
+ \old(rmtp) ≢ \null ⇒
+ \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
+ \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
+ ensures
+ remaining_valid:
+ \old(rmtp) ≢ \null ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
+ assigns \result, *rmtp;
+ assigns \result
+ \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
+ (indirect: *rqtp);
+ assigns *rmtp
+ \from __fc_time, (indirect: clock_id), (indirect: rqtp),
+ (indirect: *rqtp), (indirect: rmtp);
+
+ behavior relative_no_error:
+ assumes relative_time: (flags & 1) ≡ 0;
+ assumes not_interrupted: __fc_interrupted ≡ 0;
+ assumes no_einval: valid_clock_id(clock_id);
+ ensures result_ok: \result ≡ 0;
assigns \result;
assigns \result
\from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
(indirect: *rqtp);
+
+ behavior relative_invalid_clock_id:
+ assumes relative_time: (flags & 1) ≡ 0;
+ assumes not_interrupted: __fc_interrupted ≡ 0;
+ assumes einval: ¬valid_clock_id(clock_id);
+ ensures result_einval: \result ≡ 22;
+ assigns \result;
+ assigns \result
+ \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
+ (indirect: *rqtp);
+
+ complete behaviors relative_invalid_clock_id,
+ relative_no_error,
+ relative_interrupted,
+ absolute;
+ disjoint behaviors relative_invalid_clock_id,
+ relative_no_error,
+ relative_interrupted,
+ absolute;
*/
int clock_nanosleep(clockid_t clock_id, int flags,
struct timespec const *rqtp, struct timespec *rmtp);
@@ -1827,14 +1908,30 @@ int clock_nanosleep(clockid_t clock_id, int flags,
\initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec);
requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000;
requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp);
- assigns \result;
+ ensures result_elapsed_or_interrupted: \result ≡ 0 ∨ \result ≡ -1;
+ ensures
+ interrupted_remaining: initialization:
+ \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
+ \initialized(&\old(rmtp)->tv_sec) ∧
+ \initialized(&\old(rmtp)->tv_nsec);
+ ensures
+ interrupted_remaining_decreases:
+ \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
+ \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥
+ \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec;
+ ensures
+ interrupted_remaining_valid:
+ \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
+ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
+ assigns \result, *rmtp;
assigns \result
\from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp);
+ assigns *rmtp
+ \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp),
+ (indirect: rmtp);
*/
int nanosleep(struct timespec const *rqtp, struct timespec *rmtp);
-void tzset(void);
-
int daylight;
long timezone;
char *tzname[2];
@@ -1843,42 +1940,18 @@ char *tzname[2];
*/
void tzset(void);
-/*@ ensures
- result_null_or_inside_s:
- \result ≡ \null ∨ \subset(\result, \old(s) + (0 .. \old(n) - 1));
- assigns \result;
- assigns \result
- \from s, (indirect: *(s + (0 .. n - 1))), (indirect: c), (indirect: n);
- */
-int *wmemchr(int const *s, int c, size_t n);
-
-/*@ assigns \result;
- assigns \result
- \from (indirect: *(s1 + (0 .. n - 1))),
- (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
- */
-int wmemcmp(int const *s1, int const *s2, size_t n);
-
-/*@ requires
- src: dest: separation:
- \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
+/*@ requires valid_src: \valid_read(src + (0 .. n - 1));
+ requires valid_dest: \valid(dest + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 .. n - 1)), \result;
assigns *(dest + (0 .. n - 1))
\from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
assigns \result \from dest;
*/
-int *wmemcpy(int * __restrict dest, int const * __restrict src, size_t n);
-
-/*@ ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest + (0 .. n - 1)), \result;
- assigns *(dest + (0 .. n - 1))
- \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
- assigns \result \from dest;
- */
int *wmemmove(int *dest, int const *src, size_t n);
-/*@ ensures result_ptr: \result ≡ \old(wcs);
+/*@ requires valid_wcs: \valid(wcs + (0 .. n - 1));
+ ensures result_ptr: \result ≡ \old(wcs);
ensures
wcs: initialization: \initialized(\old(wcs) + (0 .. \old(n) - 1));
ensures
@@ -1889,7 +1962,17 @@ int *wmemmove(int *dest, int const *src, size_t n);
*/
int *wmemset(int *wcs, int wc, size_t n);
-/*@ ensures result_ptr: \result ≡ \old(dest);
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+ requires valid_wstring_dest: valid_wstring(dest);
+ requires
+ room_for_concatenation:
+ \valid(dest + (wcslen(dest) .. wcslen(dest) + wcslen(src)));
+ requires
+ separation:
+ \separated(
+ dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
+ );
+ ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 ..)), \result;
assigns *(dest + (0 ..))
\from *(dest + (0 ..)), (indirect: dest), *(src + (0 ..)),
@@ -1907,28 +1990,46 @@ int *wcscat(int * __restrict dest, int const * __restrict src);
*/
int *wcschr(int const *wcs, int wc);
-/*@ assigns \result;
+/*@ requires valid_wstring_s1: valid_read_wstring(s1);
+ requires valid_wstring_s2: valid_read_wstring(s2);
+ assigns \result;
assigns \result
\from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
*/
int wcscmp(int const *s1, int const *s2);
-/*@ ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest + (0 ..)), \result;
- assigns *(dest + (0 ..))
- \from *(src + (0 ..)), (indirect: src), *(dest + (0 ..)),
- (indirect: dest);
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+ requires room_wstring: \valid(dest + (0 .. wcslen(src)));
+ requires
+ separation:
+ \separated(dest + (0 .. wcslen(src)), src + (0 .. wcslen(src)));
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *(dest + (0 .. wcslen{Old}(src))), \result;
+ assigns *(dest + (0 .. wcslen{Old}(src)))
+ \from *(src + (0 .. wcslen{Old}(src))), (indirect: src);
assigns \result \from dest;
*/
int *wcscpy(int * __restrict dest, int const * __restrict src);
-/*@ assigns \result;
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
+ assigns \result;
assigns \result
\from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
*/
size_t wcscspn(int const *wcs, int const *accept);
-/*@ assigns *(dest + (0 ..)), \result;
+/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
+ requires valid_wstring_dest: valid_wstring(dest);
+ requires
+ room_for_concatenation:
+ \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
+ requires
+ separation:
+ \separated(
+ dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
+ );
+ assigns *(dest + (0 ..)), \result;
assigns *(dest + (0 ..))
\from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
(indirect: src), (indirect: n);
@@ -1938,7 +2039,9 @@ size_t wcscspn(int const *wcs, int const *accept);
*/
size_t wcslcat(int * __restrict dest, int const * __restrict src, size_t n);
-/*@ requires
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+ requires room_nwstring: \valid(dest + (0 .. n));
+ requires
src: dest: separation:
\separated(dest + (0 .. n - 1), src + (0 .. n - 1));
assigns *(dest + (0 .. n - 1)), \result;
@@ -1951,12 +2054,23 @@ size_t wcslcat(int * __restrict dest, int const * __restrict src, size_t n);
size_t wcslcpy(int *dest, int const *src, size_t n);
/*@ requires valid_string_s: valid_read_wstring(s);
+ ensures result_is_length: \result ≡ wcslen(\old(s));
assigns \result;
- assigns \result \from (indirect: *(s + (0 ..)));
+ assigns \result \from (indirect: *(s + (0 .. wcslen{Old}(s))));
*/
size_t wcslen(int const *s);
-/*@ ensures result_ptr: \result ≡ \old(dest);
+/*@ requires valid_nwstring_src: valid_read_nwstring(src, n);
+ requires valid_wstring_dest: valid_wstring(dest);
+ requires
+ room_for_concatenation:
+ \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n)));
+ requires
+ separation:
+ \separated(
+ dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src))
+ );
+ ensures result_ptr: \result ≡ \old(dest);
assigns *(dest + (0 ..)), \result;
assigns *(dest + (0 ..))
\from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)),
@@ -1965,17 +2079,22 @@ size_t wcslen(int const *s);
*/
int *wcsncat(int * __restrict dest, int const * __restrict src, size_t n);
-/*@ assigns \result;
+/*@ requires valid_wstring_s1: valid_read_wstring(s1);
+ requires valid_wstring_s2: valid_read_wstring(s2);
+ assigns \result;
assigns \result
\from (indirect: *(s1 + (0 .. n - 1))),
(indirect: *(s2 + (0 .. n - 1))), (indirect: n);
*/
int wcsncmp(int const *s1, int const *s2, size_t n);
-/*@ requires
+/*@ requires valid_wstring_src: valid_read_wstring(src);
+ requires room_nwstring: \valid(dest + (0 .. n - 1));
+ requires
src: dest: separation:
\separated(dest + (0 .. n - 1), src + (0 .. n - 1));
ensures result_ptr: \result ≡ \old(dest);
+ ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
assigns *(dest + (0 .. n - 1)), \result;
assigns *(dest + (0 .. n - 1))
\from *(src + (0 .. n - 1)), (indirect: src), (indirect: n);
@@ -1983,7 +2102,9 @@ int wcsncmp(int const *s1, int const *s2, size_t n);
*/
int *wcsncpy(int * __restrict dest, int const * __restrict src, size_t n);
-/*@ ensures
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
+ ensures
result_null_or_inside_wcs:
\result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
assigns \result;
@@ -1992,21 +2113,28 @@ int *wcsncpy(int * __restrict dest, int const * __restrict src, size_t n);
*/
int *wcspbrk(int const *wcs, int const *accept);
-/*@ ensures
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ ensures
result_null_or_inside_wcs:
\result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..));
assigns \result;
- assigns \result \from wcs, (indirect: *(wcs + (0 ..))), (indirect: wc);
+ assigns \result
+ \from wcs, (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))), (indirect: wc);
*/
int *wcsrchr(int const *wcs, int wc);
-/*@ assigns \result;
+/*@ requires valid_wstring_wcs: valid_read_wstring(wcs);
+ requires valid_wstring_accept: valid_read_wstring(accept);
+ assigns \result;
assigns \result
- \from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..)));
+ \from (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))),
+ (indirect: *(accept + (0 .. wcslen{Old}(accept))));
*/
size_t wcsspn(int const *wcs, int const *accept);
-/*@ ensures
+/*@ requires valid_wstring_haystack: valid_read_wstring(haystack);
+ requires valid_wstring_needle: valid_read_wstring(needle);
+ ensures
result_null_or_inside_haystack:
\result ≡ \null ∨ \subset(\result, \old(haystack) + (0 ..));
assigns \result;
@@ -2016,13 +2144,14 @@ size_t wcsspn(int const *wcs, int const *accept);
*/
int *wcsstr(int const *haystack, int const *needle);
-/*@ requires valid_stream: \valid(stream);
+/*@ requires room_nwstring: \valid(ws + (0 .. n - 1));
+ requires valid_stream: \valid(stream);
ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(ws);
ensures
terminated_string_on_success:
\result ≢ \null ⇒ valid_wstring(\old(ws));
- assigns *(ws + (0 .. n)), \result;
- assigns *(ws + (0 .. n)) \from (indirect: n), (indirect: *stream);
+ assigns *(ws + (0 .. n - 1)), \result;
+ assigns *(ws + (0 .. n - 1)) \from (indirect: n), (indirect: *stream);
assigns \result \from ws, (indirect: n), (indirect: *stream);
*/
int *fgetws(int * __restrict ws, int n, FILE * __restrict stream);
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index 9c149b3e..f0fc168c 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -261,6 +261,23 @@ axiomatic StrChr {
}
*/
/*@
+axiomatic WMemChr {
+ logic 𔹠wmemchr{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
+ reads *(s + (0 .. n - 1));
+
+ axiom wmemchr_def{L}:
+ ∀ int *s;
+ ∀ int c;
+ ∀ ℤ n;
+ wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
+
+ }
+ */
+/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
diff --git a/tests/stl/oracle/stl_utility.err.oracle b/tests/stl/oracle/stl_utility.err.oracle
deleted file mode 100644
index e69de29b..00000000
diff --git a/tests/template/oracle/template_variadic.res.oracle b/tests/template/oracle/template_variadic.res.oracle
index 584f3fe5..344ad112 100644
--- a/tests/template/oracle/template_variadic.res.oracle
+++ b/tests/template/oracle/template_variadic.res.oracle
@@ -26,24 +26,24 @@ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> {
};
typedef struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> type;
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this);
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this);
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *__frama_c_arg_0);
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
+ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *__frama_c_arg_0);
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> *__frama_c_arg_0);
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
+ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> *__frama_c_arg_0);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid_read(this); */
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this)
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this)
{
return;
}
@@ -52,9 +52,9 @@ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this
requires \valid_read(this);
requires \valid_read(__frama_c_arg_0);
*/
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *__frama_c_arg_0)
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
+ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *__frama_c_arg_0)
{
return;
}
@@ -63,9 +63,9 @@ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *__fr
requires \valid_read(this);
requires \valid(__frama_c_arg_0);
*/
-void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor(
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
-struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> *__frama_c_arg_0)
+void Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>>::Ctor
+(struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> const *this,
+ struct Tuple<Pair<int,unsigned int>,Pair<signed char,unsigned char>> *__frama_c_arg_0)
{
return;
}
--
GitLab