summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/test_runner/run_test.ml38
1 files changed, 23 insertions, 15 deletions
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 1ec2d1c8..52619c4a 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -116,20 +116,28 @@ let test_subdir backend test_name =
let () =
match Array.to_list Sys.argv with
(* Ad-hoc argument passing for now. *)
- | _exe_path :: aeneas_path :: llbc_dir :: test_name :: backend :: options ->
- let subdir = test_subdir backend test_name in
- let options = List.append (test_options backend test_name) options in
-
- let test_file_name =
+ | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options ->
+ let tests_env = { aeneas_path; llbc_dir } in
+ (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
+ let backends =
match test_name with
- | "betree_main-special" -> "betree_main"
- | _ -> test_name
+ | "betree_main-special" -> [ "fstar" ]
+ | _ -> [ "coq"; "lean"; "fstar" ]
in
- run_test { aeneas_path; llbc_dir }
- {
- name = test_file_name;
- backend;
- subdir;
- extra_aeneas_options = options;
- }
- | _ -> ()
+ List.iter
+ (fun backend ->
+ let subdir = test_subdir backend test_name in
+ let extra_aeneas_options =
+ List.append (test_options backend test_name) options
+ in
+ let test_file_name =
+ match test_name with
+ | "betree_main-special" -> "betree_main"
+ | _ -> test_name
+ in
+ let test_case =
+ { name = test_file_name; backend; subdir; extra_aeneas_options }
+ in
+ run_test tests_env test_case)
+ backends
+ | _ -> failwith "Incorrect options passed to test runner"