diff options
| author | Son Ho | 2022-10-13 18:04:31 +0200 |
|---|---|---|
| committer | Son Ho | 2022-10-13 18:04:31 +0200 |
| commit | e7b4aba11391bede785799237a73ef7bd16d0372 (patch) | |
| tree | c114050af416caef7c539cfb7ae10df889540ae6 /Makefile | |
| parent | e692a9535cecc8a19fea9d0ebf2b470a09cf4541 (diff) | |
Use "polonius" in the names instead of "nll"
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 17 |
1 files changed, 9 insertions, 8 deletions
@@ -37,7 +37,7 @@ build: tests: build trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ trans-external trans-constants \ - trans-nll-betree_nll trans-nll-betree_main + trans-polonius-betree_polonius trans-polonius-betree_main # Verify the F* files generated by the translation .PHONY: verify @@ -60,8 +60,8 @@ trans-hashmap: SUBDIR:=hashmap trans-hashmap_main: TRANS_OPTIONS += -template-clauses trans-hashmap_main: SUBDIR:=hashmap_on_disk -trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses -trans-nll-betree_nll: SUBDIR:=misc +trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses +trans-polonius-betree_polonius: SUBDIR:=misc trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses trans-constants: SUBDIR:=misc @@ -69,8 +69,8 @@ trans-constants: SUBDIR:=misc trans-external: TRANS_OPTIONS += trans-external: SUBDIR:=misc -trans-nll-betree_main: TRANS_OPTIONS += -template-clauses -trans-nll-betree_main: SUBDIR:=betree +trans-polonius-betree_main: TRANS_OPTIONS += -template-clauses +trans-polonius-betree_main: SUBDIR:=betree # 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 @@ -80,15 +80,16 @@ gen-llbc-%: build cd $(CHARON_HOME) && $(MAKE) test-$* # Generic rule to test the translation of an LLBC file. -# Note that the non-linear lifetime files are generated in the tests-nll subdirectory. +# Note that the files requiring the Polonius borrow-checker are generated +# in the tests-polonius subdirectory. .PHONY: trans-% trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc -trans-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/llbc +trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc trans-%: gen-llbc-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) -trans-nll-%: gen-llbc-nll-% +trans-polonius-%: gen-llbc-polonius-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) .PHONY: doc |