diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 92 |
1 files changed, 46 insertions, 46 deletions
@@ -85,13 +85,13 @@ clean: # Test the project by translating test files to F* .PHONY: tests -tests: trans-no_nested_borrows trans-paper \ - trans-hashmap trans-hashmap_main \ - trans-external trans-constants \ - transp-polonius_list transp-betree_main \ - test-transp-betree_main \ - trans-loops \ - trans-array trans-traits # TODO: generalize to all backends +tests: test-no_nested_borrows test-paper \ + test-hashmap test-hashmap_main \ + test-external test-constants \ + testp-polonius_list testp-betree_main \ + ctest-testp-betree_main \ + test-loops \ + test-array test-traits # TODO: generalize to all backends # Verify the F* files generated by the translation .PHONY: verify @@ -114,25 +114,25 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA # Add specific options to some tests -trans-no_nested_borrows trans-paper: \ +test-no_nested_borrows test-paper: \ OPTIONS += -test-trans-units -no-split-files -no-state -trans-no_nested_borrows trans-paper: SUBDIR := misc +test-no_nested_borrows test-paper: SUBDIR := misc tfstar-no_nested_borrows tfstar-paper: tlean-no_nested_borrows: SUBDIR := tlean-paper: SUBDIR := thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows thol4-paper: SUBDIR := misc-paper -trans-array: OPTIONS += -no-state -trans-array: SUBDIR := array +test-array: OPTIONS += -no-state +test-array: SUBDIR := array tfstar-array: OPTIONS += -decreases-clauses -template-clauses tcoq-array: OPTIONS += -use-fuel tlean-array: SUBDIR := tlean-array: OPTIONS += thol4-array: OPTIONS += -trans-traits: OPTIONS += -no-state -trans-traits: SUBDIR := traits +test-traits: OPTIONS += -no-state +test-traits: SUBDIR := traits tfstar-traits: OPTIONS += -decreases-clauses -template-clauses tcoq-traits: OPTIONS += -use-fuel tlean-traits: SUBDIR := @@ -147,16 +147,16 @@ thol4-array: thol4-traits: echo "Ignoring the traits test for HOL4" -trans-loops: OPTIONS += -no-state -trans-loops: SUBDIR := misc +test-loops: OPTIONS += -no-state +test-loops: SUBDIR := misc tfstar-loops: OPTIONS += -decreases-clauses -template-clauses tcoq-loops: OPTIONS += -use-fuel -no-split-files tlean-loops: SUBDIR := thol4-loops: SUBDIR := misc-loops # TODO: reactivate -test-trans-units -trans-hashmap: OPTIONS += -no-state -trans-hashmap: SUBDIR := hashmap +test-hashmap: OPTIONS += -no-state +test-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel tlean-hashmap: SUBDIR := @@ -164,15 +164,15 @@ tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hash thol4-hashmap: OPTIONS += # TODO: reactivate -test-trans-units -trans-hashmap_main: OPTIONS += -trans-hashmap_main: SUBDIR := hashmap_on_disk +test-hashmap_main: OPTIONS += +test-hashmap_main: SUBDIR := hashmap_on_disk tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap_main: OPTIONS += -use-fuel tlean-hashmap_main: SUBDIR := thol4-hashmap_main: OPTIONS += -transp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state -transp-polonius_list: SUBDIR := misc +testp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state +testp-polonius_list: SUBDIR := misc tfstarp-polonius_list: OPTIONS += tcoqp-polonius_list: OPTIONS += tleanp-polonius_list: SUBDIR := @@ -180,8 +180,8 @@ tleanp-polonius_list: OPTIONS += thol4p-polonius_list: SUBDIR := misc-polonius_list thol4p-polonius_list: OPTIONS += -trans-constants: OPTIONS += -test-trans-units -no-split-files -no-state -trans-constants: SUBDIR := misc +test-constants: OPTIONS += -test-trans-units -no-split-files -no-state +test-constants: SUBDIR := misc tfstar-constants: OPTIONS += tcoq-constants: OPTIONS += tlean-constants: SUBDIR := @@ -189,8 +189,8 @@ tlean-constants: OPTIONS += thol4-constants: SUBDIR := misc-constants thol4-constants: OPTIONS += -trans-external: OPTIONS += -test-trans-units -trans-external: SUBDIR := misc +test-external: OPTIONS += -test-trans-units +test-external: SUBDIR := misc tfstar-external: OPTIONS += tcoq-external: OPTIONS += tlean-external: SUBDIR := @@ -199,25 +199,25 @@ thol4-external: SUBDIR := misc-external thol4-external: OPTIONS += BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -transp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -transp-betree_main: SUBDIR:=betree +testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units +testp-betree_main: SUBDIR:=betree tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) tcoqp-betree_main: OPTIONS += -use-fuel tleanp-betree_main: SUBDIR := tleanp-betree_main: OPTIONS += thol4-betree_main: OPTIONS += -# Additional test on the betree: translate it without `-backward-no-state-update`. +# Additional, *c*ustom test on the betree: translate it without `-backward-no-state-update`. # This generates very ugly code, but is good to test the translation. -.PHONY: test-transp-betree_main -test-transp-betree_main: transp-betree_main -test-transp-betree_main: OPTIONS += -backend fstar -test-trans-units -test-transp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) -test-transp-betree_main: BACKEND_SUBDIR := "fstar" -test-transp-betree_main: SUBDIR:=betree_back_stateful -test-transp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -test-transp-betree_main: FILE = betree_main -test-transp-betree_main: +.PHONY: ctest-testp-betree_main +ctest-testp-betree_main: testp-betree_main +ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units +ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) +ctest-testp-betree_main: BACKEND_SUBDIR := "fstar" +ctest-testp-betree_main: SUBDIR:=betree_back_stateful +ctest-testp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +ctest-testp-betree_main: FILE = betree_main +ctest-testp-betree_main: $(AENEAS_CMD) # Generic rules to extract the LLBC from a rust file @@ -234,20 +234,20 @@ gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) gen-llbcp-%: $(CHARON_CMD) -# Generic rules to test the translation of an LLBC file. +# Generic rules to test the testlation of an LLBC file. # Note that the files requiring the Polonius borrow-checker are generated # in the tests-polonius subdirectory. -.PHONY: trans-% -trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) -trans-%: FILE = $* -trans-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-% +.PHONY: test-% +test-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) +test-%: FILE = $* +test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-% echo "# Test $* done" # "p" stands for "Polonius" -.PHONY: transp-% -transp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -transp-%: FILE = $* -transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% +.PHONY: testp-% +testp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +testp-%: FILE = $* +testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% echo "# Test $* done" .PHONY: tfstar-% |