From 068149ef5e0cc56c41992d01ef2fe41c9f3d6d5d Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 27 Oct 2020 12:08:43 +0100
Subject: [PATCH] [Ptests] fixes the default CMD to be used
---
ptests/Makefile | 13 +++++++++
ptests/ptests.ml | 29 ++++++++++++-------
ptests/tests/.gitignore | 1 +
ptests/tests/ptests_config | 1 +
ptests/tests/test_config | 7 +++++
ptests/tests/without-test_config/README | 2 ++
ptests/tests/without-test_config/config.i | 12 ++++++++
ptests/tests/without-test_config/empty.i | 2 ++
.../oracle/config.0.res.oracle | 1 +
.../oracle/config.1.res.oracle | 1 +
.../oracle/config.2.res.oracle | 1 +
.../oracle/config.3.res.oracle | 1 +
.../oracle/config.4.res.oracle | 1 +
.../oracle/empty.res.oracle | 1 +
14 files changed, 62 insertions(+), 11 deletions(-)
create mode 100644 ptests/Makefile
create mode 100644 ptests/tests/.gitignore
create mode 100644 ptests/tests/ptests_config
create mode 100644 ptests/tests/test_config
create mode 100644 ptests/tests/without-test_config/README
create mode 100644 ptests/tests/without-test_config/config.i
create mode 100644 ptests/tests/without-test_config/empty.i
create mode 100644 ptests/tests/without-test_config/oracle/config.0.res.oracle
create mode 100644 ptests/tests/without-test_config/oracle/config.1.res.oracle
create mode 100644 ptests/tests/without-test_config/oracle/config.2.res.oracle
create mode 100644 ptests/tests/without-test_config/oracle/config.3.res.oracle
create mode 100644 ptests/tests/without-test_config/oracle/config.4.res.oracle
create mode 100644 ptests/tests/without-test_config/oracle/empty.res.oracle
diff --git a/ptests/Makefile b/ptests/Makefile
new file mode 100644
index 00000000000..8dccd5f2574
--- /dev/null
+++ b/ptests/Makefile
@@ -0,0 +1,13 @@
+.PHONY: run-tests clean-tests purge-tests tests
+
+purge-tests:
+ find tests -name dune | grep -e "oracle.*/\|result.*/" | xargs --no-run-if-empty rm
+
+clean-tests: purge-tests
+ rm -rf _build/default/ptests/tests
+
+run-tests: purge-tests
+ dune exec -- ../ptests/ptests.exe ./tests
+ dune build @tests/ptests
+
+tests: run-tests
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 35d1c5c75d1..24b1e28ffaa 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -517,7 +517,7 @@ end = struct
let test_file_regexp = ".*\\.\\(c\\|i\\)$"
let default_toplevel = "@frama-c@ @OPTIONS@"
- let default_command = {toplevel=default_toplevel; opts=""; macros=Macros.default_macros (); logs=[]; timeout=""}
+ let default_commands config = [ { toplevel=config.dc_default_toplevel; opts=""; macros=config.dc_macros; logs=[]; timeout=""} ]
let default_config () =
{ dc_test_regexp = test_file_regexp ;
dc_macros = Macros.default_macros ();
@@ -529,7 +529,7 @@ end = struct
dc_load_module = [];
dc_filter = None ;
dc_default_toplevel = default_toplevel;
- dc_commands = [ default_command ];
+ dc_commands = [ ];
dc_dont_run = false;
dc_framac = true;
dc_default_log = [];
@@ -650,7 +650,7 @@ end = struct
(* the default toplevel for the current level of options. *)
let current_default_toplevel = ref default_toplevel
let current_default_log = ref []
- let current_default_cmds = ref [ default_command ]
+ let current_default_cmds = ref [ ]
let config_options =
[ "CMD",
@@ -681,7 +681,9 @@ end = struct
(fun command ->
{ command with opts= make_custom_opts command.opts s ;
timeout= current.dc_timeout})
- !current_default_cmds
+ (if !current_default_cmds = [] then
+ default_commands current
+ else !current_default_cmds)
in
{ current with dc_commands = new_top @ current.dc_commands;
dc_default_log = !current_default_log @
@@ -808,13 +810,18 @@ end = struct
ignore (scan_directives dir scan_buffer default);
scan_config ()))
in
- try
- let options = scan_config () in
- Scanf.Scanning.close_in scan_buffer;
- options
- with End_of_file | Scanf.Scan_failure _ ->
- Scanf.Scanning.close_in scan_buffer;
- default
+ let config =
+ try
+ let options = scan_config () in
+ Scanf.Scanning.close_in scan_buffer;
+ options
+ with End_of_file | Scanf.Scan_failure _ ->
+ Scanf.Scanning.close_in scan_buffer;
+ default
+ in
+ if config.dc_commands = [] && config.dc_framac
+ then { config with dc_commands = default_commands config }
+ else config
end else
(* if the file has disappeared, don't try to run it... *)
{ default with dc_dont_run = true }
diff --git a/ptests/tests/.gitignore b/ptests/tests/.gitignore
new file mode 100644
index 00000000000..cc129cb16f5
--- /dev/null
+++ b/ptests/tests/.gitignore
@@ -0,0 +1 @@
+**/dune
diff --git a/ptests/tests/ptests_config b/ptests/tests/ptests_config
new file mode 100644
index 00000000000..090ea442919
--- /dev/null
+++ b/ptests/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= without-test_config
diff --git a/ptests/tests/test_config b/ptests/tests/test_config
new file mode 100644
index 00000000000..c363004b9cf
--- /dev/null
+++ b/ptests/tests/test_config
@@ -0,0 +1,7 @@
+MACRO: test_config1 tests/test_config1
+MACRO: test_config2 tests/test_config2
+
+CMD: echo tests/test_config:CMD @test_config1@ @test_config2@ @test_config3@ @OPTIONS@
+
+MACRO: test_config2 tests/test_config2-redefined
+MACRO: test_config3 tests/test_config3
diff --git a/ptests/tests/without-test_config/README b/ptests/tests/without-test_config/README
new file mode 100644
index 00000000000..c0ea4803c81
--- /dev/null
+++ b/ptests/tests/without-test_config/README
@@ -0,0 +1,2 @@
+A test suite in a directory that have no ./test_config file.
+The ../test_config has to be used as if it was in this directory.
diff --git a/ptests/tests/without-test_config/config.i b/ptests/tests/without-test_config/config.i
new file mode 100644
index 00000000000..aa9229157e3
--- /dev/null
+++ b/ptests/tests/without-test_config/config.i
@@ -0,0 +1,12 @@
+/* run.config
+OPT: test#0
+STDOPT: +"test#1"
+
+MACRO: test_config3 tests/test_config3-redef
+OPT: test#2
+STDOPT: #"test#3"
+
+MACRO: test_config3 tests/test_config3-redef
+CMD: echo CMD @test_config1@ @test_config2@ @test_config3@ @OPTIONS@
+OPT: test#4
+*/
diff --git a/ptests/tests/without-test_config/empty.i b/ptests/tests/without-test_config/empty.i
new file mode 100644
index 00000000000..75a70dfea46
--- /dev/null
+++ b/ptests/tests/without-test_config/empty.i
@@ -0,0 +1,2 @@
+// Test with no file ./test_config nor run.config directive
+// Checks that the test will use the CMD directive defined into ../test_config
diff --git a/ptests/tests/without-test_config/oracle/config.0.res.oracle b/ptests/tests/without-test_config/oracle/config.0.res.oracle
new file mode 100644
index 00000000000..2bc0e2c9975
--- /dev/null
+++ b/ptests/tests/without-test_config/oracle/config.0.res.oracle
@@ -0,0 +1 @@
+tests/test_config:CMD tests/test_config1 tests/test_config2 tests/test_config3 test#0
diff --git a/ptests/tests/without-test_config/oracle/config.1.res.oracle b/ptests/tests/without-test_config/oracle/config.1.res.oracle
new file mode 100644
index 00000000000..b045b11c2a5
--- /dev/null
+++ b/ptests/tests/without-test_config/oracle/config.1.res.oracle
@@ -0,0 +1 @@
+tests/test_config:CMD tests/test_config1 tests/test_config2 tests/test_config3 test#1
diff --git a/ptests/tests/without-test_config/oracle/config.2.res.oracle b/ptests/tests/without-test_config/oracle/config.2.res.oracle
new file mode 100644
index 00000000000..e4f134b7408
--- /dev/null
+++ b/ptests/tests/without-test_config/oracle/config.2.res.oracle
@@ -0,0 +1 @@
+tests/test_config:CMD tests/test_config1 tests/test_config2 tests/test_config3-redef test#2
diff --git a/ptests/tests/without-test_config/oracle/config.3.res.oracle b/ptests/tests/without-test_config/oracle/config.3.res.oracle
new file mode 100644
index 00000000000..11a17c14edd
--- /dev/null
+++ b/ptests/tests/without-test_config/oracle/config.3.res.oracle
@@ -0,0 +1 @@
+tests/test_config:CMD tests/test_config1 tests/test_config2 tests/test_config3-redef test#3
diff --git a/ptests/tests/without-test_config/oracle/config.4.res.oracle b/ptests/tests/without-test_config/oracle/config.4.res.oracle
new file mode 100644
index 00000000000..4780a4e73d3
--- /dev/null
+++ b/ptests/tests/without-test_config/oracle/config.4.res.oracle
@@ -0,0 +1 @@
+CMD tests/test_config1 tests/test_config2-redefined tests/test_config3-redef test#4
diff --git a/ptests/tests/without-test_config/oracle/empty.res.oracle b/ptests/tests/without-test_config/oracle/empty.res.oracle
new file mode 100644
index 00000000000..1aa289856c0
--- /dev/null
+++ b/ptests/tests/without-test_config/oracle/empty.res.oracle
@@ -0,0 +1 @@
+tests/test_config:CMD tests/test_config1 tests/test_config2 tests/test_config3
--
GitLab