diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 34 |
1 files changed, 28 insertions, 6 deletions
@@ -54,7 +54,8 @@ clean: tests: build trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ trans-external trans-constants \ - trans-polonius-betree_polonius trans-polonius-betree_main + trans-polonius-betree_polonius trans-polonius-betree_main \ + test-trans-polonius-betree_main # Verify the F* files generated by the translation .PHONY: verify @@ -66,6 +67,12 @@ verify: build tests format: cd compiler && dune promote +# The commands to run Charon to generate the .llbc files +CHARON_CMD = cd $(CHARON_HOME)/$(CHARON_TEST_SUBFOLDER) && NOT_ALL_TESTS=1 $(MAKE) test-$* + +# The command to run Aeneas on the proper llbc file +AENEAS_CMD = cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$(FILE).llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) + # Add specific options to some tests trans-no_nested_borrows trans-paper: \ TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses @@ -86,19 +93,32 @@ trans-constants: SUBDIR:=misc trans-external: TRANS_OPTIONS += trans-external: SUBDIR:=misc -trans-polonius-betree_main: TRANS_OPTIONS += -template-clauses +BETREE_OPTIONS = -template-clauses +trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update trans-polonius-betree_main: SUBDIR:=betree +# Additional test on the betree: translate it without `-backward-no-state-update`. +# This generates very ugly code, but is good to test the translation. +test-trans-polonius-betree_main: trans-polonius-betree_main +test-trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS) +test-trans-polonius-betree_main: SUBDIR:=betree_back_stateful +test-trans-polonius-betree_main: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc +test-trans-polonius-betree_main: FILE = betree_main +test-trans-polonius-betree_main: + $(AENEAS_CMD) + # 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. .PHONY: gen-llbc-polonius-% +gen-llbc-polonius-%: CHARON_TEST_SUBFOLDER = tests-polonius gen-llbc-polonius-%: build - cd $(CHARON_HOME)/tests-polonius && NOT_ALL_TESTS=1 $(MAKE) test-$* + $(CHARON_CMD) .PHONY: gen-llbc-% +gen-llbc-%: CHARON_TEST_SUBFOLDER = tests gen-llbc-%: build - cd $(CHARON_HOME)/tests && NOT_ALL_TESTS=1 $(MAKE) test-$* + $(CHARON_CMD) # Generic rule to test the translation of an LLBC file. # Note that the files requiring the Polonius borrow-checker are generated @@ -107,8 +127,10 @@ gen-llbc-%: build trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc +trans-polonius-%: FILE = $* trans-polonius-%: gen-llbc-polonius-% - cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$*.llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) + $(AENEAS_CMD) +trans-%: FILE = $* trans-%: gen-llbc-% - cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$*.llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) + $(AENEAS_CMD) |