summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Makefile33
-rw-r--r--tests/test_runner/run_test.ml38
2 files changed, 28 insertions, 43 deletions
diff --git a/Makefile b/Makefile
index 0ceaa558..506dec5e 100644
--- a/Makefile
+++ b/Makefile
@@ -117,7 +117,7 @@ test: build-dev test-all
test-all: \
test-arrays \
test-betree_main \
- tfstar-betree_main-special \
+ test-betree_main-special \
test-bitwise \
test-constants \
test-demo \
@@ -154,9 +154,6 @@ else
CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$*
endif
-# The command to run Aeneas on the proper llbc file
-AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS)
-
# Generic rules to extract the LLBC from a rust file
# We use the rules in Charon's Makefile to generate the .llbc files: the options
# vary with the test files.
@@ -164,34 +161,14 @@ AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKE
gen-llbc-%:
$(CHARON_CMD)
-# Generic rules to test the translation of an LLBC file.
+# Translate the given llbc file to available backends. The test runner decides
+# which backends to use and sets test-specific options.
.PHONY: test-%
test-%: FILE = $*
-test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
+test-%: gen-llbc-%
+ $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(OPTIONS)
echo "# Test $* done"
-.PHONY: tfstar-%
-tfstar-%: BACKEND := fstar
-tfstar-%:
- $(AENEAS_CMD)
-
-.PHONY: tcoq-%
-tcoq-%: BACKEND := coq
-tcoq-%:
- $(AENEAS_CMD)
-
-.PHONY: tlean-%
-tlean-%: BACKEND := lean
-tlean-%:
- $(AENEAS_CMD)
-
-# TODO: reactivate HOL4 once traits are parameterized by their associated types
-.PHONY: thol4-%
-thol4-%: BACKEND := hol4
-thol4-%:
- echo Ignoring the $* test for HOL4
-# $(AENEAS_CMD)
-
# Nix - TODO: add the lean tests
.PHONY: nix
nix:
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"