diff options
Diffstat (limited to '')
-rw-r--r-- | tests/test_runner/run_test.ml | 15 |
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 -> [] |