[e-acsl] add test for bugfix

src/plugins/e-acsl/tests/bts/issue-eacsl-187.c

+/*@ predicate p(integer n) = \forall integer i; 0 <= i < n ==> 2 * i < n * i + 1; */
+
+int main(void) {
+  /*@ assert p(2); */
+}

src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-187.c

+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+/*@
+predicate p(integer n) = \forall integer i; 0 <= i < n ==> 2 * i < n * i + 1;
+
+*/
+int __gen_e_acsl_p(int n);
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  {
+    int __gen_e_acsl_p_2;
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+    __gen_e_acsl_p_2 = __gen_e_acsl_p(2);
+    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"p(2)",0,
+                                 __gen_e_acsl_p_2);
+    __gen_e_acsl_assert_data.blocking = 1;
+    __gen_e_acsl_assert_data.kind = "Assertion";
+    __gen_e_acsl_assert_data.pred_txt = "p(2)";
+    __gen_e_acsl_assert_data.file = "tests/bts/issue-eacsl-187.c";
+    __gen_e_acsl_assert_data.fct = "main";
+    __gen_e_acsl_assert_data.line = 4;
+    __e_acsl_assert(__gen_e_acsl_p_2,& __gen_e_acsl_assert_data);
+    __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+  }
+  /*@ assert p(2); */ ;
+  __retres = 0;
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+/*@ assigns \result;
+    assigns \result \from n; */
+int __gen_e_acsl_p(int n)
+{
+  int __gen_e_acsl_forall;
+  int __gen_e_acsl_i;
+  __gen_e_acsl_forall = 1;
+  __gen_e_acsl_i = 0;
+  while (1) {
+    if (__gen_e_acsl_i < n) ; else break;
+    if (2L * __gen_e_acsl_i < n * (long)__gen_e_acsl_i + 1L) ;
+    else {
+      __gen_e_acsl_forall = 0;
+      goto e_acsl_end_loop1;
+    }
+    __gen_e_acsl_i ++;
+  }
+  e_acsl_end_loop1: ;
+  return __gen_e_acsl_forall;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-187.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue-eacsl-187.c:4: Warning: 
+  assertion got status unknown.