From 078a1a272d73f32edb1351a89afd59290f13f5b8 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 15 Oct 2020 16:04:19 +0200
Subject: [PATCH] [eacsl] Add tests for memory models compilation
---
.../e-acsl/tests/special/e-acsl-bittree-model.c | 8 ++++++++
.../e-acsl/tests/special/e-acsl-segment-model.c | 8 ++++++++
.../oracle_ci/e-acsl-bittree-model.res.oracle | 2 ++
.../oracle_ci/e-acsl-segment-model.res.oracle | 2 ++
.../special/oracle_ci/gen_e-acsl-bittree-model.c | 16 ++++++++++++++++
.../special/oracle_ci/gen_e-acsl-segment-model.c | 16 ++++++++++++++++
.../e-acsl-bittree-model.e-acsl.err.log | 0
.../e-acsl-segment-model.e-acsl.err.log | 0
8 files changed, 52 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c
create mode 100644 src/plugins/e-acsl/tests/special/e-acsl-segment-model.c
create mode 100644 src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-bittree-model.res.oracle
create mode 100644 src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-segment-model.res.oracle
create mode 100644 src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-bittree-model.c
create mode 100644 src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-segment-model.c
create mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-bittree-model.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-segment-model.e-acsl.err.log
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c b/src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c
new file mode 100644
index 00000000000..efdd82a5ee0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c
@@ -0,0 +1,8 @@
+/* run.config_ci, run.config_dev
+ COMMENT: Compile RTL with bittree memory model
+ STDOPT:#"-e-acsl-full-mtracking"
+ MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --memory-model bittree
+ */
+int main() {
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-segment-model.c b/src/plugins/e-acsl/tests/special/e-acsl-segment-model.c
new file mode 100644
index 00000000000..d9bf523c549
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/e-acsl-segment-model.c
@@ -0,0 +1,8 @@
+/* run.config_ci, run.config_dev
+ COMMENT: Compile RTL with segment memory model
+ STDOPT:#"-e-acsl-full-mtracking"
+ MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --memory-model segment
+ */
+int main() {
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-bittree-model.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-bittree-model.res.oracle
new file mode 100644
index 00000000000..efd02631129
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-bittree-model.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/e-acsl-segment-model.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-segment-model.res.oracle
new file mode 100644
index 00000000000..efd02631129
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-segment-model.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-bittree-model.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-bittree-model.c
new file mode 100644
index 00000000000..8673c9a15aa
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-bittree-model.c
@@ -0,0 +1,16 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& __retres),(size_t)4);
+ __e_acsl_full_init((void *)(& __retres));
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& __retres));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-segment-model.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-segment-model.c
new file mode 100644
index 00000000000..8673c9a15aa
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-segment-model.c
@@ -0,0 +1,16 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& __retres),(size_t)4);
+ __e_acsl_full_init((void *)(& __retres));
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& __retres));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-bittree-model.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-bittree-model.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-segment-model.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-segment-model.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
--
GitLab