summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile29
1 files changed, 25 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index 9df5f264..606ed3eb 100644
--- a/Makefile
+++ b/Makefile
@@ -119,6 +119,8 @@ trans-no_nested_borrows trans-paper: SUBDIR := misc
tfstar-no_nested_borrows tfstar-paper:
tlean-no_nested_borrows: SUBDIR := misc-no_nested_borrows
tlean-paper: SUBDIR := misc-paper
+thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows
+thol4-paper: SUBDIR := misc-paper
trans-loops: OPTIONS += -no-state
trans-loops: SUBDIR := misc
@@ -126,18 +128,21 @@ tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
tcoq-loops: OPTIONS += -use-fuel -no-split-files
tlean-loops: SUBDIR := misc-loops
tlean-loops: OPTIONS += -decreases-clauses -template-clauses
+thol4-loops: SUBDIR := misc-loops
trans-hashmap: OPTIONS += -no-state
trans-hashmap: SUBDIR := hashmap
tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
tcoq-hashmap: OPTIONS += -use-fuel
tlean-hashmap: OPTIONS += -decreases-clauses -template-clauses
+thol4-hashmap: OPTIONS +=
trans-hashmap_main: OPTIONS +=
trans-hashmap_main: SUBDIR := hashmap_on_disk
tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
tcoq-hashmap_main: OPTIONS += -use-fuel
tlean-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
+thol4-hashmap_main: OPTIONS +=
transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
transp-polonius_list: SUBDIR := misc
@@ -145,6 +150,8 @@ tfstarp-polonius_list: OPTIONS +=
tcoqp-polonius_list: OPTIONS +=
tleanp-polonius_list: SUBDIR := misc-polonius_list
tleanp-polonius_list: OPTIONS +=
+thol4p-polonius_list: SUBDIR := misc-polonius_list
+thol4p-polonius_list: OPTIONS +=
trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
trans-constants: SUBDIR := misc
@@ -152,6 +159,8 @@ tfstar-constants: OPTIONS +=
tcoq-constants: OPTIONS +=
tlean-constants: SUBDIR := misc-constants
tlean-constants: OPTIONS +=
+thol4-constants: SUBDIR := misc-constants
+thol4-constants: OPTIONS +=
trans-external: OPTIONS +=
trans-external: SUBDIR := misc
@@ -159,6 +168,8 @@ tfstar-external: OPTIONS +=
tcoq-external: OPTIONS +=
tlean-external: SUBDIR := misc-external
tlean-external: OPTIONS +=
+thol4-external: SUBDIR := misc-external
+thol4-external: OPTIONS +=
BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
transp-betree_main: OPTIONS += -backward-no-state-update
@@ -166,6 +177,7 @@ transp-betree_main: SUBDIR:=betree
tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
tcoqp-betree_main: OPTIONS += -use-fuel
tleanp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
+thol4-betree_main: OPTIONS +=
# Additional test on the betree: translate it without `-backward-no-state-update`.
# This generates very ugly code, but is good to test the translation.
@@ -200,14 +212,14 @@ gen-llbcp-%:
.PHONY: trans-%
trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
trans-%: FILE = $*
-trans-%: gen-llbc-% tfstar-% tcoq-% tlean-%
+trans-%: 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-%
+transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
echo "# Test $* done"
.PHONY: tfstar-%
@@ -243,8 +255,6 @@ tlean-%: BACKEND_SUBDIR := lean
tlean-%:
$(AENEAS_CMD)
-
-
# "p" stands for "Polonius"
.PHONY: tleanp-%
@@ -259,6 +269,17 @@ tleanp-%: BACKEND_SUBDIR := lean
tleanp-%:
$(AENEAS_CMD)
+.PHONY: thol4-%
+thol4-%: OPTIONS += -backend hol4 -test-trans-units
+thol4-%: BACKEND_SUBDIR := hol4
+thol4-%:
+ $(AENEAS_CMD)
+
+.PHONY: thol4p-%
+thol4p-%: OPTIONS += -backend hol4 -test-trans-units
+thol4p-%: BACKEND_SUBDIR := hol4
+thol4p-%:
+ $(AENEAS_CMD)
# Nix - TODO: add the lean tests
.PHONY: nix