diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 55 | ||||
| -rw-r--r-- | tests/test_runner/run_test.ml | 29 |
2 files changed, 28 insertions, 56 deletions
@@ -37,8 +37,6 @@ OPTIONS ?= CHARON_TEST_DIR ?= $(CHARON_HOME)/tests # The options with which to call Charon CHARON_OPTIONS = -# The directory in which to extract the result of the translation -SUBDIR := #################################### # The rules @@ -157,56 +155,7 @@ 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) "$(SUBDIR)" $(BACKEND) $(OPTIONS) - -# Subdirs -test-arrays: SUBDIR := arrays -tlean-arrays: SUBDIR := - -test-betree_main: SUBDIR := betree -tlean-betree_main: SUBDIR := - -ctest-test-betree_main: SUBDIR := betree_back_stateful - -test-bitwise: SUBDIR := misc -tlean-bitwise: SUBDIR := -thol4-bitwise: SUBDIR := misc-bitwise - -test-constants: SUBDIR := misc -tlean-constants: SUBDIR := -thol4-constants: SUBDIR := misc-constants - -test-demo: SUBDIR := demo -tlean-demo: SUBDIR := Demo - -test-external: SUBDIR := misc -tlean-external: SUBDIR := -thol4-external: SUBDIR := misc-external - -test-hashmap: SUBDIR := hashmap -tlean-hashmap: SUBDIR := - -test-hashmap_main: SUBDIR := hashmap_on_disk -tlean-hashmap_main: SUBDIR := - -test-loops: SUBDIR := misc -tlean-loops: SUBDIR := -thol4-loops: SUBDIR := misc-loops - -test-no_nested_borrows: SUBDIR := misc -tlean-no_nested_borrows: SUBDIR := -thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows - -test-paper: SUBDIR := misc -tlean-paper: SUBDIR := -thol4-paper: SUBDIR := misc-paper - -test-polonius_list: SUBDIR := misc -tlean-polonius_list: SUBDIR := -thol4-polonius_list: SUBDIR := misc-polonius_list - -test-traits: SUBDIR := traits -tlean-traits: SUBDIR := +AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS) # Add specific options to some tests # TODO: reactivate -test-trans-units for hashmap and hashmap_main @@ -288,7 +237,7 @@ thol4-%: # This generates very ugly code, but is good to test the translation. .PHONY: ctest-test-betree_main ctest-test-betree_main: test-betree_main -ctest-test-betree_main: FILE = betree_main +ctest-test-betree_main: FILE = betree_main-special ctest-test-betree_main: BACKEND := fstar ctest-test-betree_main: $(AENEAS_CMD) 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 |] |