[e-acsl] In tests, uses the Eva parameter -eva-unroll-recursive-calls.

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

src/plugins/e-acsl/tests/arith/functions_rec.c

 /* run.config_ci
    COMMENT: recursive logic functions
-   STDOPT: +"-eva-ignore-recursive-calls"
+   STDOPT: +"-eva-unroll-recursive-calls 100"
 */
 
 /*@ logic integer f1(integer n) =

src/plugins/e-acsl/tests/arith/longlong.i

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

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.

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;

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;

src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle

 [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: 

src/plugins/e-acsl/tests/bts/bts1395.i

 /* run.config_ci
    COMMENT: recursive function
-   STDOPT: +"-eva-ignore-recursive-calls"
+   STDOPT: +"-eva-unroll-recursive-calls 5"
 */
 
 /*@ requires n > 0; */

src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle

 [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.

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