From 15a5ef1245bd7c6677bbf6681a69497090315762 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 13 Oct 2020 11:05:09 +0200
Subject: [PATCH] [eacsl] Add test for debug RTL compilation
---
src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c | 8 ++++++++
.../special/oracle_ci/e-acsl-rt-debug.res.oracle | 2 ++
.../tests/special/oracle_ci/gen_e-acsl-rt-debug.c | 11 +++++++++++
.../special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log | 0
4 files changed, 21 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
create mode 100644 src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-rt-debug.res.oracle
create mode 100644 src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-rt-debug.c
create mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c b/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
new file mode 100644
index 00000000000..8d050c12439
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
@@ -0,0 +1,8 @@
+/* run.config_ci, run.config_dev
+ COMMENT: Compile RTL with debug and debug verbose informations
+ STDOPT:#"-e-acsl-debug 1"
+ MACRO: ROOT_EACSL_GCC_OPTS_EXT --rt-debug --rt-verbose
+ */
+int main() {
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-rt-debug.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-rt-debug.res.oracle
new file mode 100644
index 00000000000..efd02631129
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-rt-debug.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/special/oracle_ci/gen_e-acsl-rt-debug.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-rt-debug.c
new file mode 100644
index 00000000000..5884b0f6c60
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-rt-debug.c
@@ -0,0 +1,11 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(void)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
--
GitLab