From 2afb433a59a97d99fe7f8fd8ceee96640de795ea Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Tue, 12 Oct 2021 16:18:36 +0200
Subject: [PATCH] [e-acsl] add tests
---
.../tests/gmp-only/extended_quantifiers.i | 20 ++++
.../oracle/extended_quantifiers.res.oracle | 6 ++
.../oracle/gen_extended_quantifiers.c | 94 +++++++++++++++++++
3 files changed, 120 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i
create mode 100644 src/plugins/e-acsl/tests/gmp-only/oracle/extended_quantifiers.res.oracle
create mode 100644 src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
diff --git a/src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i b/src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i
new file mode 100644
index 00000000000..4d961894a25
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i
@@ -0,0 +1,20 @@
+/* run.config
+ COMMENT: extended quantifiers (sum, product, numof)
+*/
+
+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 \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); */
+ ;
+
+ 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
new file mode 100644
index 00000000000..25892758b26
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/extended_quantifiers.res.oracle
@@ -0,0 +1,6 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:11: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:11: 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
new file mode 100644
index 00000000000..f38b7f68218
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
@@ -0,0 +1,94 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+int main(void)
+{
+ int __retres;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_k;
+ __e_acsl_mpz_t __gen_e_acsl_one;
+ 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;
+ int __gen_e_acsl_eq;
+ __gmpz_init_set_si(__gen_e_acsl_,2L);
+ __gmpz_init_set_si(__gen_e_acsl__2,10L);
+ __gmpz_init_set_si(__gen_e_acsl_one,1L);
+ __gen_e_acsl_cond = 0;
+ __gmpz_init_set_si(__gen_e_acsl_lambda,0L);
+ __gmpz_init_set_si(__gen_e_acsl_accumulator,0L);
+ __gmpz_init_set(__gen_e_acsl_k,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ while (1) {
+ __gen_e_acsl_cond = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ if (__gen_e_acsl_cond > 0) break;
+ 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;
+ __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_set(__gen_e_acsl_lambda,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __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_add(__gen_e_acsl_accumulator,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda));
+ __gmpz_add(__gen_e_acsl_k,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_one));
+ }
+ }
+ __gmpz_init_set_si(__gen_e_acsl__7,9L);
+ __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_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);
+ __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);
+ }
+ /*@ assert \numof(2, 10, \lambda ℤ k; k - 2 ≥ 0) ≡ 9; */ ;
+ __retres = 0;
+ return __retres;
+}
+
+
--
GitLab