summaryrefslogtreecommitdiff
path: root/flake.nix
diff options
context:
space:
mode:
authorNadrieril2024-05-27 11:22:37 +0200
committerNadrieril2024-05-27 14:40:34 +0200
commit9c09789c26dd8142b8a29b42e250a685aa983e58 (patch)
tree0ba6a9de8a5aa7c3c037022c0446ed2bf772227f /flake.nix
parentaee6dc227c4ed041bbbae7cf38729a4b1a3a6869 (diff)
runner: Support negative tests
Diffstat (limited to '')
-rw-r--r--flake.nix12
1 files changed, 7 insertions, 5 deletions
diff --git a/flake.nix b/flake.nix
index 68378954..f1a2258a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -118,17 +118,19 @@
export CHARON_EXE=${charon.packages.${system}.charon}/bin/charon
export TEST_RUNNER_EXE=${test_runner}/bin/test_runner
- mkdir llbc
- export LLBC_DIR=llbc
- # Copy over the llbc file we can't generate ourselves.
- cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR
-
# Copy the tests
cp -r tests tests-copy
make clean-generated-aeneas
+ mkdir tests/llbc
+ export LLBC_DIR=tests/llbc
+ # Copy over the llbc file we can't generate ourselves.
+ cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR
+
# Run the tests with extra sanity checks enabled
IN_CI=1 make test-all -j $NIX_BUILD_CORES
+ # Clean generated llbc files so we don't compare them.
+ rm -r tests/llbc
# Check that there are no differences between the generated tests
# and the original tests