From 30a8d8da36a7dc34411e5ea99ab740b7769ec788 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Sat, 14 Aug 2021 17:20:50 +0200
Subject: [PATCH] [e-acsl:tests] new test proving the unsoundness of \sum
---
.../e-acsl/tests/arith/oracle/gen_sum.c | 30 +++++++++++++++++++
.../e-acsl/tests/arith/oracle/sum.res.oracle | 2 ++
src/plugins/e-acsl/tests/arith/sum.c | 1 +
3 files changed, 33 insertions(+)
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 c5f401dc6b8..217df1e0d43 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
@@ -204,6 +204,36 @@ int main(void)
\lambda ℤ k; 1)
≡ 6; */
;
+ {
+ 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;
+ __gen_e_acsl_one_6 = 1;
+ __gen_e_acsl_cond_6 = 0;
+ __gen_e_acsl_lambda_6 = 0;
+ __gen_e_acsl_sum_6 = 0;
+ __gen_e_acsl_k_6 = 2147483647U;
+ while (1) {
+ __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_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",
+ "\\sum(2147483647, 2147483647, \\lambda integer k; k) + 1 > 2147483647",
+ "tests/arith/sum.c",16);
+ }
+ /*@ assert \sum(2147483647, 2147483647, \lambda ℤ k; k) + 1 > 2147483647;
+ */
+ ;
__retres = 0;
return __retres;
}
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 fabbced782e..b6ea52e13cb 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle
@@ -16,3 +16,5 @@
[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;
diff --git a/src/plugins/e-acsl/tests/arith/sum.c b/src/plugins/e-acsl/tests/arith/sum.c
index 3d8e9a551fe..dfa6b761cb4 100644
--- a/src/plugins/e-acsl/tests/arith/sum.c
+++ b/src/plugins/e-acsl/tests/arith/sum.c
@@ -13,6 +13,7 @@ int main(void) {
/*@ assert \sum(10, 2, \lambda integer k; k) == 0; */;
/*@ assert \sum(x * x, 2, \lambda integer k; k) == 0; */;
/*@ assert \sum(ULLONG_MAX - 5, ULLONG_MAX, \lambda integer k; 1) == 6; */;
+ /*@ assert \sum(INT_MAX, INT_MAX, \lambda integer k; k) + 1 > INT_MAX; */
return 0;
}
--
GitLab