From 5e1e4f11dc2f75f20728ea1022b29a67c87bc07c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 18 Oct 2022 22:39:45 +0200
Subject: Update the Makefile

---
 Makefile | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/Makefile b/Makefile
index 93ff7431..c59aec01 100644
--- a/Makefile
+++ b/Makefile
@@ -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
-- 
cgit v1.2.3