[e-acsl] add tests

src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i

+/* 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;
+}

src/plugins/e-acsl/tests/gmp-only/oracle/extended_quantifiers.res.oracle

+[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.

src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c

+/* 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;
+}
+
+