From 9c09789c26dd8142b8a29b42e250a685aa983e58 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 11:22:37 +0200
Subject: runner: Support negative tests

---
 flake.nix | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'flake.nix')

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
-- 
cgit v1.2.3