From 7d4304e83a66de0cce2b30faf7e1c7d6bfe410d2 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Sat, 14 Aug 2021 17:24:53 +0200
Subject: [PATCH] [e-acsl:interval] fix the unsoundness bug of \sum
---
src/plugins/e-acsl/src/analyses/interval.ml | 2 +-
src/plugins/e-acsl/tests/arith/oracle/gen_sum.c | 12 +++++-------
src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle | 3 +--
3 files changed, 7 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 91807d502aa..a17d2b3b7f5 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 217df1e0d43..ec90f50490c 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 b6ea52e13cb..e11486ce61c 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.
--
GitLab