diff options
| author | Son Ho | 2022-10-18 22:39:45 +0200 |
|---|---|---|
| committer | Son Ho | 2022-10-18 22:39:45 +0200 |
| commit | 5e1e4f11dc2f75f20728ea1022b29a67c87bc07c (patch) | |
| tree | ce392cb5b0a9d76b595a461f4fea3c9d57ccbc7c | |
| parent | 10e9c20073e1fcd3acf1194b9074a21bdccd44ca (diff) | |
Update the Makefile
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 10 |
1 files changed, 7 insertions, 3 deletions
@@ -75,9 +75,13 @@ 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 # vary with the test files. +.PHONY: gen-llbc-polonius-% +gen-llbc-polonius-%: build + cd $(CHARON_HOME)/tests-polonius && $(MAKE) test-$* + .PHONY: gen-llbc-% gen-llbc-%: build - cd $(CHARON_HOME) && $(MAKE) test-$* + cd $(CHARON_HOME)/tests && $(MAKE) test-$* # Generic rule to test the translation of an LLBC file. # Note that the files requiring the Polonius borrow-checker are generated @@ -86,10 +90,10 @@ gen-llbc-%: build trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc -trans-%: gen-llbc-% +trans-polonius-%: gen-llbc-polonius-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) -trans-polonius-%: gen-llbc-polonius-% +trans-%: gen-llbc-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) .PHONY: doc |