diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 39 |
1 files changed, 26 insertions, 13 deletions
@@ -90,7 +90,8 @@ tests: trans-no_nested_borrows trans-paper \ trans-external trans-constants \ transp-polonius_list transp-betree_main \ test-transp-betree_main \ - trans-loops + trans-loops \ + trans-array # TODO: generalize to all backends # Verify the F* files generated by the translation .PHONY: verify @@ -122,6 +123,18 @@ 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 +tfstar-array: OPTIONS += -decreases-clauses -template-clauses +tcoq-array: OPTIONS += -use-fuel +tlean-array: SUBDIR := +tlean-array: OPTIONS += +thol4-array: OPTIONS += + +# TODO: activate the arrays for all the backends +thol4-array: + echo "Ignoring the array test for HOL4" + trans-loops: OPTIONS += -no-state trans-loops: SUBDIR := misc tfstar-loops: OPTIONS += -decreases-clauses -template-clauses @@ -129,15 +142,15 @@ tcoq-loops: OPTIONS += -use-fuel -no-split-files tlean-loops: SUBDIR := thol4-loops: SUBDIR := misc-loops -trans-hashmap: OPTIONS += -no-state +trans-hashmap: OPTIONS += -no-state -test-trans-units trans-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel tlean-hashmap: SUBDIR := -tlean-hashmap: OPTIONS += +tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it thol4-hashmap: OPTIONS += -trans-hashmap_main: OPTIONS += +trans-hashmap_main: OPTIONS += -test-trans-units trans-hashmap_main: SUBDIR := hashmap_on_disk tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap_main: OPTIONS += -use-fuel @@ -162,7 +175,7 @@ tlean-constants: OPTIONS += thol4-constants: SUBDIR := misc-constants thol4-constants: OPTIONS += -trans-external: OPTIONS += +trans-external: OPTIONS += -test-trans-units trans-external: SUBDIR := misc tfstar-external: OPTIONS += tcoq-external: OPTIONS += @@ -172,7 +185,7 @@ thol4-external: SUBDIR := misc-external thol4-external: OPTIONS += BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -transp-betree_main: OPTIONS += -backward-no-state-update +transp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units transp-betree_main: SUBDIR:=betree tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) tcoqp-betree_main: OPTIONS += -use-fuel @@ -224,20 +237,20 @@ transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% echo "# Test $* done" .PHONY: tfstar-% -tfstar-%: OPTIONS += -backend fstar -test-trans-units +tfstar-%: OPTIONS += -backend fstar tfstar-%: BACKEND_SUBDIR := fstar tfstar-%: $(AENEAS_CMD) # "p" stands for "Polonius" .PHONY: tfstarp-% -tfstarp-%: OPTIONS += -backend fstar -test-trans-units +tfstarp-%: OPTIONS += -backend fstar tfstarp-%: BACKEND_SUBDIR := fstar tfstarp-%: $(AENEAS_CMD) .PHONY: tcoq-% -tcoq-%: OPTIONS += -backend coq -test-trans-units +tcoq-%: OPTIONS += -backend coq tcoq-%: BACKEND_SUBDIR := coq tcoq-%: $(AENEAS_CMD) @@ -250,7 +263,7 @@ tcoqp-%: $(AENEAS_CMD) .PHONY: tlean-% -tlean-%: OPTIONS += -backend lean -test-trans-units +tlean-%: OPTIONS += -backend lean tlean-%: BACKEND_SUBDIR := lean tlean-%: $(AENEAS_CMD) @@ -258,19 +271,19 @@ tlean-%: # "p" stands for "Polonius" .PHONY: tleanp-% -tleanp-%: OPTIONS += -backend lean -test-trans-units +tleanp-%: OPTIONS += -backend lean tleanp-%: BACKEND_SUBDIR := lean tleanp-%: $(AENEAS_CMD) .PHONY: thol4-% -thol4-%: OPTIONS += -backend hol4 -test-trans-units +thol4-%: OPTIONS += -backend hol4 thol4-%: BACKEND_SUBDIR := hol4 thol4-%: $(AENEAS_CMD) .PHONY: thol4p-% -thol4p-%: OPTIONS += -backend hol4 -test-trans-units +thol4p-%: OPTIONS += -backend hol4 thol4p-%: BACKEND_SUBDIR := hol4 thol4p-%: $(AENEAS_CMD) |