diff options
author | Son HO | 2024-06-06 09:15:22 +0200 |
---|---|---|
committer | GitHub | 2024-06-06 09:15:22 +0200 |
commit | 961cc880311aed3319b08755c5a43816e2490d7f (patch) | |
tree | 80cc3d5db32d7198adbdf89e516484dc01e58186 /tests/test_runner/run_test.ml | |
parent | baa0771885546816461e063131162b94c6954d86 (diff) | |
parent | a4dd9fe0598328976862868097f59207846d865c (diff) |
Merge pull request #233 from AeneasVerif/son/borrow-check
Add a `-borrow-check` option
Diffstat (limited to 'tests/test_runner/run_test.ml')
-rw-r--r-- | tests/test_runner/run_test.ml | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index c17c17be..0c3426c5 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -50,25 +50,35 @@ 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 + (* 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 |