diff --git a/ptests/Makefile b/ptests/Makefile index 8dccd5f2574a697356a1769c19c19f35dbf3bca8..2a5a585305aa906b6435f3eb97b2be7285586225 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 1bd64804faa367d18110755779cbf8e9ebd8a92c..d73047c9f65a56c2699db6d9b367adc9e8961797 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 0000000000000000000000000000000000000000..75d737ebce83a54fed8b762232c5d91d3ad1d848 --- /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 0000000000000000000000000000000000000000..352ae03088e977994ea6baee36788134ff8c2742 --- /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 0000000000000000000000000000000000000000..628d824bcc72487d0ad5d112e8c641821542873c --- /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 0000000000000000000000000000000000000000..d8df396ade8c39ec6e0e14895457f5878d208d07 --- /dev/null +++ b/ptests/tests/nothing/tests/ptests_config @@ -0,0 +1 @@ +DEFAULT_SUITES= basic