diff --git a/convert_acsl.ml b/convert_acsl.ml
index 8e0f9dccc23bcd0249e4a623fd22d0104e6140cc..0e9ed0a6c868f291c185b54b1f24fc6af0f068bb 100644
--- a/convert_acsl.ml
+++ b/convert_acsl.ml
@@ -66,13 +66,34 @@ let convert_fkind = function
| FDouble -> Cil_types.FDouble
| FLongDouble -> Cil_types.FLongDouble
+let int_to_char c =
+ let open Int64 in
+ let char_max = of_int 256 in
+ let mk_char c =
+ Char.unsafe_chr (Option.get (unsigned_to_int (unsigned_rem c char_max)))
+ in
+ let rec aux seq c =
+ let seq = Seq.cons (mk_char c) seq in
+ let c = unsigned_div c char_max in
+ if equal c zero then String.of_seq seq else aux seq c
+ in
+ (* NB: intermediate_format uses int there, but, at least for wide chars, it's
+ better to stick with int64, that allows for unsigned operations. The whole
+ thing would probably need a complete overhaul, though.
+ *)
+ aux Seq.empty (Int64.of_int c)
+
+let convert_char c = "'" ^ int_to_char c ^ "'"
+
+let convert_wchar c = "L'" ^ int_to_char c ^ "'"
+
let convert_logic_constant = function
| LCInt v -> IntConstant v
| LStr s -> StringConstant s
| LWStr _s ->
Frama_Clang_option.not_yet_implemented "Wide string support in logic"
- | LChr c -> IntConstant (string_of_int c)
- | LWChr c -> IntConstant (string_of_int c)
+ | LChr c -> IntConstant (convert_char c)
+ | LWChr c -> IntConstant (convert_wchar c)
| LCReal s -> FloatConstant s
| LCEnum (v,_) -> IntConstant (Int64.to_string v)
(* TODO: add support into ACSL for that? *)
diff --git a/framaCIRGen_src/ACSLTermOrPredicate.cpp b/framaCIRGen_src/ACSLTermOrPredicate.cpp
index 74a4653cdec6c571d7866321c0dd47523add4870..0a39763b22fc689c0530a1587d67508a697fa533 100644
--- a/framaCIRGen_src/ACSLTermOrPredicate.cpp
+++ b/framaCIRGen_src/ACSLTermOrPredicate.cpp
@@ -6323,21 +6323,11 @@ TermOrPredicate::readToken(Parser::State& state, Parser::Arguments& arguments) {
if (token.isChar()) {
constant = logic_constant_LChr(token.getChar());
valueType = logic_type_Lint(ICHAR);
- node =
- term_node_TCastE(
- logic_type_dup(valueType),
- term_cons(
- term_node_TConst(constant),
- arguments.newTokenLocation(), NULL));
+ node = term_node_TConst(constant);
} else { //wide char
constant = logic_constant_LWChr(token.getWideChar());
valueType = logic_type_Lint(IWCHAR);
- node =
- term_node_TCastE(
- logic_type_dup(valueType),
- term_cons(
- term_node_TConst(constant),
- arguments.newTokenLocation(),NULL));
+ node = term_node_TConst(constant);
}
break;
}
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index 19fb1e1cbe1998b55f08f890b09b414245f70890..eff921abff11f9d62192decda394797983dafdac 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -161,33 +161,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -195,14 +195,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -295,33 +294,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -329,14 +325,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index e5a02cc7a2908bfd6771dba682ccb08c547c2569..73fc88a93955f16cc45253cb7734bf953875bcb1 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -130,33 +130,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -164,14 +164,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -264,33 +263,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -298,14 +294,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/specs/oracle/basic.res.oracle b/tests/specs/oracle/basic.res.oracle
index 2de5b3b93c9d5a72f7c1c8ecd4b9869ffdb189a1..a92d6f6db2c1fd896d5fac8202416c04b7e57dad 100644
--- a/tests/specs/oracle/basic.res.oracle
+++ b/tests/specs/oracle/basic.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing basic.cpp (external front-end)
Now output intermediate result
/* Generated by Frama-C */
-/*@ lemma test_char: (char)0 ≢ (char)97;
+/*@ lemma test_char: '\000' ≢ 'a';
*/
diff --git a/tests/specs/oracle/wchar_t.res.oracle b/tests/specs/oracle/wchar_t.res.oracle
index adecf2ef1d13c9e6a4e6a89bad75e9724ddce9d6..942aac0eb71929122f14a660400add29964fdf94 100644
--- a/tests/specs/oracle/wchar_t.res.oracle
+++ b/tests/specs/oracle/wchar_t.res.oracle
@@ -4,8 +4,7 @@ Now output intermediate result
typedef long wchar_t;
/*@ predicate is_normal_char(wchar_t c) = 0 ≤ c ≤ 255;
*/
-/*@
-predicate wchar_buff{L}(wchar_t *p, ℤ l) = \at(*(p + l) ≡ (wchar_t)0,L);
+/*@ predicate wchar_buff{L}(wchar_t *p, ℤ l) = \at(*(p + l) ≡ 0,L);
*/
int freq[256];
/*@ requires is_normal_char(c); */
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index 158a5df03761a6ff0b7954894a01b69076d5f119..1eeeb04cedc37f13b53a5b184804db8707cda528 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -568,33 +568,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -602,14 +602,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -702,33 +701,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -736,14 +732,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/stl/oracle/stl_bool.res.oracle b/tests/stl/oracle/stl_bool.res.oracle
index 64160356e0812d94b5e81bacf6e238028255655d..6a1f7bc52060dcd5b6606f095431ecd1dac8d2f9 100644
--- a/tests/stl/oracle/stl_bool.res.oracle
+++ b/tests/stl/oracle/stl_bool.res.oracle
@@ -216,33 +216,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -250,14 +250,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -350,33 +349,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -384,14 +380,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index b4e115ee3fe5c3a9089c493a64fd112ee27c4314..b0b48095a6bb25b71a3a75544c3991059ce47729 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -376,33 +376,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -410,14 +410,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -510,33 +509,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -544,14 +540,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index ce15968f67d2aae01758ccfa8669393a2e63a55a..eb4496e12916e2ac5d07e1ea48a37fc9a67a40fa 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -382,33 +382,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -416,14 +416,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -516,33 +515,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -550,14 +546,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index d8f78952a309b6652709d2a13bb0a7476a70f0a2..081aec941dbb3f3c8f93d4f509d9e9ae6b7ae533 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -350,33 +350,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -384,14 +384,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -484,33 +483,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -518,14 +514,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 014225c031ca311a59e353244ead192a7c143f53..6da10dc3d2387ca867f0f14173b8da0d913d319e 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -331,33 +331,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -365,14 +365,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -465,33 +464,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -499,14 +495,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 1f306e3324fc334c905324e1371b9cce0e110314..76a56143a2298c620ee1999032857191fd0c0a4d 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -332,33 +332,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -366,14 +366,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -466,33 +465,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -500,14 +496,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index 0cc69025abd99f5982d62e82d18cb47af089b151..4638556b5c23b35f2c67494e9923b5d0bc9f0128 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -294,33 +294,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -328,14 +328,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -428,33 +427,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -462,14 +458,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index e61c0e41eb1039a215debe66e27075a51d81b161..168665b70a7c96535b0cc3b11aca75d8c5cbb178 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -152,33 +152,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -186,14 +186,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -286,33 +285,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -320,14 +316,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
diff --git a/tests/stl/oracle/stl_unique_ptr.res.oracle b/tests/stl/oracle/stl_unique_ptr.res.oracle
index 51284e7d35e254fa9ef3c3d5af18d304f0d3ef1a..8dd60c4bcd2bcdd470f1b0c0952c082798a288c4 100644
--- a/tests/stl/oracle/stl_unique_ptr.res.oracle
+++ b/tests/stl/oracle/stl_unique_ptr.res.oracle
@@ -875,33 +875,33 @@ axiomatic StrLen {
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
- *(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
+ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
+ ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
axiom strlen_at_null{L}:
- ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
+ ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
- 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
+ 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
@@ -909,14 +909,13 @@ axiomatic StrLen {
axiom strlen_create{L}:
∀ char *s;
- ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
+ ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
- 0 ≤ strlen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
@@ -1009,33 +1008,30 @@ axiomatic WcsLen {
axiom wcslen_pos_or_null{L}:
∀ wchar_t *s;
∀ ℤ i;
- 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (wchar_t)0) ∧
- *(s + i) ≡ (wchar_t)0 ⇒ wcslen(s) ≡ i;
+ 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
+ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
- ∀ wchar_t *s;
- (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (wchar_t)0) ⇒ wcslen(s) < 0;
+ ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (wchar_t)0;
+ ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
axiom wcslen_at_null{L}:
- ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (wchar_t)0;
+ ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
axiom wcslen_not_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (wchar_t)0 ⇒ i < wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ wchar_t *s;
- ∀ int i;
- 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (wchar_t)0 ⇒ i ≡ wcslen(s);
+ ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ wchar_t *s;
@@ -1043,14 +1039,13 @@ axiomatic WcsLen {
axiom wcslen_create{L}:
∀ wchar_t *s;
- ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒ 0 ≤ wcslen(s) ≤ i;
+ ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ wchar_t *s;
∀ int i;
∀ int k;
- 0 ≤ k ≤ i ∧ *(s + i) ≡ (wchar_t)0 ⇒
- 0 ≤ wcslen(s + k) ≤ i - k;
+ 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/