summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Makefile34
1 files changed, 28 insertions, 6 deletions
diff --git a/Makefile b/Makefile
index c9b0b566..a0ce6d21 100644
--- a/Makefile
+++ b/Makefile
@@ -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)