From 54185e9604642ec1a93f74b2165555afa67e7580 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 21 Feb 2024 14:07:39 +0100
Subject: [PATCH] [ACSL++] better char litteral translation
- no more casts inserted in front of the litteral
- use actual `'c'` value (or `L'c'` for wide char) instead of numerical one
---
convert_acsl.ml | 25 ++++++++++-
framaCIRGen_src/ACSLTermOrPredicate.cpp | 14 +-----
tests/basic/oracle/placement_new.res.oracle | 45 +++++++++----------
tests/basic/oracle/placement_newb.res.oracle | 45 +++++++++----------
tests/specs/oracle/basic.res.oracle | 2 +-
tests/specs/oracle/wchar_t.res.oracle | 3 +-
tests/stl/oracle/stl_algorithm.res.oracle | 45 +++++++++----------
tests/stl/oracle/stl_bool.res.oracle | 45 +++++++++----------
tests/stl/oracle/stl_functional.res.oracle | 45 +++++++++----------
tests/stl/oracle/stl_memory.res.oracle | 45 +++++++++----------
.../stl_shared_ptr_mistake10.res.oracle | 45 +++++++++----------
.../oracle/stl_shared_ptr_mistake5.res.oracle | 45 +++++++++----------
.../oracle/stl_shared_ptr_mistake6.res.oracle | 45 +++++++++----------
tests/stl/oracle/stl_system_error.res.oracle | 45 +++++++++----------
tests/stl/oracle/stl_typeinfo.res.oracle | 45 +++++++++----------
tests/stl/oracle/stl_unique_ptr.res.oracle | 45 +++++++++----------
16 files changed, 267 insertions(+), 317 deletions(-)
diff --git a/convert_acsl.ml b/convert_acsl.ml
index 8e0f9dcc..0e9ed0a6 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 74a4653c..0a39763b 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 19fb1e1c..eff921ab 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 e5a02cc7..73fc88a9 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 2de5b3b9..a92d6f6d 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 adecf2ef..942aac0e 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 158a5df0..1eeeb04c 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 64160356..6a1f7bc5 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 b4e115ee..b0b48095 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 ce15968f..eb4496e1 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 d8f78952..081aec94 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 014225c0..6da10dc3 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 1f306e33..76a56143 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 0cc69025..4638556b 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 e61c0e41..168665b7 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 51284e7d..8dd60c4b 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;
}
*/
--
GitLab