From f9b2a1053b91b7f362b6dc14c7514146cd4511fb Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Wed, 13 Oct 2021 10:03:49 +0200
Subject: [PATCH] [e-acsl] code review
---
.../src/analyses/predicate_normalizer.ml | 1 -
src/plugins/e-acsl/src/analyses/typing.ml | 2 +
.../tests/gmp-only/extended_quantifiers.i | 11 +-
.../oracle/extended_quantifiers.res.oracle | 20 +-
.../oracle/gen_extended_quantifiers.c | 277 +++++++++++++++---
5 files changed, 266 insertions(+), 45 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml b/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
index 8ff2f7c5a09..46efb9de68c 100644
--- a/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
+++ b/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
@@ -134,7 +134,6 @@ let preprocess_term ~loc t =
(Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
| _ -> None
-
let preprocessor = object
inherit Visitor.frama_c_inplace
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 787dd4cc249..f7159b31556 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -416,6 +416,8 @@ let rec type_term
| TSizeOfStr _
| TAlignOf _ ->
let i = Interval.infer t in
+ (* a constant or an left value directly under a lambda should be a gmp
+ if the infered context for the lambda is gmp *)
let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
dup ty
diff --git a/src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i b/src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i
index 4d961894a25..b8da5291288 100644
--- a/src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i
+++ b/src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i
@@ -4,16 +4,13 @@
int main(void) {
- /* assert \sum(2, 10, \lambda integer k; 2 * k) == 108; */;
- /* assert \sum(10, 2, \lambda integer k; k) == 0; */;
- /* assert \sum(1, 10, \lambda integer k; 1) == 10; */;
+ /*@ assert \sum(2, 10, \lambda integer k; 2 * k) == 108; */;
+ /*@ assert \sum(1, 10, \lambda integer k; 1) == 10; */;
/*@ assert \numof(2, 10, \lambda integer k; k - 2 >= 0) == 9; */;
- /* assert \product(1, 10, \lambda integer k; k) == 3628800; */;
- /* assert \product(-10, 10, \lambda integer k; k) == 0; */;
- /* assert \product(-20, -1, \lambda integer k; 2 * k)
- == \product(1, 20, \lambda integer k; 2 * k); */
+ /*@ assert \product(1, 10, \lambda integer k; k) == 3628800; */;
+ /*@ assert \product(-10, 10, \lambda integer k; k) == 0; */;
;
return 0;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/extended_quantifiers.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle/extended_quantifiers.res.oracle
index 25892758b26..ab3eacdf01b 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/extended_quantifiers.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/extended_quantifiers.res.oracle
@@ -1,6 +1,22 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp-only/extended_quantifiers.i:11: Warning:
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:7: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/gmp-only/extended_quantifiers.i:11: Warning:
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:7: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:8: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:8: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:10: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:10: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:12: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:12: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:13: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:13: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
index f38b7f68218..f20f45faae5 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
@@ -14,7 +14,7 @@ int main(void)
int __gen_e_acsl_cond;
__e_acsl_mpz_t __gen_e_acsl_lambda;
__e_acsl_mpz_t __gen_e_acsl_accumulator;
- __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl__4;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_,2L);
__gmpz_init_set_si(__gen_e_acsl__2,10L);
@@ -31,38 +31,16 @@ int main(void)
else {
{
__e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl_sub;
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_ge;
- __e_acsl_mpz_t __gen_e_acsl_if;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
__gmpz_init_set_si(__gen_e_acsl__3,2L);
- __gmpz_init(__gen_e_acsl_sub);
- __gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_k),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __gmpz_init_set_si(__gen_e_acsl__4,0L);
- __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- if (__gen_e_acsl_ge >= 0) {
- __e_acsl_mpz_t __gen_e_acsl__5;
- __gmpz_init_set_si(__gen_e_acsl__5,1L);
- __gmpz_init_set(__gen_e_acsl_if,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __gmpz_clear(__gen_e_acsl__5);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__6;
- __gmpz_init_set_si(__gen_e_acsl__6,0L);
- __gmpz_init_set(__gen_e_acsl_if,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
- __gmpz_clear(__gen_e_acsl__6);
- }
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k));
__gmpz_set(__gen_e_acsl_lambda,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
__gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_sub);
- __gmpz_clear(__gen_e_acsl__4);
- __gmpz_clear(__gen_e_acsl_if);
+ __gmpz_clear(__gen_e_acsl_mul);
}
__gmpz_add(__gen_e_acsl_accumulator,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator),
@@ -72,21 +50,250 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_one));
}
}
- __gmpz_init_set_si(__gen_e_acsl__7,9L);
+ __gmpz_init_set_si(__gen_e_acsl__4,108L);
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","main",
- "\\numof(2, 10, \\lambda integer k; k - 2 >= 0) == 9",
- "tests/gmp-only/extended_quantifiers.i",11);
+ "\\sum(2, 10, \\lambda integer k; 2 * k) == 108",
+ "tests/gmp-only/extended_quantifiers.i",7);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl__2);
__gmpz_clear(__gen_e_acsl_k);
__gmpz_clear(__gen_e_acsl_one);
__gmpz_clear(__gen_e_acsl_lambda);
__gmpz_clear(__gen_e_acsl_accumulator);
- __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl__4);
+ }
+ /*@ assert \sum(2, 10, \lambda ℤ k; 2 * k) ≡ 108; */ ;
+ {
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_k_2;
+ __e_acsl_mpz_t __gen_e_acsl_one_2;
+ int __gen_e_acsl_cond_2;
+ __e_acsl_mpz_t __gen_e_acsl_lambda_2;
+ __e_acsl_mpz_t __gen_e_acsl_accumulator_2;
+ int __gen_e_acsl_eq_2;
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
+ __gmpz_init_set_si(__gen_e_acsl__6,10L);
+ __gmpz_init_set_si(__gen_e_acsl_one_2,1L);
+ __gen_e_acsl_cond_2 = 0;
+ __gmpz_init_set_si(__gen_e_acsl_lambda_2,0L);
+ __gmpz_init_set_si(__gen_e_acsl_accumulator_2,0L);
+ __gmpz_init_set(__gen_e_acsl_k_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ while (1) {
+ __gen_e_acsl_cond_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ if (__gen_e_acsl_cond_2 > 0) break;
+ else {
+ {
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __gmpz_init_set_str(__gen_e_acsl__7,"1",10);
+ __gmpz_set(__gen_e_acsl_lambda_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_clear(__gen_e_acsl__7);
+ }
+ __gmpz_add(__gen_e_acsl_accumulator_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_2));
+ __gmpz_add(__gen_e_acsl_k_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_2));
+ }
+ }
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,1,"Assertion","main",
+ "\\sum(1, 10, \\lambda integer k; 1) == 10",
+ "tests/gmp-only/extended_quantifiers.i",8);
+ __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_k_2);
+ __gmpz_clear(__gen_e_acsl_one_2);
+ __gmpz_clear(__gen_e_acsl_lambda_2);
+ __gmpz_clear(__gen_e_acsl_accumulator_2);
+ }
+ /*@ assert \sum(1, 10, \lambda ℤ k; 1) ≡ 10; */ ;
+ {
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl_k_3;
+ __e_acsl_mpz_t __gen_e_acsl_one_3;
+ int __gen_e_acsl_cond_3;
+ __e_acsl_mpz_t __gen_e_acsl_lambda_3;
+ __e_acsl_mpz_t __gen_e_acsl_accumulator_3;
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ int __gen_e_acsl_eq_3;
+ __gmpz_init_set_si(__gen_e_acsl__8,2L);
+ __gmpz_init_set_si(__gen_e_acsl__9,10L);
+ __gmpz_init_set_si(__gen_e_acsl_one_3,1L);
+ __gen_e_acsl_cond_3 = 0;
+ __gmpz_init_set_si(__gen_e_acsl_lambda_3,0L);
+ __gmpz_init_set_si(__gen_e_acsl_accumulator_3,0L);
+ __gmpz_init_set(__gen_e_acsl_k_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ while (1) {
+ __gen_e_acsl_cond_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ if (__gen_e_acsl_cond_3 > 0) break;
+ else {
+ {
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ int __gen_e_acsl_ge;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __gmpz_init_set_si(__gen_e_acsl__10,2L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __gmpz_init_set_si(__gen_e_acsl__11,0L);
+ __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ if (__gen_e_acsl_ge >= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__12;
+ __gmpz_init_set_si(__gen_e_acsl__12,1L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ __gmpz_clear(__gen_e_acsl__12);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__13;
+ __gmpz_init_set_si(__gen_e_acsl__13,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ __gmpz_clear(__gen_e_acsl__13);
+ }
+ __gmpz_set(__gen_e_acsl_lambda_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl_if);
+ }
+ __gmpz_add(__gen_e_acsl_accumulator_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_3));
+ __gmpz_add(__gen_e_acsl_k_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_3));
+ }
+ }
+ __gmpz_init_set_si(__gen_e_acsl__14,9L);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ __e_acsl_assert(__gen_e_acsl_eq_3 == 0,1,"Assertion","main",
+ "\\numof(2, 10, \\lambda integer k; k - 2 >= 0) == 9",
+ "tests/gmp-only/extended_quantifiers.i",10);
+ __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_k_3);
+ __gmpz_clear(__gen_e_acsl_one_3);
+ __gmpz_clear(__gen_e_acsl_lambda_3);
+ __gmpz_clear(__gen_e_acsl_accumulator_3);
+ __gmpz_clear(__gen_e_acsl__14);
}
/*@ assert \numof(2, 10, \lambda ℤ k; k - 2 ≥ 0) ≡ 9; */ ;
+ {
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl__16;
+ __e_acsl_mpz_t __gen_e_acsl_k_4;
+ __e_acsl_mpz_t __gen_e_acsl_one_4;
+ int __gen_e_acsl_cond_4;
+ __e_acsl_mpz_t __gen_e_acsl_lambda_4;
+ __e_acsl_mpz_t __gen_e_acsl_accumulator_4;
+ __e_acsl_mpz_t __gen_e_acsl__17;
+ int __gen_e_acsl_eq_4;
+ __gmpz_init_set_si(__gen_e_acsl__15,1L);
+ __gmpz_init_set_si(__gen_e_acsl__16,10L);
+ __gmpz_init_set_si(__gen_e_acsl_one_4,1L);
+ __gen_e_acsl_cond_4 = 0;
+ __gmpz_init_set_si(__gen_e_acsl_lambda_4,0L);
+ __gmpz_init_set_si(__gen_e_acsl_accumulator_4,1L);
+ __gmpz_init_set(__gen_e_acsl_k_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
+ while (1) {
+ __gen_e_acsl_cond_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
+ if (__gen_e_acsl_cond_4 > 0) break;
+ else {
+ __gmpz_set(__gen_e_acsl_lambda_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4));
+ __gmpz_mul(__gen_e_acsl_accumulator_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_4));
+ __gmpz_add(__gen_e_acsl_k_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_4));
+ }
+ }
+ __gmpz_init_set_ui(__gen_e_acsl__17,3628800UL);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
+ __e_acsl_assert(__gen_e_acsl_eq_4 == 0,1,"Assertion","main",
+ "\\product(1, 10, \\lambda integer k; k) == 3628800",
+ "tests/gmp-only/extended_quantifiers.i",12);
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl__16);
+ __gmpz_clear(__gen_e_acsl_k_4);
+ __gmpz_clear(__gen_e_acsl_one_4);
+ __gmpz_clear(__gen_e_acsl_lambda_4);
+ __gmpz_clear(__gen_e_acsl_accumulator_4);
+ __gmpz_clear(__gen_e_acsl__17);
+ }
+ /*@ assert \product(1, 10, \lambda ℤ k; k) ≡ 3628800; */ ;
+ {
+ __e_acsl_mpz_t __gen_e_acsl__18;
+ __e_acsl_mpz_t __gen_e_acsl_neg;
+ __e_acsl_mpz_t __gen_e_acsl_k_5;
+ __e_acsl_mpz_t __gen_e_acsl_one_5;
+ int __gen_e_acsl_cond_5;
+ __e_acsl_mpz_t __gen_e_acsl_lambda_5;
+ __e_acsl_mpz_t __gen_e_acsl_accumulator_5;
+ __e_acsl_mpz_t __gen_e_acsl__19;
+ int __gen_e_acsl_eq_5;
+ __gmpz_init_set_si(__gen_e_acsl__18,10L);
+ __gmpz_init(__gen_e_acsl_neg);
+ __gmpz_neg(__gen_e_acsl_neg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
+ __gmpz_init_set_si(__gen_e_acsl_one_5,1L);
+ __gen_e_acsl_cond_5 = 0;
+ __gmpz_init_set_si(__gen_e_acsl_lambda_5,0L);
+ __gmpz_init_set_si(__gen_e_acsl_accumulator_5,1L);
+ __gmpz_init_set(__gen_e_acsl_k_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg));
+ while (1) {
+ __gen_e_acsl_cond_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
+ if (__gen_e_acsl_cond_5 > 0) break;
+ else {
+ __gmpz_set(__gen_e_acsl_lambda_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_5));
+ __gmpz_mul(__gen_e_acsl_accumulator_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_5));
+ __gmpz_add(__gen_e_acsl_k_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_5));
+ }
+ }
+ __gmpz_init_set_si(__gen_e_acsl__19,0L);
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
+ __e_acsl_assert(__gen_e_acsl_eq_5 == 0,1,"Assertion","main",
+ "\\product(-10, 10, \\lambda integer k; k) == 0",
+ "tests/gmp-only/extended_quantifiers.i",13);
+ __gmpz_clear(__gen_e_acsl__18);
+ __gmpz_clear(__gen_e_acsl_neg);
+ __gmpz_clear(__gen_e_acsl_k_5);
+ __gmpz_clear(__gen_e_acsl_one_5);
+ __gmpz_clear(__gen_e_acsl_lambda_5);
+ __gmpz_clear(__gen_e_acsl_accumulator_5);
+ __gmpz_clear(__gen_e_acsl__19);
+ }
+ /*@ assert \product(-10, 10, \lambda ℤ k; k) ≡ 0; */ ;
__retres = 0;
return __retres;
}
--
GitLab