From 28e28ec38000762d064edfb6038be156c06bf81a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 22 Feb 2024 15:57:49 +0100
Subject: [PATCH] [clang2ir] fix implicit conversion of boolean term to
predicate
---
framaCIRGen_src/ACSLTermOrPredicate.cpp | 10 +++++--
tests/basic/oracle/placement_new.res.oracle | 10 +++----
tests/basic/oracle/placement_newb.res.oracle | 10 +++----
tests/specs/oracle/logic_defs.res.oracle | 4 +--
tests/stl/oracle/stl_algorithm.res.oracle | 28 +++++++++----------
tests/stl/oracle/stl_bool.res.oracle | 28 +++++++++----------
tests/stl/oracle/stl_functional.res.oracle | 28 +++++++++----------
tests/stl/oracle/stl_memory.res.oracle | 28 +++++++++----------
.../stl_shared_ptr_mistake10.res.oracle | 28 +++++++++----------
.../oracle/stl_shared_ptr_mistake5.res.oracle | 28 +++++++++----------
.../oracle/stl_shared_ptr_mistake6.res.oracle | 28 +++++++++----------
tests/stl/oracle/stl_system_error.res.oracle | 28 +++++++++----------
tests/stl/oracle/stl_typeinfo.res.oracle | 28 +++++++++----------
tests/stl/oracle/stl_unique_ptr.res.oracle | 28 +++++++++----------
14 files changed, 159 insertions(+), 155 deletions(-)
diff --git a/framaCIRGen_src/ACSLTermOrPredicate.cpp b/framaCIRGen_src/ACSLTermOrPredicate.cpp
index 0a39763b..2c88ed0d 100644
--- a/framaCIRGen_src/ACSLTermOrPredicate.cpp
+++ b/framaCIRGen_src/ACSLTermOrPredicate.cpp
@@ -26,6 +26,7 @@
//
#include "ACSLTermOrPredicate.h"
+#include "Clang_utils.h"
#include "clang/AST/DeclTemplate.h"
namespace Acsl {
@@ -3769,20 +3770,25 @@ TermOrPredicate::apply(Operator& operation, logic_type& ltypeResult,
ltypeResult = logic_type_dup((logic_type)
f->returned_type->content.container);
if (isPlainBooleanType(ltypeResult, context)) {
+ predicate relation;
location zeroLoc = copy_loc(expressionResult->loc);
zeroLoc->linenum1 = zeroLoc->linenum2;
zeroLoc->charnum1 = zeroLoc->charnum2;
+ if (context.is_builtin_boolean(ltypeResult)) {
+ relation =
+ predicate_Prel(REQ,term_dup(expressionResult),term_true(zeroLoc));
+ } else {
term zero = tzero(zeroLoc);
- predicate relation;
if (ltypeResult->tag_logic_type == LINTEGER)
relation = predicate_Prel(RNEQ, term_dup(expressionResult), zero);
else
relation = predicate_Prel(RNEQ, term_cons(term_node_TLogic_coerce(
logic_type_Linteger(), term_dup(expressionResult)),
copy_loc(expressionResult->loc), NULL), zero);
+ }
predicateResult = predicate_named_cons(NULL,
copy_loc(expressionResult->loc), relation);
- };
+ }
}
else {
predicateResult =
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index eff921ab..9db3964d 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -134,7 +134,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -148,7 +148,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -264,7 +264,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -281,7 +281,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -370,7 +370,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index 73fc88a9..239ec155 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -103,7 +103,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -117,7 +117,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -233,7 +233,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -250,7 +250,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -339,7 +339,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
diff --git a/tests/specs/oracle/logic_defs.res.oracle b/tests/specs/oracle/logic_defs.res.oracle
index 609fc25c..03bdce44 100644
--- a/tests/specs/oracle/logic_defs.res.oracle
+++ b/tests/specs/oracle/logic_defs.res.oracle
@@ -54,9 +54,7 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
/*@ logic 𔹠test5(int a, struct A b) = a ≡ b.x;
*/
/*@
-lemma foo:
- ∀ int a;
- ∀ struct A b; test(a, b) ⇔ test5(a, b) ≢ (0 ≢ 0);
+lemma foo: ∀ int a; ∀ struct A b; test(a, b) ⇔ test5(a, b) ≡ \true;
*/
int main(void)
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index 1eeeb04c..dfee6bd7 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -541,7 +541,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -555,7 +555,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -671,7 +671,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -688,7 +688,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -777,7 +777,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
@@ -883,7 +883,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
- assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
@@ -894,7 +894,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
- assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
@@ -949,7 +949,7 @@ void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
@@ -1005,7 +1005,7 @@ int strcoll(char const *s1, char const *s2);
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
@@ -1016,7 +1016,7 @@ int strcoll(char const *s1, char const *s2);
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -1040,13 +1040,13 @@ char *strchrnul(char const *s, int c);
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -1140,7 +1140,7 @@ char *__fc_strtok_ptr;
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
@@ -1202,7 +1202,7 @@ char *strtok(char * restrict s, char const * restrict delim);
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
diff --git a/tests/stl/oracle/stl_bool.res.oracle b/tests/stl/oracle/stl_bool.res.oracle
index 6a1f7bc5..3fe6d50b 100644
--- a/tests/stl/oracle/stl_bool.res.oracle
+++ b/tests/stl/oracle/stl_bool.res.oracle
@@ -189,7 +189,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -203,7 +203,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -319,7 +319,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -336,7 +336,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -425,7 +425,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
@@ -531,7 +531,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
- assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
@@ -542,7 +542,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
- assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
@@ -597,7 +597,7 @@ void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
@@ -653,7 +653,7 @@ int strcoll(char const *s1, char const *s2);
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
@@ -664,7 +664,7 @@ int strcoll(char const *s1, char const *s2);
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -688,13 +688,13 @@ char *strchrnul(char const *s, int c);
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -788,7 +788,7 @@ char *__fc_strtok_ptr;
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
@@ -850,7 +850,7 @@ char *strtok(char * restrict s, char const * restrict delim);
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index b0b48095..99400493 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -349,7 +349,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -363,7 +363,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -479,7 +479,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -496,7 +496,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -585,7 +585,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
@@ -691,7 +691,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
- assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
@@ -702,7 +702,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
- assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
@@ -757,7 +757,7 @@ void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
@@ -813,7 +813,7 @@ int strcoll(char const *s1, char const *s2);
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
@@ -824,7 +824,7 @@ int strcoll(char const *s1, char const *s2);
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -848,13 +848,13 @@ char *strchrnul(char const *s, int c);
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -948,7 +948,7 @@ char *__fc_strtok_ptr;
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
@@ -1010,7 +1010,7 @@ char *strtok(char * restrict s, char const * restrict delim);
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index eb4496e1..78a7cb72 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -355,7 +355,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -369,7 +369,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -485,7 +485,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -502,7 +502,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -591,7 +591,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
@@ -697,7 +697,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
- assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
@@ -708,7 +708,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
- assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
@@ -763,7 +763,7 @@ void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
@@ -819,7 +819,7 @@ int strcoll(char const *s1, char const *s2);
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
@@ -830,7 +830,7 @@ int strcoll(char const *s1, char const *s2);
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -854,13 +854,13 @@ char *strchrnul(char const *s, int c);
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -954,7 +954,7 @@ char *__fc_strtok_ptr;
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
@@ -1016,7 +1016,7 @@ char *strtok(char * restrict s, char const * restrict delim);
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index 081aec94..289ad1a7 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -323,7 +323,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -337,7 +337,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -453,7 +453,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -470,7 +470,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -559,7 +559,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
@@ -712,7 +712,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
- assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
@@ -723,7 +723,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
- assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
@@ -778,7 +778,7 @@ void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
@@ -834,7 +834,7 @@ int strcoll(char const *s1, char const *s2);
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
@@ -845,7 +845,7 @@ int strcoll(char const *s1, char const *s2);
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -869,13 +869,13 @@ char *strchrnul(char const *s, int c);
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -969,7 +969,7 @@ char *__fc_strtok_ptr;
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
@@ -1031,7 +1031,7 @@ char *strtok(char * restrict s, char const * restrict delim);
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 6da10dc3..834540a7 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -304,7 +304,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -318,7 +318,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -434,7 +434,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -451,7 +451,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -540,7 +540,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
@@ -693,7 +693,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
- assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
@@ -704,7 +704,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
- assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
@@ -759,7 +759,7 @@ void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
@@ -815,7 +815,7 @@ int strcoll(char const *s1, char const *s2);
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
@@ -826,7 +826,7 @@ int strcoll(char const *s1, char const *s2);
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -850,13 +850,13 @@ char *strchrnul(char const *s, int c);
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -950,7 +950,7 @@ char *__fc_strtok_ptr;
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
@@ -1012,7 +1012,7 @@ char *strtok(char * restrict s, char const * restrict delim);
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 76a56143..a0741928 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -305,7 +305,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -319,7 +319,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -435,7 +435,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -452,7 +452,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -541,7 +541,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
@@ -694,7 +694,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
- assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
@@ -705,7 +705,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
- assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
@@ -760,7 +760,7 @@ void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
@@ -816,7 +816,7 @@ int strcoll(char const *s1, char const *s2);
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
@@ -827,7 +827,7 @@ int strcoll(char const *s1, char const *s2);
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -851,13 +851,13 @@ char *strchrnul(char const *s, int c);
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -951,7 +951,7 @@ char *__fc_strtok_ptr;
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
@@ -1013,7 +1013,7 @@ char *strtok(char * restrict s, char const * restrict delim);
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index 4638556b..7cb1e09c 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -267,7 +267,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -281,7 +281,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -397,7 +397,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -414,7 +414,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -503,7 +503,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
@@ -608,7 +608,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
- assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
@@ -619,7 +619,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
- assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
@@ -674,7 +674,7 @@ void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
@@ -730,7 +730,7 @@ int strcoll(char const *s1, char const *s2);
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
@@ -741,7 +741,7 @@ int strcoll(char const *s1, char const *s2);
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -765,13 +765,13 @@ char *strchrnul(char const *s, int c);
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -865,7 +865,7 @@ char *__fc_strtok_ptr;
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
@@ -927,7 +927,7 @@ char *strtok(char * restrict s, char const * restrict delim);
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index 168665b7..9323b3fe 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -125,7 +125,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -139,7 +139,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -255,7 +255,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -272,7 +272,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -361,7 +361,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
@@ -466,7 +466,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
- assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
@@ -477,7 +477,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
- assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
@@ -532,7 +532,7 @@ void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
@@ -588,7 +588,7 @@ int strcoll(char const *s1, char const *s2);
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
@@ -599,7 +599,7 @@ int strcoll(char const *s1, char const *s2);
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -623,13 +623,13 @@ char *strchrnul(char const *s, int c);
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -723,7 +723,7 @@ char *__fc_strtok_ptr;
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
@@ -785,7 +785,7 @@ char *strtok(char * restrict s, char const * restrict delim);
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
diff --git a/tests/stl/oracle/stl_unique_ptr.res.oracle b/tests/stl/oracle/stl_unique_ptr.res.oracle
index 8dd60c4b..991d273f 100644
--- a/tests/stl/oracle/stl_unique_ptr.res.oracle
+++ b/tests/stl/oracle/stl_unique_ptr.res.oracle
@@ -848,7 +848,7 @@ axiomatic MemChr {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ memchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -862,7 +862,7 @@ axiomatic MemSet {
∀ char *s;
∀ ℤ c;
∀ ℤ n;
- memset(s, c, n) ≢ (0 ≢ 0) ⇔
+ memset(s, c, n) ≡ \true ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
@@ -978,7 +978,7 @@ axiomatic StrChr {
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
- strchr(s, c) ≢ (0 ≢ 0) ⇔
+ strchr(s, c) ≡ \true ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
@@ -995,7 +995,7 @@ axiomatic WMemChr {
∀ wchar_t *s;
∀ long c;
∀ ℤ n;
- wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
+ wmemchr(s, c, n) ≡ \true ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
@@ -1084,7 +1084,7 @@ axiomatic WcsChr {
axiom wcschr_def{L}:
∀ wchar_t *wcs;
∀ ℤ wc;
- wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+ wcschr(wcs, wc) ≡ \true ⇔
(∃ ℤ i;
0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)((int)wc));
@@ -1190,7 +1190,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
behavior found:
- assumes char_found: memchr((char *)s, c, n) ≢ (0 ≢ 0);
+ assumes char_found: memchr((char *)s, c, n) ≡ \true;
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_char: (int)*((char *)\result) ≡ \old(c);
ensures
@@ -1201,7 +1201,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
(unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
behavior not_found:
- assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true);
ensures result_null: \result ≡ \null;
*/
void *memchr(void const *s, int c, size_t n);
@@ -1256,7 +1256,7 @@ void *memmove(void *dest, void const *src, size_t n);
/*@ requires valid_s: valid_or_empty(s, n);
ensures
- acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≢ (0 ≢ 0);
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
ensures result_ptr: \result ≡ \old(s);
assigns *((char *)s + (0 .. n - 1)), \result;
assigns *((char *)s + (0 .. n - 1)) \from c;
@@ -1312,7 +1312,7 @@ int strcoll(char const *s1, char const *s2);
\from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: *\result ≡ (char)\old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures
@@ -1323,7 +1323,7 @@ int strcoll(char const *s1, char const *s2);
∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -1347,13 +1347,13 @@ char *strchrnul(char const *s, int c);
assigns \result \from s, *(s + (0 ..)), c;
behavior found:
- assumes char_found: strchr(s, c) ≢ (0 ≢ 0);
+ assumes char_found: strchr(s, c) ≡ \true;
ensures result_char: (int)*\result ≡ \old(c);
ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s));
ensures result_valid_string: valid_read_string(\result);
behavior not_found:
- assumes char_not_found: strchr(s, c) ≡ (0 ≢ 0);
+ assumes char_not_found: ¬(strchr(s, c) ≡ \true);
ensures result_null: \result ≡ \null;
behavior default:
@@ -1447,7 +1447,7 @@ char *__fc_strtok_ptr;
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
@@ -1509,7 +1509,7 @@ char *strtok(char * restrict s, char const * restrict delim);
(valid_read_string(s) ∧
(∀ int i;
0 ≤ i < strlen(delim) ⇒
- strchr(s, *(delim + i)) ≡ (0 ≢ 0)));
+ ¬(strchr(s, *(delim + i)) ≡ \true)));
ensures
result_subset:
\result ≡ \null ∨ \subset(\result, \old(s) + (0 ..));
--
GitLab