From 5228b7c205136720b4861efbf2323422ad77ddc0 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 24 Apr 2019 16:33:33 +0200
Subject: [PATCH] [tests] partial update
---
tests/libc/oracle/fc_libc.1.res.oracle | 4 ++--
tests/misc/oracle/obfuscate.res.oracle | 2 +-
tests/spec/oracle/all.res.oracle | 10 ++++-----
tests/spec/oracle/null_ptr.res.oracle | 2 +-
tests/spec/oracle/parsing.res.oracle | 4 ++--
.../oracle/real_typing_bts1309.res.oracle | 2 +-
.../syntax/oracle/static_formals_1.res.oracle | 22 +++++++++----------
7 files changed, 23 insertions(+), 23 deletions(-)
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 0e7823ec685..4202b6e1aa9 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4783,7 +4783,7 @@ int unsetenv(char const *name)
requires
alignment_is_a_suitable_power_of_two:
alignment ≥ sizeof(void *) ∧
- ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
assigns __fc_heap_status, \result;
assigns __fc_heap_status
\from (indirect: alignment), size, __fc_heap_status;
@@ -4820,7 +4820,7 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
assert
alignment_is_a_suitable_power_of_two:
alignment ≥ sizeof(void *) ∧
- ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
*/
;
*memptr = malloc(size);
diff --git a/tests/misc/oracle/obfuscate.res.oracle b/tests/misc/oracle/obfuscate.res.oracle
index 124447020ca..c56321364a9 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 ≢ 0? 1 ≢ 0: 0 ≢ 0; */ ;
+ /*@ assert property: V3? 1 ≢ 0: 0 ≢ 0; */ ;
L2: ;
return V3;
}
diff --git a/tests/spec/oracle/all.res.oracle b/tests/spec/oracle/all.res.oracle
index eb8254c5c9c..8543e35a53d 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 ≢ 0? P: Q;
+ axiom f: 0? P: Q;
axiom g: (P ⇒ P) ∧ (¬P ⇒ Q);
@@ -39,13 +39,13 @@ axiomatic Test {
}
*/
-/*@ predicate R(ℤ i, ℤ j) = (1 ≢ 0? i + j: (j: j)) ≡ i + j;
+/*@ predicate R(ℤ i, ℤ j) = (1? i + j: (j: j)) ≡ i + j;
*/
-/*@ predicate S(ℤ i, ℤ j) = (1 ≢ 0? (i: j): j) ≡ j;
+/*@ predicate S(ℤ i, ℤ j) = (1? (i: j): j) ≡ j;
*/
-/*@ predicate T(ℤ i, ℤ j) = (1 ≢ 0? i: j) ≡ i;
+/*@ predicate T(ℤ i, ℤ j) = (1? i: j) ≡ i;
*/
-/*@ lemma tauto: 0 ≢ 0? T(0, 0): R(1, 2);
+/*@ lemma tauto: 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/null_ptr.res.oracle b/tests/spec/oracle/null_ptr.res.oracle
index 5412691e03a..59e76f0ef7d 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 ≢ 0) ≡ \true; */
+/*@ ensures \result ≡ \true; */
int g(void)
{
int __retres;
diff --git a/tests/spec/oracle/parsing.res.oracle b/tests/spec/oracle/parsing.res.oracle
index 487e29fb134..37ceb452828 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) ≡ (0 ≢ 0);
+/*@ lemma bidon1{Here}: ∀ int *t; !*(t + 0) ≡ 0;
*/
-/*@ lemma bidon2{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (0 ≢ 0);
+/*@ lemma bidon2{Here}: ∀ int *t; !*(t + 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 263809eb183..47e5a9adb68 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 ≢ 0? f: 2.0); */ ;
+ /*@ assert 0.0 ≤ (c? f: 2.0); */ ;
return;
}
diff --git a/tests/syntax/oracle/static_formals_1.res.oracle b/tests/syntax/oracle/static_formals_1.res.oracle
index a699b713faa..33d75e1e69f 100644
--- a/tests/syntax/oracle/static_formals_1.res.oracle
+++ b/tests/syntax/oracle/static_formals_1.res.oracle
@@ -2,23 +2,23 @@
[kernel] Parsing tests/syntax/static_formals_2.c (with preprocessing)
/* Generated by Frama-C */
/*@ requires /* vid:23, lvid:23 */x < 10; */
-static int /* vid:52 */f(int /* vid:23, lvid:23 */x);
+static int /* vid:54 */f(int /* vid:23, lvid:23 */x);
-int /* vid:26 */g(void)
+int /* vid:28 */g(void)
{
- int /* vid:27 */tmp;
- /* vid:27 */tmp = /* vid:52 */f(4);
- return /* vid:27 */tmp;
+ int /* vid:29 */tmp;
+ /* vid:29 */tmp = /* vid:54 */f(4);
+ return /* vid:29 */tmp;
}
-/*@ requires /* vid:47, lvid:47 */x < 10; */
-static int /* vid:53 */f_0(int /* vid:47, lvid:47 */x);
+/*@ requires /* vid:49, lvid:49 */x < 10; */
+static int /* vid:55 */f_0(int /* vid:49, lvid:49 */x);
-int /* vid:50 */h(void)
+int /* vid:52 */h(void)
{
- int /* vid:51 */tmp;
- /* vid:51 */tmp = /* vid:53 */f_0(6);
- return /* vid:51 */tmp;
+ int /* vid:53 */tmp;
+ /* vid:53 */tmp = /* vid:55 */f_0(6);
+ return /* vid:53 */tmp;
}
--
GitLab