From d0c15bc9a92c37ee8646a5dea58cd60ad9de4226 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 2 Apr 2020 15:59:10 +0200
Subject: [PATCH] [eacsl:test] Update test oracles
---
.../at_on-purely-logic-variables.res.oracle | 24 +++++++------
.../gen_at_on-purely-logic-variables.c | 36 ++++++++++++-------
.../tests/arith/oracle_ci/gen_rationals.c | 4 +--
.../oracle_ci/gen_functions_contiki.c | 2 +-
.../tests/memory/oracle_ci/gen_memsize.c | 18 +++++-----
5 files changed, 50 insertions(+), 34 deletions(-)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
index 0b02e09b98b..ceb8eed7a93 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
@@ -13,7 +13,7 @@
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
+ assert \initialized(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
@@ -24,7 +24,8 @@
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_3 +
- ((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_v - -5) - 1)));
+ (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +
+ (int)((int)(__gen_e_acsl_v - -5) - 1)));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:34: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:31: Warning:
@@ -33,7 +34,8 @@
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
+ assert
+ \initialized(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_3 - -9) - 1));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
@@ -44,17 +46,19 @@
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_6 +
- ((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_v_3 - -5) - 1)));
+ (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
+ (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:45: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:43: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
+ assert \initialized(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
+ assert
+ \initialized(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n - 1) - 1));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
@@ -63,7 +67,7 @@
function __gen_e_acsl_f: postcondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
+ assert \initialized(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
@@ -74,9 +78,9 @@
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_7 +
- ((__gen_e_acsl_u_5 - 10) * 300 +
- (((__gen_e_acsl_v_5 - -10) - 1) * 100 +
- ((__gen_e_acsl_w - 100) - 1))));
+ (int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +
+ (int)((int)((int)((int)(__gen_e_acsl_v_5 - -10) - 1) * 100)
+ + (int)((int)(__gen_e_acsl_w - 100) - 1))));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:54: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:63: Warning:
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
index 007bc6daa68..17dee710545 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
@@ -56,7 +56,7 @@ void g(void)
"tests/arith/at_on-purely-logic-variables.c",16);
/*@ assert
Eva: initialization:
- \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
+ \initialized(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3));
*/
if (! *(__gen_e_acsl_at + (__gen_e_acsl_w - 3))) ;
else {
@@ -240,7 +240,7 @@ int main(void)
"tests/arith/at_on-purely-logic-variables.c",29);
/*@ assert
Eva: initialization:
- \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
+ \initialized(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2));
*/
if (! *(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2))) ;
else {
@@ -289,8 +289,8 @@ int main(void)
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_3 +
- ((__gen_e_acsl_u - 9) * 11 +
- ((__gen_e_acsl_v - -5) - 1)));
+ (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +
+ (int)((int)(__gen_e_acsl_v - -5) - 1)));
*/
if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + ((
__gen_e_acsl_v - -5) - 1))))
@@ -374,7 +374,8 @@ int main(void)
"tests/arith/at_on-purely-logic-variables.c",41);
/*@ assert
Eva: initialization:
- \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
+ \initialized(__gen_e_acsl_at_5 +
+ (int)((int)(__gen_e_acsl_k_3 - -9) - 1));
*/
if (! (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)) == 0L))
;
@@ -427,8 +428,9 @@ int main(void)
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_6 +
- ((__gen_e_acsl_u_3 - 9) * 32 +
- ((__gen_e_acsl_v_3 - -5) - 1)));
+ (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32)
+ +
+ (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
*/
if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_3 - 9) * 32 + (
(__gen_e_acsl_v_3 - -5) - 1))))
@@ -514,9 +516,17 @@ int main(void)
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_7 +
- ((__gen_e_acsl_u_5 - 10) * 300 +
- (((__gen_e_acsl_v_5 - -10) - 1) * 100 +
- ((__gen_e_acsl_w - 100) - 1))));
+ (int)((int)((int)(__gen_e_acsl_u_5 - 10) *
+ 300)
+ +
+ (int)((int)((int)((int)(__gen_e_acsl_v_5
+ - -10)
+ - 1)
+ * 100)
+ +
+ (int)((int)(__gen_e_acsl_w -
+ 100)
+ - 1))));
*/
if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_5 - 10) * 300 + (
((__gen_e_acsl_v_5 - -10) - 1) * 100 + (
@@ -650,7 +660,8 @@ void __gen_e_acsl_f(int *t)
"tests/arith/at_on-purely-logic-variables.c",7);
/*@ assert
Eva: initialization:
- \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
+ \initialized(__gen_e_acsl_at +
+ (int)((int)(__gen_e_acsl_n - 1) - 1));
*/
if (*(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1))) {
int __gen_e_acsl_valid_read_2;
@@ -665,7 +676,8 @@ void __gen_e_acsl_f(int *t)
"tests/arith/at_on-purely-logic-variables.c",7);
/*@ assert
Eva: initialization:
- \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
+ \initialized(__gen_e_acsl_at_2 +
+ (int)((int)(__gen_e_acsl_n - 1) - 1));
*/
__gen_e_acsl_and = *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
}
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
index bd22a341b9b..7943b9907d6 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
@@ -57,9 +57,9 @@ int main(void)
__gmpq_clear(__gen_e_acsl__4);
}
/*@ assert 0.1 ≡ 0.1; */ ;
- __e_acsl_assert(1,"Assertion","main","(double)1.0 == 1.0",
+ __e_acsl_assert(1,"Assertion","main","1.0 == 1.0",
"tests/arith/rationals.c",14);
- /*@ assert (double)1.0 ≡ 1.0; */ ;
+ /*@ assert 1.0 ≡ 1.0; */ ;
{
__e_acsl_mpq_t __gen_e_acsl__5;
double __gen_e_acsl__6;
diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
index 259afb2e7cf..47e55d3fc12 100644
--- a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
+++ b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
@@ -8,7 +8,7 @@ struct list {
/*@
logic ℤ length_aux{L}(struct list *l, ℤ n) =
\at(n < 0? -1:
- (l ≡ (struct list *)((void *)0)? n:
+ (l ≡ (struct list *)0? n:
(n < 2147483647? length_aux(l->next, n + 1): -1)),
L);
*/
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
index a7e98e9b929..60fc5642381 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
@@ -57,25 +57,25 @@ int main(int argc, char **argv)
"__e_acsl_heap_allocation_size == 16",
"tests/memory/memsize.c",50);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
- __e_acsl_assert(b == (char *)0,"Assertion","main",
- "b == (char *)((void *)0)","tests/memory/memsize.c",51);
- /*@ assert b ≡ (char *)((void *)0); */ ;
+ __e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
+ "tests/memory/memsize.c",51);
+ /*@ assert b ≡ (char *)0; */ ;
b = (char *)calloc(18446744073709551615UL,18446744073709551615UL);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
"tests/memory/memsize.c",55);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
- __e_acsl_assert(b == (char *)0,"Assertion","main",
- "b == (char *)((void *)0)","tests/memory/memsize.c",56);
- /*@ assert b ≡ (char *)((void *)0); */ ;
+ __e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
+ "tests/memory/memsize.c",56);
+ /*@ assert b ≡ (char *)0; */ ;
b = (char *)malloc(18446744073709551615UL);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
"tests/memory/memsize.c",60);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
- __e_acsl_assert(b == (char *)0,"Assertion","main",
- "b == (char *)((void *)0)","tests/memory/memsize.c",61);
- /*@ assert b ≡ (char *)((void *)0); */ ;
+ __e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
+ "tests/memory/memsize.c",61);
+ /*@ assert b ≡ (char *)0; */ ;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
--
GitLab