From 7941e99a5ea009771f748c65085f5f3df8b7078b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 23 Mar 2022 16:37:08 +0100
Subject: [PATCH] [e-acsl] enable dune tests
---
src/plugins/e-acsl/.gitignore | 2 --
src/plugins/e-acsl/tests/builtin/dune | 7 +++++++
src/plugins/e-acsl/tests/builtin/strcat.c | 8 ++++----
src/plugins/e-acsl/tests/builtin/strcmp.c | 8 ++++----
src/plugins/e-acsl/tests/builtin/strcpy.c | 8 ++++----
src/plugins/e-acsl/tests/builtin/strlen.c | 8 ++++----
src/plugins/e-acsl/tests/dune | 13 ++++++-------
src/plugins/e-acsl/tests/format/dune | 7 +++++++
src/plugins/e-acsl/tests/format/fprintf.c | 6 +++---
src/plugins/e-acsl/tests/format/printf.c | 2 +-
src/plugins/e-acsl/tests/ptests_config | 3 ++-
src/plugins/e-acsl/tests/test_config | 5 +++--
src/plugins/e-acsl/tests/test_config_dev | 6 ++++--
13 files changed, 49 insertions(+), 34 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/builtin/dune
create mode 100644 src/plugins/e-acsl/tests/format/dune
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 5a408ad7fca..6f12194ddbc 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -49,8 +49,6 @@
/doc/userman/*.log
/doc/userman/*.lof
/doc/userman/eacslversion.tex
-/tests/test_config
-/tests/test_config_dev
/tests/*/result*/*
.frama-c
META.frama-c-e_acsl
diff --git a/src/plugins/e-acsl/tests/builtin/dune b/src/plugins/e-acsl/tests/builtin/dune
new file mode 100644
index 00000000000..9dbf4e24533
--- /dev/null
+++ b/src/plugins/e-acsl/tests/builtin/dune
@@ -0,0 +1,7 @@
+(subdir
+ result/utils
+ (copy_files ../../utils/*))
+
+(subdir
+ result_dev/utils
+ (copy_files ../../utils/*))
diff --git a/src/plugins/e-acsl/tests/builtin/strcat.c b/src/plugins/e-acsl/tests/builtin/strcat.c
index ae47c89f292..4f5097eee1c 100644
--- a/src/plugins/e-acsl/tests/builtin/strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/strcat.c
@@ -2,10 +2,10 @@
COMMENT: Test `strcat` and `strncat` E-ACSL built-ins
DEPS: @PTEST_DEPS@ utils/signalled.h
STDOPT: +"-eva-precision=1"
- COMMENT: This part is blank on purpose (test stability + Dune)
-
-
-
+*/
+/* run.config_dev
+ MACRO: INCLUDED_HEADERS utils/signalled.h
+ COMMENT: This part is blank on purpose (test stability + Dune)
*/
diff --git a/src/plugins/e-acsl/tests/builtin/strcmp.c b/src/plugins/e-acsl/tests/builtin/strcmp.c
index 10c86c02e0a..37f43a40214 100644
--- a/src/plugins/e-acsl/tests/builtin/strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/strcmp.c
@@ -2,10 +2,10 @@
COMMENT: Test `strcmp` and `strncmp` E-ACSL built-ins
DEPS: @PTEST_DEPS@ utils/signalled.h
STDOPT:
- COMMENT: This part is blank on purpose (test stability + Dune)
-
-
-
+*/
+/* run.config_dev
+ MACRO: INCLUDED_HEADERS utils/signalled.h
+ COMMENT: This part is blank on purpose (test stability + Dune)
*/
diff --git a/src/plugins/e-acsl/tests/builtin/strcpy.c b/src/plugins/e-acsl/tests/builtin/strcpy.c
index 51987a4299d..fcf30f6cd25 100644
--- a/src/plugins/e-acsl/tests/builtin/strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/strcpy.c
@@ -2,10 +2,10 @@
COMMENT: Test `strcpy` and `strncpy` E-ACSL built-ins
DEPS: @PTEST_DEPS@ utils/signalled.h
STDOPT:
- COMMENT: This part is blank on purpose (test stability + Dune)
-
-
-
+*/
+/* run.config_dev
+ MACRO: INCLUDED_HEADERS utils/signalled.h
+ COMMENT: This part is blank on purpose (test stability + Dune)
*/
diff --git a/src/plugins/e-acsl/tests/builtin/strlen.c b/src/plugins/e-acsl/tests/builtin/strlen.c
index b570dfe679e..5ec3ad21914 100644
--- a/src/plugins/e-acsl/tests/builtin/strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/strlen.c
@@ -2,10 +2,10 @@
COMMENT: Test `strlen` E-ACSL built-ins
DEPS: @PTEST_DEPS@ utils/signalled.h
STDOPT:
- COMMENT: This part is blank on purpose (test stability + Dune)
-
-
-
+*/
+/* run.config_dev
+ MACRO: INCLUDED_HEADERS utils/signalled.h
+ COMMENT: This part is blank on purpose (test stability + Dune)
*/
diff --git a/src/plugins/e-acsl/tests/dune b/src/plugins/e-acsl/tests/dune
index 30ba5050fcd..5a43bd223a0 100644
--- a/src/plugins/e-acsl/tests/dune
+++ b/src/plugins/e-acsl/tests/dune
@@ -1,7 +1,6 @@
-; Used by the ptests directive `LIBS: ../../print` in `tests_config` files.
-; (library
-; (name print)
-; (modules print)
-; (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-e-acsl.core)
-; (flags -open Frama_c_kernel)
-; )
+(library
+ (name E_ACSL_test)
+ (modules E_ACSL_test)
+ (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-e-acsl.core)
+ (flags -open Frama_c_kernel)
+)
diff --git a/src/plugins/e-acsl/tests/format/dune b/src/plugins/e-acsl/tests/format/dune
new file mode 100644
index 00000000000..9dbf4e24533
--- /dev/null
+++ b/src/plugins/e-acsl/tests/format/dune
@@ -0,0 +1,7 @@
+(subdir
+ result/utils
+ (copy_files ../../utils/*))
+
+(subdir
+ result_dev/utils
+ (copy_files ../../utils/*))
diff --git a/src/plugins/e-acsl/tests/format/fprintf.c b/src/plugins/e-acsl/tests/format/fprintf.c
index d882296dc46..71cbd78f9a6 100644
--- a/src/plugins/e-acsl/tests/format/fprintf.c
+++ b/src/plugins/e-acsl/tests/format/fprintf.c
@@ -2,11 +2,11 @@
COMMENT: Check behaviours of format functions
DEPS: @PTEST_DEPS@ utils/signalled.h
STDOPT: +"-eva-precision=1"
+*/
+/* run.config_dev
+ MACRO: INCLUDED_HEADERS utils/signalled.h
COMMENT: This part is blank on purpose (test stability + Dune)
-
-
-
*/
#include "utils/signalled.h"
diff --git a/src/plugins/e-acsl/tests/format/printf.c b/src/plugins/e-acsl/tests/format/printf.c
index a70af11be01..321fca54b30 100644
--- a/src/plugins/e-acsl/tests/format/printf.c
+++ b/src/plugins/e-acsl/tests/format/printf.c
@@ -5,11 +5,11 @@
*/
/* run.config_dev
MACRO: ROOT_EACSL_GCC_OPTS_EXT @ROOT_EACSL_GCC_OPTS_EXT@ -e "-Wno-maybe-uninitialized"
+ MACRO: INCLUDED_HEADERS utils/signalled.h
COMMENT: This part is blank on purpose (test stability + Dune)
-
*/
#include "utils/signalled.h"
diff --git a/src/plugins/e-acsl/tests/ptests_config b/src/plugins/e-acsl/tests/ptests_config
index 824139152c3..0c0f44a5c36 100644
--- a/src/plugins/e-acsl/tests/ptests_config
+++ b/src/plugins/e-acsl/tests/ptests_config
@@ -1 +1,2 @@
-IGNORE= DEFAULT_SUITES = arith bts builtin constructs examples format full-mtracking gmp-only memory special temporal
+DEFAULT_SUITES = arith bts builtin concurrency constructs examples format full-mtracking gmp-only memory special temporal
+dev_SUITES = arith bts builtin concurrency constructs examples format full-mtracking gmp-only memory special temporal
diff --git a/src/plugins/e-acsl/tests/test_config b/src/plugins/e-acsl/tests/test_config
index 32bdb4f86a1..a729d3877fc 100644
--- a/src/plugins/e-acsl/tests/test_config
+++ b/src/plugins/e-acsl/tests/test_config
@@ -2,12 +2,13 @@ MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
MACRO: MACHDEP -machdep gcc_x86_64
MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -verbose 0 -no-unicode
-MACRO: EACSL -e-acsl -e-acsl-share @PTEST_SHARE_DIR@/e-acsl -e-acsl-verbose 1
+COMMENT: no more share to set with Dune
+MACRO: EACSL -e-acsl -e-acsl-verbose 1
MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive -eva-warn-key loop-unroll:auto=inactive
MACRO: EVENTUALLY -print -ocode @DEST@.c
-PLUGIN: E_ACSL eva,scope,variadic rtegen
+PLUGIN: e-acsl eva,scope,inout,variadic rtegen
LIBS: @PTEST_SUITE_DIR@/../E_ACSL_test
LOG: gen_@PTEST_NAME@.c
diff --git a/src/plugins/e-acsl/tests/test_config_dev b/src/plugins/e-acsl/tests/test_config_dev
index 0ce872fd889..4f999011228 100644
--- a/src/plugins/e-acsl/tests/test_config_dev
+++ b/src/plugins/e-acsl/tests/test_config_dev
@@ -7,10 +7,10 @@ MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X --no-assert-print-data
COMMENT: Default options for the frama-c invocation
MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0
-PLUGIN: E_ACSL eva,scope,variadic rtegen
+PLUGIN: e-acsl eva,scope,variadic rtegen
COMMENT: The dependency to the plugin share directory has not to be explicited
-DEPS: @PTEST_SUITE_DIR@/../wrapper.sh
+DEPS: @PTEST_SUITE_DIR@/../wrapper.sh @INCLUDED_HEADERS@
EXEC: LOG @EACSL_ERR@ @PTEST_SUITE_DIR@/../wrapper.sh "@frama-c-exe@" "@PTEST_RESULT@" "@PTEST_NAME@" "@PTEST_FILE@" "@EACSL_ERR@" "@ROOT_EACSL_GCC_MISC_OPTS@ @ROOT_EACSL_GCC_OPTS_EXT@" "@PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@ @ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" "@ROOT_EACSL_EXEC_FILTER@"
@@ -26,3 +26,5 @@ COMMENT: Define the following macro in a test to filter the output of the test e
COMMENT: You can chain several filters by separating commands with |. However sed cannot
COMMENT: use | as a delimiter, please use / or another character instead.
MACRO: ROOT_EACSL_EXEC_FILTER cat
+
+MACRO: INCLUDED_HEADERS
--
GitLab