From 349bf237aca7202fb91ae660f15c3ad331e86ebd Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 16 Jul 2021 15:40:24 +0200
Subject: [PATCH] [eacsl] Update tests
---
.../e-acsl/tests/bts/issue-eacsl-172.c | 9 ++++++++
.../tests/bts/oracle/gen_issue-eacsl-172.c | 21 +++++++++++++++++++
.../bts/oracle/issue-eacsl-172.res.oracle | 2 ++
.../oracle_dev/issue-eacsl-172.e-acsl.err.log | 0
4 files changed, 32 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/bts/issue-eacsl-172.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-172.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-172.e-acsl.err.log
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 00000000000..4be6d489f1a
--- /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 00000000000..fc026da4d14
--- /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 00000000000..efd02631129
--- /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 00000000000..e69de29bb2d
--
GitLab