From 2291934834131e8a6c0c839afa83a2cfb00162d8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Feb 2022 11:23:18 +0100
Subject: Update the Makefile to make it more generic

---
 Makefile | 38 ++++++++++++++++++++++++--------------
 1 file changed, 24 insertions(+), 14 deletions(-)

diff --git a/Makefile b/Makefile
index 2089f6b8..67212e22 100644
--- a/Makefile
+++ b/Makefile
@@ -1,30 +1,40 @@
-all: build-run
+all: build-test
 
 CHARON_HOME=../charon/charon
 CHARON_TESTS_DIR=$(CHARON_HOME)/tests/src
 DEST_DIR=tests/
 
-RS_TEST_FILE1=tests/src/no_nested_borrows.rs
-CFIM_TEST_FILE1=$(CHARON_TESTS_DIR)/no_nested_borrows.cfim
+# Default translation options:
+# - insert calls to the normalizer in the translated code to test the
+#   generated unit functions
+TRANS_OPTIONS=-test-trans-units
 
-RS_TEST_FILE2=tests/src/hashmap.rs
-CFIM_TEST_FILE2=$(CHARON_TESTS_DIR)/hashmap.cfim
+# Build the project and test it
+.PHONY: build-test
+build-test: build test
 
 # Build the project
 .PHONY: build
 build:
 	dune build src/main.exe
 
-# Build the project and run the executable
-.PHONY: build-run
-build-run: build
-	dune exec -- src/main.exe $(CFIM_TEST_FILE1) -dest $(DEST_DIR) -test-units -test-trans-units
-	dune exec -- src/main.exe $(CFIM_TEST_FILE2) -dest $(DEST_DIR) -test-trans-units
+# Test the project
+.PHONY: test
+test: build translate-no_nested_borrows translate-hashmap
 
-.PHONY: generate-cfim
-generate-cfim:
-	cd ../charon/charon && cargo run $(RS_TEST_FILE1)
-	cd ../charon/charon && cargo run $(RS_TEST_FILE2)
+# Add specific options to some tests
+translate-no_nested_borrows: OPTIONS := $(OPTIONS) -test-units
 
+# Generic rule to extract the CFIM from a rust file
+.PHONY: gen-cfim-%
+gen-cfim-%: build
+	cd ../charon/charon && cargo run tests/src/$*.rs
+
+# Generic rule to test the translation on a CFIM file
+.PHONY: translate-%
+translate-%: gen-cfim-%
+	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.cfim -dest $(DEST_DIR) $(TRANS_OPTIONS)
+
+.PHONY: doc
 doc:
 	dune build @doc
-- 
cgit v1.2.3