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 0000000000000000000000000000000000000000..64c896816225bc4e3c40874e3ae0bb8a6a8e34f6 --- /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 0000000000000000000000000000000000000000..f8be21500b2e3acf531f87309718cba4c249f1fb --- /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 0000000000000000000000000000000000000000..7d556feb94e7297c6c986b727ae07354af5aacd4 --- /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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391