diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-172.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-172.c new file mode 100644 index 0000000000000000000000000000000000000000..4be6d489f1a879136e9c639d8f95e8ba6ed80cb4 --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-172.c @@ -0,0 +1,9 @@ +/* run.config + COMMENT: frama-c/e-acsl#172, test for a term with two successive logic + coercion. +*/ +double d2 = 11.; +int main() { + //@ assert (int)d2 > 10; + return 0; +} diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c new file mode 100644 index 0000000000000000000000000000000000000000..fc026da4d148cc8c2687c8506992e1dae583cfd6 --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c @@ -0,0 +1,21 @@ +/* Generated by Frama-C */ +#include "stddef.h" +#include "stdio.h" +double d2 = 11.; +int main(void) +{ + int __retres; + __e_acsl_assert(-2147483649. < d2,1,"RTE","main", + "float_to_int: -2147483649 < d2", + "tests/bts/issue-eacsl-172.c",7); + __e_acsl_assert(d2 < 2147483648.,1,"RTE","main", + "float_to_int: d2 < 2147483648", + "tests/bts/issue-eacsl-172.c",7); + __e_acsl_assert((int)d2 > 10,1,"Assertion","main","(int)d2 > 10", + "tests/bts/issue-eacsl-172.c",7); + /*@ assert (int)d2 > 10; */ ; + __retres = 0; + return __retres; +} + + diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-172.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-172.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624 --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-172.res.oracle @@ -0,0 +1,2 @@ +[e-acsl] beginning translation. +[e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-172.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-172.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391