diff --git a/src/plugins/e-acsl/tests/arith/functions_rec.c b/src/plugins/e-acsl/tests/arith/functions_rec.c
index 8feb6f4e59dde504eb7ad2e4374c94867e39802a..89eb4a6a15c7c0f242611ebc534fea5aafa09d90 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 9be4c44511b20d6b432aee24fd7b92f026d3cd9f..9dc71da4e6dc44fc36bb79c1ed0dd5390cbf0137 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 490eda1facc8ddd5e0b0ea133de1d4f871d3e14f..a30ec62a8b4a0a1fc14312fac9b2ef01ef5888c9 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 fc96bb91d0626f1828b71d3eb12c44e8ef57f99f..b766248de7c8fd4d07f231228583ebb240bd00a3 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 015b45a630e6b6006768996e99dccb81acf5910e..21f7073ae453abd87367cfa6774390b8b8e87753 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 a8d7dc220ee03e4929c36d12d7a5bd8e329e52dd..36e0f42013b7f8302a598494fa5d342a8b7a2b7e 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 ef01c83d78b3a55f12e943321f73fdc7567fe102..34b85b1ee8c73ac93cbf2eb25dde331690ad4ab0 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 30c8d8ed4cd52200784001e557b21efd970c070b..efd026311297e55d8fefb674326118e6ece88624 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 1e95f4093d1686374aeefee4b482a76c9516c257..7ffe91bbde5d7c8b8cc2d47711157452d4ab25d5 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;
}