From a233fd4f1e13d078c318d0d563cfa721e430a4db Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 27 Oct 2020 16:01:43 +0100
Subject: [PATCH] [PTESTS] allows to redefine the topvel command
---
ptests/Makefile | 9 +++++++--
ptests/ptests.ml | 11 ++++++++---
ptests/tests/cmd/README | 3 +++
ptests/tests/{ => cmd/tests}/ptests_config | 0
ptests/tests/{ => cmd/tests}/test_config | 0
.../tests/{ => cmd/tests}/without-test_config/README | 0
.../{ => cmd/tests}/without-test_config/config.i | 0
.../tests/{ => cmd/tests}/without-test_config/empty.i | 0
.../without-test_config/oracle/config.0.res.oracle | 0
.../without-test_config/oracle/config.1.res.oracle | 0
.../without-test_config/oracle/config.2.res.oracle | 0
.../without-test_config/oracle/config.3.res.oracle | 0
.../without-test_config/oracle/config.4.res.oracle | 0
.../without-test_config/oracle/empty.res.oracle | 0
ptests/tests/nothing/README | 3 +++
.../tests/nothing/tests/basic/oracle/empty.res.oracle | 1 +
ptests/tests/nothing/tests/ptests_config | 1 +
17 files changed, 23 insertions(+), 5 deletions(-)
create mode 100644 ptests/tests/cmd/README
rename ptests/tests/{ => cmd/tests}/ptests_config (100%)
rename ptests/tests/{ => cmd/tests}/test_config (100%)
rename ptests/tests/{ => cmd/tests}/without-test_config/README (100%)
rename ptests/tests/{ => cmd/tests}/without-test_config/config.i (100%)
rename ptests/tests/{ => cmd/tests}/without-test_config/empty.i (100%)
rename ptests/tests/{ => cmd/tests}/without-test_config/oracle/config.0.res.oracle (100%)
rename ptests/tests/{ => cmd/tests}/without-test_config/oracle/config.1.res.oracle (100%)
rename ptests/tests/{ => cmd/tests}/without-test_config/oracle/config.2.res.oracle (100%)
rename ptests/tests/{ => cmd/tests}/without-test_config/oracle/config.3.res.oracle (100%)
rename ptests/tests/{ => cmd/tests}/without-test_config/oracle/config.4.res.oracle (100%)
rename ptests/tests/{ => cmd/tests}/without-test_config/oracle/empty.res.oracle (100%)
create mode 100644 ptests/tests/nothing/README
create mode 100644 ptests/tests/nothing/tests/basic/oracle/empty.res.oracle
create mode 100644 ptests/tests/nothing/tests/ptests_config
diff --git a/ptests/Makefile b/ptests/Makefile
index 8dccd5f2574..2a5a585305a 100644
--- a/ptests/Makefile
+++ b/ptests/Makefile
@@ -6,8 +6,13 @@ purge-tests:
clean-tests: purge-tests
rm -rf _build/default/ptests/tests
+TESTS= nothing cmd
+# opts
+
run-tests: purge-tests
- dune exec -- ../ptests/ptests.exe ./tests
- dune build @tests/ptests
+ for dir in $(TESTS) ; do \
+ dune exec -- ../ptests/ptests.exe ./tests/$$dir/tests ; \
+ done
+ dune build $(addprefix @tests/,$(addsuffix /tests/ptests,$(TESTS)))
tests: run-tests
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 1bd64804faa..d73047c9f65 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -130,9 +130,10 @@ let () =
locale *)
let macro_default_options = "-journal-disable -check -no-autoload-plugins"
-let macro_frama_c_only = "frama-c @DEFAULT_OPTIONS@"
-let macro_frama_c_cmd = "frama-c @DEFAULT_OPTIONS@ @PLUGIN_OPTIONS@"
-let macro_frama_c = "frama-c @DEFAULT_OPTIONS@ @PLUGIN_OPTIONS@ @PTEST_FILE@"
+let macro_frama_c_exe = "frama-c"
+let macro_frama_c_only = "@frama-c-exe@ @DEFAULT_OPTIONS@"
+let macro_frama_c_cmd = "@frama-c-exe@ @DEFAULT_OPTIONS@ @PLUGIN_OPTIONS@"
+let macro_frama_c = "@frama-c-exe@ @DEFAULT_OPTIONS@ @PLUGIN_OPTIONS@ @PTEST_FILE@"
let example_msg =
Format.sprintf
@@ -160,6 +161,8 @@ let example_msg =
# the current list of options related to PLUGIN, MODULE and LIBS to load@ \
@@OPTIONS@@ \
# the current list of options related to OPT and STDOPT directives (for CMD directives)@ \
+ @@frama-c-exe@@ \
+ # shortcut defined as follow: %s@ \
@@frama-c-only@@ \
# shortcut defined as follow: %s@ \
@@frama-c@@ \
@@ -168,6 +171,7 @@ let example_msg =
# shortcut defined as follow: %s@ \
@]@ @]"
macro_default_options
+ macro_frama_c_exe
macro_frama_c_only
macro_frama_c
macro_frama_c_cmd
@@ -419,6 +423,7 @@ module Macros = struct
let default_macros = add_list
[ "PLUGIN", "" ;
"DEFAULT_OPTIONS", macro_default_options;
+ "frama-c-exe", macro_frama_c_exe;
"frama-c-only", macro_frama_c_only;
"frama-c-cmd", macro_frama_c_cmd;
"frama-c", macro_frama_c;
diff --git a/ptests/tests/cmd/README b/ptests/tests/cmd/README
new file mode 100644
index 00000000000..75d737ebce8
--- /dev/null
+++ b/ptests/tests/cmd/README
@@ -0,0 +1,3 @@
+Test suite where ./test_config contents:
+- 1 CMD
+- no OPT
diff --git a/ptests/tests/ptests_config b/ptests/tests/cmd/tests/ptests_config
similarity index 100%
rename from ptests/tests/ptests_config
rename to ptests/tests/cmd/tests/ptests_config
diff --git a/ptests/tests/test_config b/ptests/tests/cmd/tests/test_config
similarity index 100%
rename from ptests/tests/test_config
rename to ptests/tests/cmd/tests/test_config
diff --git a/ptests/tests/without-test_config/README b/ptests/tests/cmd/tests/without-test_config/README
similarity index 100%
rename from ptests/tests/without-test_config/README
rename to ptests/tests/cmd/tests/without-test_config/README
diff --git a/ptests/tests/without-test_config/config.i b/ptests/tests/cmd/tests/without-test_config/config.i
similarity index 100%
rename from ptests/tests/without-test_config/config.i
rename to ptests/tests/cmd/tests/without-test_config/config.i
diff --git a/ptests/tests/without-test_config/empty.i b/ptests/tests/cmd/tests/without-test_config/empty.i
similarity index 100%
rename from ptests/tests/without-test_config/empty.i
rename to ptests/tests/cmd/tests/without-test_config/empty.i
diff --git a/ptests/tests/without-test_config/oracle/config.0.res.oracle b/ptests/tests/cmd/tests/without-test_config/oracle/config.0.res.oracle
similarity index 100%
rename from ptests/tests/without-test_config/oracle/config.0.res.oracle
rename to ptests/tests/cmd/tests/without-test_config/oracle/config.0.res.oracle
diff --git a/ptests/tests/without-test_config/oracle/config.1.res.oracle b/ptests/tests/cmd/tests/without-test_config/oracle/config.1.res.oracle
similarity index 100%
rename from ptests/tests/without-test_config/oracle/config.1.res.oracle
rename to ptests/tests/cmd/tests/without-test_config/oracle/config.1.res.oracle
diff --git a/ptests/tests/without-test_config/oracle/config.2.res.oracle b/ptests/tests/cmd/tests/without-test_config/oracle/config.2.res.oracle
similarity index 100%
rename from ptests/tests/without-test_config/oracle/config.2.res.oracle
rename to ptests/tests/cmd/tests/without-test_config/oracle/config.2.res.oracle
diff --git a/ptests/tests/without-test_config/oracle/config.3.res.oracle b/ptests/tests/cmd/tests/without-test_config/oracle/config.3.res.oracle
similarity index 100%
rename from ptests/tests/without-test_config/oracle/config.3.res.oracle
rename to ptests/tests/cmd/tests/without-test_config/oracle/config.3.res.oracle
diff --git a/ptests/tests/without-test_config/oracle/config.4.res.oracle b/ptests/tests/cmd/tests/without-test_config/oracle/config.4.res.oracle
similarity index 100%
rename from ptests/tests/without-test_config/oracle/config.4.res.oracle
rename to ptests/tests/cmd/tests/without-test_config/oracle/config.4.res.oracle
diff --git a/ptests/tests/without-test_config/oracle/empty.res.oracle b/ptests/tests/cmd/tests/without-test_config/oracle/empty.res.oracle
similarity index 100%
rename from ptests/tests/without-test_config/oracle/empty.res.oracle
rename to ptests/tests/cmd/tests/without-test_config/oracle/empty.res.oracle
diff --git a/ptests/tests/nothing/README b/ptests/tests/nothing/README
new file mode 100644
index 00000000000..352ae03088e
--- /dev/null
+++ b/ptests/tests/nothing/README
@@ -0,0 +1,3 @@
+Test suite where ./test_config contents:
+- no CMD
+- no OPT
diff --git a/ptests/tests/nothing/tests/basic/oracle/empty.res.oracle b/ptests/tests/nothing/tests/basic/oracle/empty.res.oracle
new file mode 100644
index 00000000000..628d824bcc7
--- /dev/null
+++ b/ptests/tests/nothing/tests/basic/oracle/empty.res.oracle
@@ -0,0 +1 @@
+frama-c default-options:=-journal-disable -check -no-autoload-plugins:= empty.i
diff --git a/ptests/tests/nothing/tests/ptests_config b/ptests/tests/nothing/tests/ptests_config
new file mode 100644
index 00000000000..d8df396ade8
--- /dev/null
+++ b/ptests/tests/nothing/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= basic
--
GitLab