From c44f3d8aafc5c45032ee16a2f85a160f66f9a6e9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Mar 2022 23:38:12 +0100
Subject: Update the Makefile to call Charon's Makefile on the tests

---
 Makefile | 21 ++++++---------------
 1 file changed, 6 insertions(+), 15 deletions(-)

diff --git a/Makefile b/Makefile
index 0c772e41..57832518 100644
--- a/Makefile
+++ b/Makefile
@@ -43,24 +43,15 @@ translate-nll-betree_nll: TRANS_OPTIONS=-test-units -no-split-files -no-state -n
 translate-nll-betree_nll: SUBDIR:=misc
 
 # Generic rules to extract the LLBC from a rust file
-# The "standard" and the nll (non-linear lifetime) tests are in separate
-# directories in Charon
+# We use the rules in Charon's Makefile to generate the .llbc files: the options
+# vary with the test files.
 .PHONY: gen-llbc-%
-
-# TODO: remove those "gen-..." rules, and just do `make` in the charon repo
-gen-llbc-%: CHARON_OPTIONS = --dest ../tests/llbc --no-code-duplication
-gen-llbc-%: CHARON_TESTS_SRC = ../tests/src
-
-gen-llbc-nll-%: CHARON_OPTIONS = --dest ../tests-nll/llbc --no-code-duplication --nll
-gen-llbc-nll-%: CHARON_TESTS_SRC = ../tests-nll/src
-
 gen-llbc-%: build
-	cd $(CHARON_HOME)/charon && cargo run $(CHARON_TESTS_SRC)/$*.rs $(CHARON_OPTIONS)
-
-gen-llbc-nll-%: build
-	cd $(CHARON_HOME)/charon && cargo run $(CHARON_TESTS_SRC)/$*.rs $(CHARON_OPTIONS)
+	cd $(CHARON_HOME) && make test-$*
 
-# Generic rule to test the translation on a LLBC file
+# Generic rule to test the translation on an LLBC file.
+# Note that the non-linear lifetime files are generated in the tests-nll
+# subdirectory.
 .PHONY: translate-%
 translate-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
 translate-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/llbc
-- 
cgit v1.2.3