diff --git a/src/plugins/e-acsl/tests/constructs/decrease.i b/src/plugins/e-acsl/tests/constructs/decrease.i index b5dc3a50ca7515eb3f4fa32bcff259c351083bce..569bcb71d0f339ffec25afb1935e3da6e30b0053 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 74f4f63423966d0396e43ebbb9a02c8887c3ddcf..2a909408ab28551a31c8128f578c384ab0e246df 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 41a66ca7b5efb2a1f491aca7a9eefbe396862a59..116816df289b37cce0dcf9fe63c4b5fe6b748abf 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; }