diff options
| author | Nadrieril | 2024-05-22 18:57:19 +0200 |
|---|---|---|
| committer | Guillaume Boisseau | 2024-05-24 14:24:38 +0200 |
| commit | 6ae8cde046530371345863f04d84be32b2a757bf (patch) | |
| tree | a76277d0c6d94e2ed667d14330918ceb00dd0587 /tests | |
| parent | 6f14e8c699169aa11ea9c106f8cae1ba593569d0 (diff) | |
Move the subdirectory selection to the test runner
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/test_runner/run_test.ml | 29 |
1 files changed, 26 insertions, 3 deletions
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 379abe04..52ff7276 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -3,9 +3,32 @@ let concat_path = List.fold_left Filename.concat "" let () = match Array.to_list Sys.argv with (* Ad-hoc argument passing for now. *) - | _exe_path :: aeneas_path :: tests_dir :: test_name :: subdir :: backend - :: options -> - let input_file = concat_path [ tests_dir; "llbc"; test_name ] ^ ".llbc" in + | _exe_path :: aeneas_path :: tests_dir :: test_name :: backend :: options -> + (* Reproduces the file layout that was set by the Makefile. FIXME: cleanup *) + let subdir = + match (backend, test_name) with + | "lean", "demo" -> "Demo" + | "lean", _ -> "." + | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name + | _, "betree_main" -> "betree" + | _, "betree_main-special" -> "betree_back_stateful" + | _, "hashmap_main" -> "hashmap_on_disk" + | "hol4", _ -> "misc-" ^ test_name + | ( _, + ( "bitwise" | "constants" | "external" | "loops" + | "no_nested_borrows" | "paper" | "polonius_list" ) ) -> + "misc" + | _ -> test_name + in + + let test_file_name = + match test_name with + | "betree_main-special" -> "betree_main" + | _ -> test_name + in + let input_file = + concat_path [ tests_dir; "llbc"; test_file_name ] ^ ".llbc" + in let dest_dir = concat_path [ "tests"; backend; subdir ] in let args = [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |] |