From 99ff7a49e3c43c75d991e923f54e54f86d0d5781 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Sat, 27 Apr 2019 11:53:48 +0200
Subject: [PATCH] revert to use x!=0 for converting x to boolean
---
src/kernel_services/ast_queries/logic_typing.ml | 3 ++-
.../wp/tests/wp_acsl/oracle/precedence.res.oracle | 12 ++++++------
tests/misc/oracle/booleans.res.oracle | 4 ++--
tests/misc/oracle/obfuscate.res.oracle | 2 +-
tests/spec/oracle/all.res.oracle | 10 +++++-----
tests/spec/oracle/logic_type.res.oracle | 6 +++---
tests/spec/oracle/null_ptr.res.oracle | 2 +-
tests/spec/oracle/parsing.res.oracle | 4 ++--
tests/spec/oracle/real_typing_bts1309.res.oracle | 2 +-
9 files changed, 23 insertions(+), 22 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index b2c51f3b799..727d6639ffd 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1229,7 +1229,8 @@ struct
| t1, Ltype ({lt_name = name},[])
when name = Utf8_logic.boolean && is_integral_type t1 ->
let t2 = Ltype (C.find_logic_type Utf8_logic.boolean,[]) in
- { e with term_node = TLogic_coerce(t2,e); term_type = t2 }
+ let e = mk_cast e Linteger in
+ Logic_const.term ~loc (TBinOp(Ne,e,lzero ~loc())) t2
| t1, Linteger when Logic_const.is_boolean_type t1 && explicit ->
logic_coerce Linteger e
| t1, Ctype t2 when Logic_const.is_boolean_type t1
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle
index e6908ae1869..0071a69eb1e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle
@@ -778,19 +778,19 @@ void predicate(int x, int a, int b)
ensures
ko: r_precedence_and_eq:
\old(p) ≡ \old(q) ∧ \old(r) ≢ 0 ⇔
- (ð”¹)\old(p) ≡ ((ð”¹)\old(q) ∧ (ð”¹)\old(r));
+ (\old(p) ≢ 0) ≡ (\old(q) ≢ 0 ∧ \old(r) ≢ 0);
ensures
ko: l_precedence_and_eq:
\old(p) ≢ 0 ∧ \old(q) ≡ \old(r) ⇔
- ((ð”¹)\old(p) ∧ (ð”¹)\old(q)) ≡ (ð”¹)\old(r);
+ (\old(p) ≢ 0 ∧ \old(q) ≢ 0) ≡ (\old(r) ≢ 0);
ensures
ko: l_nonassoc_eq:
\old(p) ≡ \old(q) ≡ \old(r) ⇔
- (\old(p) ≡ \old(q)) ≡ (ð”¹)\old(r);
+ (\old(p) ≡ \old(q)) ≡ (\old(r) ≢ 0);
ensures
ko: r_nonassoc_eq:
\old(p) ≡ \old(q) ≡ \old(r) ⇔
- (ð”¹)\old(p) ≡ (\old(q) ≡ \old(r));
+ (\old(p) ≢ 0) ≡ (\old(q) ≡ \old(r));
ensures
r_precedence_neq_and:
\old(p) ≢ \old(q) ∧ R ⇔ \old(p) ≢ \old(q) ∧ R;
@@ -800,11 +800,11 @@ void predicate(int x, int a, int b)
ensures
ko: r_precedence_and_neq:
\old(p) ≢ \old(q) ∧ \old(r) ≢ 0 ⇔
- (ð”¹)\old(p) ≢ ((ð”¹)\old(q) ∧ (ð”¹)\old(r));
+ (\old(p) ≢ 0) ≢ (\old(q) ≢ 0 ∧ \old(r) ≢ 0);
ensures
ko: l_precedence_and_neq:
\old(p) ≢ 0 ∧ \old(q) ≢ \old(r) ⇔
- ((ð”¹)\old(p) ∧ (ð”¹)\old(q)) ≢ (ð”¹)\old(r);
+ (\old(p) ≢ 0 ∧ \old(q) ≢ 0) ≢ (\old(r) ≢ 0);
*/
void comparison(int p, int q, int r)
{
diff --git a/tests/misc/oracle/booleans.res.oracle b/tests/misc/oracle/booleans.res.oracle
index d54bc6a7cc3..8f7927c6bce 100644
--- a/tests/misc/oracle/booleans.res.oracle
+++ b/tests/misc/oracle/booleans.res.oracle
@@ -29,8 +29,8 @@ int main(void)
{
int __retres;
int x = 42;
- /*@ check (ð”¹)x ≡ (ð”¹)17; */ ;
- /*@ check (ℤ)(ð”¹)x ≡ 17; */ ;
+ /*@ check (x ≢ 0) ≡ (17 ≢ 0); */ ;
+ /*@ check ((ℤ)x ≢ 0) ≡ 17; */ ;
__retres = 0;
return __retres;
}
diff --git a/tests/misc/oracle/obfuscate.res.oracle b/tests/misc/oracle/obfuscate.res.oracle
index 3c55a38dad0..124447020ca 100644
--- a/tests/misc/oracle/obfuscate.res.oracle
+++ b/tests/misc/oracle/obfuscate.res.oracle
@@ -123,7 +123,7 @@ int F3(int f2)
V3 = 0;
if (f2) goto L2;
V3 ++;
- /*@ assert property: (ð”¹)V3? 1 ≢ 0: 0 ≢ 0; */ ;
+ /*@ assert property: V3 ≢ 0? 1 ≢ 0: 0 ≢ 0; */ ;
L2: ;
return V3;
}
diff --git a/tests/spec/oracle/all.res.oracle b/tests/spec/oracle/all.res.oracle
index 26a8ebc75b7..eb8254c5c9c 100644
--- a/tests/spec/oracle/all.res.oracle
+++ b/tests/spec/oracle/all.res.oracle
@@ -29,7 +29,7 @@ axiomatic Test {
axiom e: P ⊻ Q;
- axiom f: (ð”¹)0? P: Q;
+ axiom f: 0 ≢ 0? P: Q;
axiom g: (P ⇒ P) ∧ (¬P ⇒ Q);
@@ -39,13 +39,13 @@ axiomatic Test {
}
*/
-/*@ predicate R(ℤ i, ℤ j) = ((ð”¹)1? i + j: (j: j)) ≡ i + j;
+/*@ predicate R(ℤ i, ℤ j) = (1 ≢ 0? i + j: (j: j)) ≡ i + j;
*/
-/*@ predicate S(ℤ i, ℤ j) = ((ð”¹)1? (i: j): j) ≡ j;
+/*@ predicate S(ℤ i, ℤ j) = (1 ≢ 0? (i: j): j) ≡ j;
*/
-/*@ predicate T(ℤ i, ℤ j) = ((ð”¹)1? i: j) ≡ i;
+/*@ predicate T(ℤ i, ℤ j) = (1 ≢ 0? i: j) ≡ i;
*/
-/*@ lemma tauto: (ð”¹)0? T(0, 0): R(1, 2);
+/*@ lemma tauto: 0 ≢ 0? T(0, 0): R(1, 2);
*/
/*@ lemma tauto2: (R(0, 1) ⇒ S(3, 4)) ∧ (¬R(0, 1) ⇒ T(5, 6));
*/
diff --git a/tests/spec/oracle/logic_type.res.oracle b/tests/spec/oracle/logic_type.res.oracle
index c1cc68010da..c7f4d27c228 100644
--- a/tests/spec/oracle/logic_type.res.oracle
+++ b/tests/spec/oracle/logic_type.res.oracle
@@ -55,11 +55,11 @@ void h(void)
*/
/*@ logic _Bool _Bool_from_boolean(𔹠b) = (_Bool)b;
*/
-/*@ logic 𔹠boolean_from_integer(ℤ b) = (ð”¹)b;
+/*@ logic 𔹠boolean_from_integer(ℤ b) = b ≢ 0;
*/
-/*@ logic 𔹠boolean_from_int(int b) = (ð”¹)b;
+/*@ logic 𔹠boolean_from_int(int b) = b ≢ 0;
*/
-/*@ logic 𔹠boolean_from_Bool(_Bool b) = b;
+/*@ logic 𔹠boolean_from_Bool(_Bool b) = b ≢ 0;
*/
diff --git a/tests/spec/oracle/null_ptr.res.oracle b/tests/spec/oracle/null_ptr.res.oracle
index 55b0cc5e433..5412691e03a 100644
--- a/tests/spec/oracle/null_ptr.res.oracle
+++ b/tests/spec/oracle/null_ptr.res.oracle
@@ -22,7 +22,7 @@ void f(char *x)
return;
}
-/*@ ensures (ð”¹)\result ≡ \true; */
+/*@ ensures (\result ≢ 0) ≡ \true; */
int g(void)
{
int __retres;
diff --git a/tests/spec/oracle/parsing.res.oracle b/tests/spec/oracle/parsing.res.oracle
index 4cff9264d42..487e29fb134 100644
--- a/tests/spec/oracle/parsing.res.oracle
+++ b/tests/spec/oracle/parsing.res.oracle
@@ -7,9 +7,9 @@
/* Generated by Frama-C */
/*@ lemma bidon{Here}: ∀ int *t; ¬(*(t + 0) > 0);
*/
-/*@ lemma bidon1{Here}: ∀ int *t; !(ð”¹)*(t + 0) ≡ (ð”¹)0;
+/*@ lemma bidon1{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (0 ≢ 0);
*/
-/*@ lemma bidon2{Here}: ∀ int *t; !(ð”¹)*(t + 0) ≡ (ð”¹)0;
+/*@ lemma bidon2{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (0 ≢ 0);
*/
/*@
predicate foo{L}(int *a, int *b, int length) =
diff --git a/tests/spec/oracle/real_typing_bts1309.res.oracle b/tests/spec/oracle/real_typing_bts1309.res.oracle
index 1a15afbf483..263809eb183 100644
--- a/tests/spec/oracle/real_typing_bts1309.res.oracle
+++ b/tests/spec/oracle/real_typing_bts1309.res.oracle
@@ -3,7 +3,7 @@
void foo(int c)
{
float f = (float)1.0;
- /*@ assert 0.0 ≤ ((ð”¹)c? f: 2.0); */ ;
+ /*@ assert 0.0 ≤ (c ≢ 0? f: 2.0); */ ;
return;
}
--
GitLab