diff --git a/ptests/Makefile b/ptests/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..8dccd5f2574a697356a1769c19c19f35dbf3bca8
--- /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 35d1c5c75d1a8a75a22c256ed2e5a2a010e5bf40..24b1e28ffaa581a4c39f2c8b38133ff83404c4e5 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 0000000000000000000000000000000000000000..cc129cb16f5d6dfdc679d5fb58ea08837ae58cb6
--- /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 0000000000000000000000000000000000000000..090ea4429196560292b06cc7f13bd76e925920a1
--- /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 0000000000000000000000000000000000000000..c363004b9cf6267bfe992f5c5d938efa9447be16
--- /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 0000000000000000000000000000000000000000..c0ea4803c819e7d30b3896cfe032b66b1a24dafd
--- /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 0000000000000000000000000000000000000000..aa9229157e38669a925c850f09487d94768b0a2c
--- /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 0000000000000000000000000000000000000000..75a70dfea46b9e7c4760cd77c4c1f2cd702ea2e4
--- /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 0000000000000000000000000000000000000000..2bc0e2c997568fb471c3d09fcf502453f61aabb9
--- /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 0000000000000000000000000000000000000000..b045b11c2a563e4f57abad8414af77eadb71daf3
--- /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 0000000000000000000000000000000000000000..e4f134b7408f35967d1a24741bfefb2f91a13d3b
--- /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 0000000000000000000000000000000000000000..11a17c14edd44d5015fc9bf4c05da1bcf81336e7
--- /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 0000000000000000000000000000000000000000..4780a4e73d39fcfed2cfaf81dfa80d8a0fea69cf
--- /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 0000000000000000000000000000000000000000..1aa289856c068eae730b69de6b55b11991724e64
--- /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