[e-acsl] add test for issue eacsl#149

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

+#include <limits.h>
+
+int main (int argc, char *argv[]) {
+  /*@ assert \exists unsigned int x; -1 < x < 5 && x == 0;*/
+  /*@ assert !(\forall unsigned int x; -1 < x < 5 ==> x != 0);*/
+  return 0;
+}

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

+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(int argc, char **argv)
+{
+  int __retres;
+  {
+    int __gen_e_acsl_exists;
+    int __gen_e_acsl_x;
+    __gen_e_acsl_exists = 0;
+    /*@ assert
+        Eva: signed_overflow: (unsigned int)((int)(-1)) + 1 ≤ 2147483647;
+    */
+    __gen_e_acsl_x = (unsigned int)(-1) + 1;
+    while (1) {
+      if (__gen_e_acsl_x < 5) ; else break;
+      if (! (__gen_e_acsl_x == 0)) ;
+      else {
+        __gen_e_acsl_exists = 1;
+        goto e_acsl_end_loop1;
+      }
+      __gen_e_acsl_x ++;
+    }
+    e_acsl_end_loop1: ;
+    __e_acsl_assert(__gen_e_acsl_exists,1,"Assertion","main",
+                    "\\exists unsigned int x; -1 < x < 5 && x == 0",
+                    "tests/bts/issue-eacsl-149.c",4);
+  }
+  /*@ assert ∃ unsigned int x; -1 < x < 5 ∧ x ≡ 0; */ ;
+  {
+    int __gen_e_acsl_forall;
+    int __gen_e_acsl_x_2;
+    __gen_e_acsl_forall = 1;
+    __gen_e_acsl_x_2 = (unsigned int)(-1) + 1;
+    while (1) {
+      if (__gen_e_acsl_x_2 < 5) ; else break;
+      if (__gen_e_acsl_x_2 != 0) ;
+      else {
+        __gen_e_acsl_forall = 0;
+        goto e_acsl_end_loop2;
+      }
+      __gen_e_acsl_x_2 ++;
+    }
+    e_acsl_end_loop2: ;
+    __e_acsl_assert(! __gen_e_acsl_forall,1,"Assertion","main",
+                    "!(\\forall unsigned int x; -1 < x < 5 ==> x != 0)",
+                    "tests/bts/issue-eacsl-149.c",5);
+  }
+  /*@ assert ¬(∀ unsigned int x; -1 < x < 5 ⇒ x ≢ 0); */ ;
+  __retres = 0;
+  return __retres;
+}
+
+

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

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue-eacsl-149.c:4: Warning: 
+  signed overflow. assert (unsigned int)((int)(-1)) + 1 ≤ 2147483647;