[e-acsl:interval] fix the unsoundness bug of \sum

src/plugins/e-acsl/src/analyses/interval.ml

@@ -360,7 +360,7 @@ let interv_of_extended_quantifier lambda lb up name =
        let max_lb, max_ub = Ival.min_and_max ub_iv in
        (* the number of iterations is the distance between the upper bound and
           the lower bound, or 0 if it is negative. *)
-       let delta a b = Z.max Z.zero (Z.sub a b) in
+       let delta a b = Z.max Z.zero (Z.add Z.one (Z.sub a b)) in
        let min_iteration_number =
          (* the minimum number of iterations is the distance between the
             smallest upper bound and the biggest lower bound. *)

src/plugins/e-acsl/tests/arith/oracle/gen_sum.c

@@ -208,8 +208,8 @@ int main(void)
     unsigned int __gen_e_acsl_k_6;
     unsigned int __gen_e_acsl_one_6;
     int __gen_e_acsl_cond_6;
-    int __gen_e_acsl_lambda_6;
-    int __gen_e_acsl_sum_6;
+    unsigned int __gen_e_acsl_lambda_6;
+    unsigned int __gen_e_acsl_sum_6;
     __gen_e_acsl_one_6 = 1;
     __gen_e_acsl_cond_6 = 0;
     __gen_e_acsl_lambda_6 = 0;
@@ -219,15 +219,13 @@ int main(void)
       __gen_e_acsl_cond_6 = __gen_e_acsl_k_6 > 2147483647U;
       if (__gen_e_acsl_cond_6) break;
       else {
-        __gen_e_acsl_lambda_6 = (int)__gen_e_acsl_k_6;
+        __gen_e_acsl_lambda_6 = __gen_e_acsl_k_6;
         __gen_e_acsl_sum_6 += __gen_e_acsl_lambda_6;
         __gen_e_acsl_k_6 += __gen_e_acsl_one_6;
       }
     }
-    /*@ assert Eva: signed_overflow: __gen_e_acsl_sum_6 + 1 ≤ 2147483647;
-    */
-    __e_acsl_assert((unsigned int)(__gen_e_acsl_sum_6 + 1) > 2147483647U,1,
-                    "Assertion","main",
+    __e_acsl_assert(__gen_e_acsl_sum_6 + 1U > 2147483647U,1,"Assertion",
+                    "main",
                     "\\sum(2147483647, 2147483647, \\lambda integer k; k) + 1 > 2147483647",
                     "tests/arith/sum.c",16);
   }

src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle

@@ -16,5 +16,4 @@
 [eva:alarm] tests/arith/sum.c:15: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/arith/sum.c:15: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/sum.c:16: Warning: 
-  signed overflow. assert __gen_e_acsl_sum_6 + 1 ≤ 2147483647;
+[eva:alarm] tests/arith/sum.c:16: Warning: assertion got status unknown.