summaryrefslogtreecommitdiff
path: root/tests/test_runner/run_test.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/test_runner/run_test.ml15
1 files changed, 11 insertions, 4 deletions
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index c17c17be..9bdfe81d 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -50,21 +50,28 @@ end
(* Run Aeneas on a specific input with the given options *)
let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
let backend_str = Backend.to_string backend in
+ let backend_command = Backend.to_command backend in
let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
let output_file =
Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
in
+
let per_backend = Backend.Map.find backend case.per_backend in
let subdir = per_backend.subdir in
let check_output = per_backend.check_output in
let aeneas_options = per_backend.aeneas_options in
let action = per_backend.action in
- let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in
+ (* No destination directory if we borrow-check *)
+ let dest_command =
+ match backend with
+ | Backend.BorrowCheck -> []
+ | _ ->
+ let subdir = match subdir with None -> [] | Some x -> [ x ] in
+ [ "-dest"; concat_path ([ env.dest_dir; backend_str ] @ subdir) ]
+ in
(* Build the command *)
- let args =
- [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ]
- in
+ let args = [ env.aeneas_path; input_file ] @ dest_command @ backend_command in
let abort_on_error =
match action with
| Skip | Normal -> []