Skip to content
Snippets Groups Projects
Commit 235d6ea6 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[ci] make sure to always enable tests

parent f9354e13
No related branches found
No related tags found
No related merge requests found
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
mk_tests { mk_tests {
tests-name = "default-config-tests"; tests-name = "default-config-tests";
tests-command = '' 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 dune build -j1 --display short @ptests_config
''; '';
} }
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
mk_tests { mk_tests {
tests-name = "e-acsl-tests"; tests-name = "e-acsl-tests";
tests-command = '' 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 dune build -j1 --display short @src/plugins/e-acsl/tests/ptests
''; '';
} }
...@@ -10,6 +10,6 @@ let tvalue = " @tests/value/" + ptests ; in ...@@ -10,6 +10,6 @@ let tvalue = " @tests/value/" + ptests ; in
mk_tests { mk_tests {
tests-name = eva-tests ; tests-name = eva-tests ;
tests-command = '' 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" ; dune build -j1 --display short'' + tbuiltins + tfloat + tidct + tvalue + "\n" ;
} }
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
mk_tests { mk_tests {
tests-name = "full-tests"; tests-name = "full-tests";
tests-command = '' 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 dune build @ptests
''; '';
has-wp-proofs = true ; has-wp-proofs = true ;
......
...@@ -129,7 +129,7 @@ stdenvNoCC.mkDerivation rec { ...@@ -129,7 +129,7 @@ stdenvNoCC.mkDerivation rec {
checkPhase = '' checkPhase = ''
runHook preCheck 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 dune build -j1 --display short @ptests_config
''; '';
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
mk_tests { mk_tests {
tests-name = "kernel-tests"; tests-name = "kernel-tests";
tests-command = '' tests-command = ''
dune exec -- frama-c-ptests tests dune exec -- frama-c-ptests -never-disabled tests
dune build -j1 --display short \ dune build -j1 --display short \
@tests/cil/ptests \ @tests/cil/ptests \
@tests/compliance/ptests \ @tests/compliance/ptests \
......
...@@ -8,7 +8,7 @@ ...@@ -8,7 +8,7 @@
# - tests-command (mandatory): # - tests-command (mandatory):
# The tests command to execute, generally something like: # 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 # dune build -j1 --display short @src/plugins/e-acsl/tests/ptests
# '' # ''
# #
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
mk_tests { mk_tests {
tests-name = "plugins-tests"; tests-name = "plugins-tests";
tests-command = '' 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 \ dune build -j1 --display short \
@tests/callgraph/ptests \ @tests/callgraph/ptests \
@tests/constant_propagation/ptests \ @tests/constant_propagation/ptests \
......
...@@ -6,7 +6,7 @@ let mk_tests_distrib = mk_tests.override { ...@@ -6,7 +6,7 @@ let mk_tests_distrib = mk_tests.override {
mk_tests_distrib { mk_tests_distrib {
tests-name = "src-distrib-tests"; tests-name = "src-distrib-tests";
tests-command = '' 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 dune build -j1 --display short @ptests_config
''; '';
} }
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
mk_tests { mk_tests {
tests-name = "wp-tests"; tests-name = "wp-tests";
tests-command = '' 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 dune build -j1 --display short @src/plugins/wp/tests/ptests
''; '';
has-wp-proofs = true ; has-wp-proofs = true ;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment