From 61deca84972591a08b44557f0d70cf6201c6fb6c Mon Sep 17 00:00:00 2001
From: thibautbenjamin <thibaut.benjamin@polytechnique.edu>
Date: Tue, 20 Jul 2021 15:02:39 +0200
Subject: [PATCH] [e-acsl] add test for issue eacsl#149

---
 .../e-acsl/tests/bts/issue-eacsl-149.c        |  7 +++
 .../tests/bts/oracle/gen_issue-eacsl-149.c    | 54 +++++++++++++++++++
 .../bts/oracle/issue-eacsl-149.res.oracle     |  4 ++
 .../oracle_dev/issue-eacsl-149.e-acsl.err.log |  0
 4 files changed, 65 insertions(+)
 create mode 100644 src/plugins/e-acsl/tests/bts/issue-eacsl-149.c
 create mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
 create mode 100644 src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-149.res.oracle
 create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-149.e-acsl.err.log

diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-149.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-149.c
new file mode 100644
index 00000000000..64c89681622
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-149.c
@@ -0,0 +1,7 @@
+#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;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
new file mode 100644
index 00000000000..f8be21500b2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
@@ -0,0 +1,54 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-149.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-149.res.oracle
new file mode 100644
index 00000000000..7d556feb94e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-149.res.oracle
@@ -0,0 +1,4 @@
+[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;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-149.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-149.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
-- 
GitLab