From ba8a379e97d2c9497b9e68e06c773b0b678201d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Mon, 12 Apr 2021 14:41:02 +0200 Subject: [PATCH] [e-acsl] In test decrease.i, uses Eva parameter -eva-unroll-recursive-calls. Instead of the deprecated parameter -eva-ignore-recursive-calls. --- .../e-acsl/tests/constructs/decrease.i | 2 +- .../constructs/oracle_ci/decrease.res.oracle | 62 ------------------- .../tests/constructs/oracle_ci/gen_decrease.c | 2 - 3 files changed, 1 insertion(+), 65 deletions(-) diff --git a/src/plugins/e-acsl/tests/constructs/decrease.i b/src/plugins/e-acsl/tests/constructs/decrease.i index b5dc3a50ca7..569bcb71d0f 100644 --- a/src/plugins/e-acsl/tests/constructs/decrease.i +++ b/src/plugins/e-acsl/tests/constructs/decrease.i @@ -1,5 +1,5 @@ /* run.config_ci, run.config_dev - STDOPT: +"-eva-ignore-recursive-calls -eva-slevel 7" + STDOPT: +"-eva-unroll-recursive-calls 10 -eva-slevel 7" */ // Test that the last iteration of the variant can be negative diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle index 74f4f634239..2a909408ab2 100644 --- a/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle +++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle @@ -9,65 +9,3 @@ E-ACSL construct `decreases clause' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". -[eva] tests/constructs/decrease.i:43: Warning: - recursive call during value analysis - of __gen_e_acsl_fib (__gen_e_acsl_fib <- fib :: tests/constructs/decrease.i:40 <- - __gen_e_acsl_fib :: tests/constructs/decrease.i:74 <- - main). - Assuming the call has no effect. The analysis will be unsound. -[eva] tests/constructs/decrease.i:43: Warning: - recursive call during value analysis - of __gen_e_acsl_fib (__gen_e_acsl_fib <- fib :: tests/constructs/decrease.i:40 <- - __gen_e_acsl_fib :: tests/constructs/decrease.i:74 <- - main). - Assuming the call has no effect. The analysis will be unsound. -[eva:alarm] tests/constructs/decrease.i:43: Warning: - signed overflow. - assert -2147483648 ≤ tmp + tmp_0; - (tmp from fib(n - 1), tmp_0 from fib(n - 2)) -[eva:alarm] tests/constructs/decrease.i:43: Warning: - signed overflow. - assert tmp + tmp_0 ≤ 2147483647; - (tmp from fib(n - 1), tmp_0 from fib(n - 2)) -[eva:alarm] tests/constructs/decrease.i:75: Warning: - function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva] tests/constructs/decrease.i:58: Warning: - recursive call during value analysis - of __gen_e_acsl_even (__gen_e_acsl_even <- odd :: tests/constructs/decrease.i:47 <- - __gen_e_acsl_odd :: tests/constructs/decrease.i:52 <- - even :: tests/constructs/decrease.i:50 <- - __gen_e_acsl_even :: tests/constructs/decrease.i:77 <- - main). - Assuming the call has no effect. The analysis will be unsound. -[eva:alarm] tests/constructs/decrease.i:78: Warning: - function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva] tests/constructs/decrease.i:58: Warning: - recursive call during value analysis - of __gen_e_acsl_even (__gen_e_acsl_even <- odd :: tests/constructs/decrease.i:47 <- - __gen_e_acsl_odd :: tests/constructs/decrease.i:52 <- - even :: tests/constructs/decrease.i:50 <- - __gen_e_acsl_even :: tests/constructs/decrease.i:79 <- - main). - Assuming the call has no effect. The analysis will be unsound. -[eva:alarm] tests/constructs/decrease.i:80: Warning: - function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva] tests/constructs/decrease.i:52: Warning: - recursive call during value analysis - of __gen_e_acsl_odd (__gen_e_acsl_odd <- even :: tests/constructs/decrease.i:50 <- - __gen_e_acsl_even :: tests/constructs/decrease.i:58 <- - odd :: tests/constructs/decrease.i:47 <- - __gen_e_acsl_odd :: tests/constructs/decrease.i:81 <- - main). - Assuming the call has no effect. The analysis will be unsound. -[eva:alarm] tests/constructs/decrease.i:82: Warning: - function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva] tests/constructs/decrease.i:52: Warning: - recursive call during value analysis - of __gen_e_acsl_odd (__gen_e_acsl_odd <- even :: tests/constructs/decrease.i:50 <- - __gen_e_acsl_even :: tests/constructs/decrease.i:58 <- - odd :: tests/constructs/decrease.i:47 <- - __gen_e_acsl_odd :: tests/constructs/decrease.i:83 <- - main). - Assuming the call has no effect. The analysis will be unsound. -[eva:alarm] tests/constructs/decrease.i:84: Warning: - function __e_acsl_assert, behavior blocking: precondition got status unknown. diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c index 41a66ca7b5e..116816df289 100644 --- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c +++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c @@ -87,8 +87,6 @@ int fib(int n) } tmp = __gen_e_acsl_fib(n - 1); tmp_0 = __gen_e_acsl_fib(n - 2); - /*@ assert Eva: signed_overflow: -2147483648 ≤ tmp + tmp_0; */ - /*@ assert Eva: signed_overflow: tmp + tmp_0 ≤ 2147483647; */ __retres = tmp + tmp_0; return_label: return __retres; } -- GitLab