[e-acsl] In test decrease.i, uses Eva parameter -eva-unroll-recursive-calls.

Instead of the deprecated parameter -eva-ignore-recursive-calls.

src/plugins/e-acsl/tests/constructs/decrease.i

 /* 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

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.

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;
 }