diff --git a/nix/default-config-tests.nix b/nix/default-config-tests.nix
index 5ba96c479ab83caf4cfae47b0318d0e517544c78..04f0b1bdb3dd8fc6492d23338b6dc90b1d706ba3 100644
--- a/nix/default-config-tests.nix
+++ b/nix/default-config-tests.nix
@@ -3,7 +3,7 @@
mk_tests {
tests-name = "default-config-tests";
tests-command = ''
- dune exec -- frama-c-ptests tests src/plugins/*/tests
+ dune exec -- frama-c-ptests -never-disabled tests src/plugins/*/tests
dune build -j1 --display short @ptests_config
'';
}
diff --git a/nix/e-acsl-tests.nix b/nix/e-acsl-tests.nix
index 7128d8d4a33a0b740c9fc78be436b4db41c10ae5..79c82e91a45bce3690396b3a3883d6e4d01aa832 100644
--- a/nix/e-acsl-tests.nix
+++ b/nix/e-acsl-tests.nix
@@ -3,7 +3,7 @@
mk_tests {
tests-name = "e-acsl-tests";
tests-command = ''
- dune exec -- frama-c-ptests tests src/plugins/e-acsl/tests
+ dune exec -- frama-c-ptests -never-disabled tests src/plugins/e-acsl/tests
dune build -j1 --display short @src/plugins/e-acsl/tests/ptests
'';
}
diff --git a/nix/eva-tests.nix b/nix/eva-tests.nix
index 41a12edd7b5734107ed0b9e29af3ea6f060fe618..9ee646931383a5b861e0bec28a5ac7e3c869ffcf 100644
--- a/nix/eva-tests.nix
+++ b/nix/eva-tests.nix
@@ -10,6 +10,6 @@ let tvalue = " @tests/value/" + ptests ; in
mk_tests {
tests-name = eva-tests ;
tests-command = ''
- dune exec -- frama-c-ptests tests
+ dune exec -- frama-c-ptests -never-disabled tests
dune build -j1 --display short'' + tbuiltins + tfloat + tidct + tvalue + "\n" ;
}
diff --git a/nix/full-tests.nix b/nix/full-tests.nix
index 511d04ce19ef5fc2bff7198e2e1e4f8b7d19397a..670aebbadc892b8fbd7ba674bfab64ec8f01618d 100644
--- a/nix/full-tests.nix
+++ b/nix/full-tests.nix
@@ -5,7 +5,7 @@
mk_tests {
tests-name = "full-tests";
tests-command = ''
- dune exec -- frama-c-ptests tests src/plugins/*/tests
+ dune exec -- frama-c-ptests -never-disabled tests src/plugins/*/tests
dune build @ptests
'';
has-wp-proofs = true ;
diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix
index 637d1b86b89fec34f929dc779ab58b141a836cb9..46f974137fc5bf1bb35de1fa2129e98979376e2e 100644
--- a/nix/internal-tests.nix
+++ b/nix/internal-tests.nix
@@ -129,7 +129,7 @@ stdenvNoCC.mkDerivation rec {
checkPhase = ''
runHook preCheck
- dune exec -- frama-c-ptests tests src/plugins/*/tests
+ dune exec -- frama-c-ptests -never-disabled tests src/plugins/*/tests
dune build -j1 --display short @ptests_config
'';
diff --git a/nix/kernel-tests.nix b/nix/kernel-tests.nix
index 03b05e9c2ab553a727c28a2e1badb52b57b21e7d..4b99a89ceca490cf47203fd76143a79885ff10a2 100644
--- a/nix/kernel-tests.nix
+++ b/nix/kernel-tests.nix
@@ -3,7 +3,7 @@
mk_tests {
tests-name = "kernel-tests";
tests-command = ''
- dune exec -- frama-c-ptests tests
+ dune exec -- frama-c-ptests -never-disabled tests
dune build -j1 --display short \
@tests/cil/ptests \
@tests/compliance/ptests \
diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix
index 4241026860bcff77cdc51a27b028e3a258de6257..42f7f396a65cdd2d1f48be36b34d858594f0f4d8 100644
--- a/nix/mk_tests.nix
+++ b/nix/mk_tests.nix
@@ -8,7 +8,7 @@
# - tests-command (mandatory):
# The tests command to execute, generally something like:
# ''
-# dune exec -- frama-c-ptests tests src/plugins/e-acsl/tests
+# dune exec -- frama-c-ptests -never-disabled tests src/plugins/e-acsl/tests
# dune build -j1 --display short @src/plugins/e-acsl/tests/ptests
# ''
#
diff --git a/nix/plugins-tests.nix b/nix/plugins-tests.nix
index 6a051fe20ed3ba227b800ac941733c932e9c505e..cbbeb33d9d2fb3eb6dc8438d4cc9d0e746720061 100644
--- a/nix/plugins-tests.nix
+++ b/nix/plugins-tests.nix
@@ -3,7 +3,7 @@
mk_tests {
tests-name = "plugins-tests";
tests-command = ''
- dune exec -- frama-c-ptests tests src/plugins/*/tests
+ dune exec -- frama-c-ptests -never-disabled tests src/plugins/*/tests
dune build -j1 --display short \
@tests/callgraph/ptests \
@tests/constant_propagation/ptests \
diff --git a/nix/src-distrib-tests.nix b/nix/src-distrib-tests.nix
index c1a52472721dbaded752b7007d2cd94ddef5943d..6655a194c4c6f36aad1c92c81b8da5b2791ca13d 100644
--- a/nix/src-distrib-tests.nix
+++ b/nix/src-distrib-tests.nix
@@ -6,7 +6,7 @@ let mk_tests_distrib = mk_tests.override {
mk_tests_distrib {
tests-name = "src-distrib-tests";
tests-command = ''
- dune exec -- frama-c-ptests tests src/plugins/*/tests
+ dune exec -- frama-c-ptests -never-disabled tests src/plugins/*/tests
dune build -j1 --display short @ptests_config
'';
}
diff --git a/nix/wp-tests.nix b/nix/wp-tests.nix
index c431e8fe8072f253db36402f1c2888d5ff6b2186..86c9114a8aab2a2c645179f2b400b6db89b8b9ed 100644
--- a/nix/wp-tests.nix
+++ b/nix/wp-tests.nix
@@ -3,7 +3,7 @@
mk_tests {
tests-name = "wp-tests";
tests-command = ''
- dune exec -- frama-c-ptests src/plugins/wp/tests
+ dune exec -- frama-c-ptests -never-disabled src/plugins/wp/tests
dune build -j1 --display short @src/plugins/wp/tests/ptests
'';
has-wp-proofs = true ;
diff --git a/tools/ptests/ptests.ml b/tools/ptests/ptests.ml
index 13254fdc71308c2a8615f2d77739283e874eb773..70b15a30939e721576038a52be0c196560acea76 100644
--- a/tools/ptests/ptests.ml
+++ b/tools/ptests/ptests.ml
@@ -159,6 +159,8 @@ let macro_frama_c_cmd = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@"
let macro_frama_c = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@"
let macro_frama_c_share = ref "../../../../install/default/share/frama-c/share"
+let never_disabled = ref false
+
let default_toplevel = ref "@frama-c@"
(** the files in [suites] whose name matches
@@ -314,6 +316,9 @@ let argspec =
("-macro-frama-c-share", Arg.String (fun s -> macro_frama_c_share := s),
" <value> Set the @FRAMAC_SHARE@ macro (defaults to "^ !macro_frama_c_share ^")");
+ ("-never-disabled", Arg.Set never_disabled,
+ " disable the generation of the enabled_if dune field: tests are never disabled (for CI purpose)");
+
("-dune-alias", Arg.String (fun s -> default_dune_alias := s),
" <name> Use @<name> as dune alias to exectute tests (defaults to "^ !default_dune_alias ^")");
]
@@ -1259,11 +1264,16 @@ let pp_list_deps fmt l =
(* kind={env_var,source_tree,glob_files,...} *)
Format.fprintf fmt " (%s %S)" kind deps) l
-let pp_enabled_if fmt deps =
+let pp_enabled_if_content fmt deps =
Format.fprintf fmt "(and %s%a)"
(Option.value ~default:"true" deps.enabled_if)
Fmt.(list (var_libavailable framac_plugin)) (list_of_deps deps.load_plugin)
+let pp_enabled_if fmt deps =
+ Format.fprintf fmt "%s(enabled_if %a)"
+ (if !never_disabled then ";" else "")
+ pp_enabled_if_content deps
+
let pp_command_deps fmt command =
Format.fprintf fmt "%S %a (package frama-c) %a"
(* the test file *)
@@ -1408,7 +1418,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(alias %S)\n \
(targets %S %S %a %a)\n \
(deps %S %S %S %a %a)\n \
- (enabled_if %a)\n\
+ %a\n\
(action (run %s %S %S %a))\n\
)@."
(* rule: *)
@@ -1451,7 +1461,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(alias %S)\n \
(targets %S %S %a %a)\n \
(deps %a)\n \
- (enabled_if %a)\n\
+ %a\n\
(action (with-stderr-to %S (with-stdout-to %S (%s (system %S)))))\n\
)@."
(* rule: *)
@@ -1478,7 +1488,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule ; FILTER %s #%d OF TEST FILE %S\n \
(deps %S)
- (enabled_if %a)\n\
+ %a\n\
(action (with-stdout-to %S (with-accepted-exit-codes (or 0 1 2 125) (system %S))))\n\
)@."
(* rule: *)
@@ -1498,7 +1508,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule ; COMPARE TARGET #%d OF TEST #%d FOR TEST FILE %S\n \
(alias %s)\n \
- (enabled_if %a)\n\
+ %a\n\
(action (diff %S %S))\n\
)@."
(* rule: *)
@@ -1515,7 +1525,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
"(rule ; REPRODUCE TEST #%d OF TEST FILE %S\n \
(alias %S)\n \
(deps %a (universe))\n \
- (enabled_if %a)\n\
+ %a\n\
(action (%s (system %S)))\n\
)@."
(* rule: *)
@@ -1534,7 +1544,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
"(rule ; SHOW TEST COMMAND #%d OF TEST FILE %S\n \
(alias %S)\n \
(deps %a (universe))\n \
- (enabled_if %a)\n\
+ %a\n\
(action (system %S))\n\
)@."
(* rule: *)
@@ -1553,7 +1563,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule\n \
(alias %S)\n \
- (enabled_if %a)\n\
+ %a\n\
(action (diff %S %S))\n\
)@."
(* alias: *)
@@ -1566,7 +1576,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule\n \
(alias %S)\n \
- (enabled_if %a)\n\
+ %a\n\
(action (diff %S %S))\n\
)@."
(* alias: *)
@@ -1579,7 +1589,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(alias (name %S)\n \
(deps (alias %S))\n \
- (enabled_if %a)\n\
+ %a\n\
)@."
(ptests_alias ~env)
diff_alias
@@ -1698,7 +1708,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
(alias %s)\n \
(deps %a %a)\n \
(targets %a %a)\n \
- (enabled_if %a)\n\
+ %a\n\
(action (run %s %%{dep:%s} %S))\n\
)@."
(* rule: *)
@@ -1732,7 +1742,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
(alias %s)\n \
(deps (package frama-c)%a)\n \
(targets %a %a)\n \
- (enabled_if %a)\n\
+ %a\n\
(action (system %S))\n\
)@."
(* rule: *)
@@ -1756,7 +1766,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
"(rule ; SHOW EXECNOW COMMAND #%d OF TEST FILE %S\n \
(alias %s)\n \
(deps %a (universe))\n \
- (enabled_if %a)\n\
+ %a\n\
(action (system %S))\n\
)@."
(* rule: *)
@@ -1774,7 +1784,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
Format.fprintf result_fmt
"(rule ; COMPARE TARGET #%d OF EXECNOW #%d FOR TEST FILE %S\n \
(alias %s)\n \
- (enabled_if %a)\n\
+ %a\n\
(action (diff %S %S))\n\
)@."
(* rule: *)