From fb6421ecb079b122f5daa3b21bb4d30fdf3561b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 3 Nov 2020 11:23:21 +0100
Subject: [PATCH] [e-acsl] In tests, uses the Eva parameter
-eva-unroll-recursive-calls.
Instead of the deprecated parameter -eva-ignore-recursive-calls.
---
.../e-acsl/tests/arith/functions_rec.c | 2 +-
src/plugins/e-acsl/tests/arith/longlong.i | 2 +-
.../arith/oracle_ci/functions_rec.res.oracle | 67 -------------------
.../tests/arith/oracle_ci/gen_functions_rec.c | 28 --------
.../tests/arith/oracle_ci/gen_longlong.c | 2 -
.../tests/arith/oracle_ci/longlong.res.oracle | 8 ---
src/plugins/e-acsl/tests/bts/bts1395.i | 2 +-
.../tests/bts/oracle_ci/bts1395.res.oracle | 14 ----
.../e-acsl/tests/bts/oracle_ci/gen_bts1395.c | 2 -
9 files changed, 3 insertions(+), 124 deletions(-)
diff --git a/src/plugins/e-acsl/tests/arith/functions_rec.c b/src/plugins/e-acsl/tests/arith/functions_rec.c
index 8feb6f4e59d..89eb4a6a15c 100644
--- a/src/plugins/e-acsl/tests/arith/functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/functions_rec.c
@@ -1,6 +1,6 @@
/* run.config_ci
COMMENT: recursive logic functions
- STDOPT: +"-eva-ignore-recursive-calls"
+ STDOPT: +"-eva-unroll-recursive-calls 100"
*/
/*@ logic integer f1(integer n) =
diff --git a/src/plugins/e-acsl/tests/arith/longlong.i b/src/plugins/e-acsl/tests/arith/longlong.i
index 9be4c44511b..9dc71da4e6d 100644
--- a/src/plugins/e-acsl/tests/arith/longlong.i
+++ b/src/plugins/e-acsl/tests/arith/longlong.i
@@ -1,6 +1,6 @@
/* run.config_ci
COMMENT: upgrading longlong to GMP
- STDOPT: +"-eva-ignore-recursive-calls"
+ STDOPT: +"-eva-unroll-recursive-calls 8"
*/
unsigned long long my_pow(unsigned int x, unsigned int n) {
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle
index 490eda1facc..a30ec62a8b4 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle
@@ -8,80 +8,13 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:23: Warning:
assertion got status unknown.
-[eva] tests/arith/functions_rec.c:7: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f1_2 (__gen_e_acsl_f1_2 <- __gen_e_acsl_f1_2 :: tests/arith/functions_rec.c:7 <-
- __gen_e_acsl_f1 :: tests/arith/functions_rec.c:24 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
[eva:alarm] tests/arith/functions_rec.c:24: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:24: Warning:
assertion got status unknown.
-[eva] tests/arith/functions_rec.c:10: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/arith/functions_rec.c:10 <-
- __gen_e_acsl_f2 :: tests/arith/functions_rec.c:26 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva] tests/arith/functions_rec.c:10: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/arith/functions_rec.c:10 <-
- __gen_e_acsl_f2 :: tests/arith/functions_rec.c:26 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva] tests/arith/functions_rec.c:10: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/arith/functions_rec.c:10 <-
- __gen_e_acsl_f2 :: tests/arith/functions_rec.c:26 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- division by zero. assert __gen_e_acsl_f2_8 ≢ 0;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow.
- assert -2147483648 ≤ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow. assert __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6 ≤ 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow.
- assert
- (int)(__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8 ≤
- 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- division by zero. assert __gen_e_acsl_f2_13 ≢ 0;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow.
- assert -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow.
- assert __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow.
- assert
- (int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13 ≤
- 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:26: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:26: Warning:
assertion got status unknown.
-[eva] tests/arith/functions_rec.c:14: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/arith/functions_rec.c:14 <-
- __gen_e_acsl_f3 :: tests/arith/functions_rec.c:28 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
[eva:alarm] tests/arith/functions_rec.c:28: Warning:
assertion got status unknown.
-[eva] tests/arith/functions_rec.c:17: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/arith/functions_rec.c:17 <-
- __gen_e_acsl_f4 :: tests/arith/functions_rec.c:30 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/arith/functions_rec.c:30: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:30: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
index fc96bb91d06..b766248de7c 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
@@ -183,20 +183,6 @@ int __gen_e_acsl_f2(int n)
__e_acsl_assert(__gen_e_acsl_f2_13 != 0,1,"RTE","f2",
"division_by_zero: __gen_e_acsl_f2_13 != 0",
"tests/arith/functions_rec.c",10);
- /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_13 ≢ 0; */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13
- ≤ 2147483647;
- */
__gen_e_acsl_if_4 = (__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13;
}
return __gen_e_acsl_if_4;
@@ -216,20 +202,6 @@ int __gen_e_acsl_f2_2(long n)
__e_acsl_assert(__gen_e_acsl_f2_8 != 0,1,"RTE","f2_2",
"division_by_zero: __gen_e_acsl_f2_8 != 0",
"tests/arith/functions_rec.c",10);
- /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_8 ≢ 0; */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6 ≤ 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8
- ≤ 2147483647;
- */
__gen_e_acsl_if_3 = (__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8;
}
return __gen_e_acsl_if_3;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
index 015b45a630e..21f7073ae45 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
@@ -12,8 +12,6 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
}
tmp_0 = my_pow(x,n / (unsigned int)2);
tmp = (int)tmp_0;
- /*@ assert Eva: signed_overflow: -2147483648 ≤ tmp * tmp; */
- /*@ assert Eva: signed_overflow: tmp * tmp ≤ 2147483647; */
tmp *= tmp;
if (n % (unsigned int)2 == (unsigned int)0) {
__retres = (unsigned long long)tmp;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle
index a8d7dc220ee..36e0f42013b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle
@@ -1,13 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva] tests/arith/longlong.i:9: Warning:
- recursive call during value analysis
- of my_pow (my_pow <- my_pow :: tests/arith/longlong.i:16 <- main). Assuming
- the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/arith/longlong.i:10: Warning:
- signed overflow. assert -2147483648 ≤ tmp * tmp;
-[eva:alarm] tests/arith/longlong.i:10: Warning:
- signed overflow. assert tmp * tmp ≤ 2147483647;
[eva:alarm] tests/arith/longlong.i:17: Warning:
function __gmpz_import: precondition got status unknown.
[eva:alarm] tests/arith/longlong.i:17: Warning:
diff --git a/src/plugins/e-acsl/tests/bts/bts1395.i b/src/plugins/e-acsl/tests/bts/bts1395.i
index ef01c83d78b..34b85b1ee8c 100644
--- a/src/plugins/e-acsl/tests/bts/bts1395.i
+++ b/src/plugins/e-acsl/tests/bts/bts1395.i
@@ -1,6 +1,6 @@
/* run.config_ci
COMMENT: recursive function
- STDOPT: +"-eva-ignore-recursive-calls"
+ STDOPT: +"-eva-unroll-recursive-calls 5"
*/
/*@ requires n > 0; */
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle
index 30c8d8ed4cd..efd02631129 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle
@@ -1,16 +1,2 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva] tests/bts/bts1395.i:9: Warning:
- recursive call during value analysis
- of __gen_e_acsl_fact (__gen_e_acsl_fact <- fact :: tests/bts/bts1395.i:7 <-
- __gen_e_acsl_fact :: tests/bts/bts1395.i:13 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/bts/bts1395.i:9: Warning:
- signed overflow. assert -2147483648 ≤ n * tmp;
- (tmp from fact(n - 1))
-[eva:alarm] tests/bts/bts1395.i:9: Warning:
- signed overflow. assert n * tmp ≤ 2147483647;
- (tmp from fact(n - 1))
-[eva:alarm] tests/bts/bts1395.i:14: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
index 1e95f4093d1..7ffe91bbde5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
@@ -16,8 +16,6 @@ int fact(int n)
}
tmp = __gen_e_acsl_fact(n - 1);
;
- /*@ assert Eva: signed_overflow: -2147483648 ≤ n * tmp; */
- /*@ assert Eva: signed_overflow: n * tmp ≤ 2147483647; */
__retres = n * tmp;
return_label: return __retres;
}
--
GitLab