diff options
author | Nadrieril | 2024-05-27 11:22:37 +0200 |
---|---|---|
committer | Nadrieril | 2024-05-27 14:40:34 +0200 |
commit | 9c09789c26dd8142b8a29b42e250a685aa983e58 (patch) | |
tree | 0ba6a9de8a5aa7c3c037022c0446ed2bf772227f /flake.nix | |
parent | aee6dc227c4ed041bbbae7cf38729a4b1a3a6869 (diff) |
runner: Support negative tests
Diffstat (limited to '')
-rw-r--r-- | flake.nix | 12 |
1 files changed, 7 insertions, 5 deletions
@@ -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 |