summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-06-05 16:48:08 +0200
committerSon Ho2024-06-05 16:48:08 +0200
commitc6ba96bf0723fd46432d73e52eaf6b0859c75fa8 (patch)
tree93eeb9a225b45987e9da7a49b1295153702ee569
parent0a0ab7c0e159e736a3187b8121d106ee76651f57 (diff)
Update the test runner
-rw-r--r--tests/test_runner/run_test.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 9bdfe81d..0c3426c5 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -72,10 +72,13 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
(* Build the command *)
let args = [ env.aeneas_path; input_file ] @ dest_command @ backend_command in
+ (* If we target a specific backend and the test is known to fail, we abort
+ on error so as not to generate any files *)
let abort_on_error =
match action with
| Skip | Normal -> []
- | KnownFailure -> [ "-abort-on-error" ]
+ | KnownFailure ->
+ if backend = Backend.BorrowCheck then [] else [ "-abort-on-error" ]
in
let args = List.concat [ args; aeneas_options; abort_on_error ] in
let cmd = Command.make args in