diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml index 91807d502aa5ad5089b4c5acd90ef71a89b298f6..a17d2b3b7f535a9619bfe08e0f8e335ffc6fcab6 100644 --- a/src/plugins/e-acsl/src/analyses/interval.ml +++ b/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. *) diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c b/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c index 217df1e0d43af0579fd78e3308f5841c998d066c..ec90f50490c41ddaf232785f5390e53a240043c0 100644 --- a/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c +++ b/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); } diff --git a/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle index b6ea52e13cb7621a3b3ed4a0b7f6fc52b609b37a..e11486ce61cb951c82b1443d7722c119f2bbc16d 100644 --- a/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle +++ b/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.