From 4c3a164ed570ecfa721255519554911754913271 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 20 Jun 2022 06:21:57 +0200
Subject: Add makefiles to test the F* files

---
 Makefile | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 1e62dfd5..58919a7b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-all: build-test
+all: build-test-verify
 
 CHARON_HOME = ../charon
 CHARON_EXEC = $(CHARON_HOME)/charon
@@ -19,21 +19,26 @@ TRANS_OPTIONS := -test-trans-units $(OPTIONS)
 SUBDIR :=
 
 # Build the project and test it
-.PHONY: build-test
-build-test: build test
+.PHONY: build-test-verify
+build-test-verify: build test verify
 
 # Build the project
 .PHONY: build
 build:
 	dune build src/main.exe
 
-# Test the project
+# Test the project by translating test files to F*
 .PHONY: test
 test: build trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-nll-betree_nll \
 	trans-nll-betree_main
 
+# Verify the translated F* files
+.PHONY: verify
+verify: build test
+	cd tests && make all
+
 # Add specific options to some tests
 trans-no_nested_borrows trans-paper: \
 	TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
-- 
cgit v1.2.3


From 227869ddd73782834162c64a34f260b438f5cbae Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 20 Jun 2022 06:23:44 +0200
Subject: Make minor modifications

---
 Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 58919a7b..694dc964 100644
--- a/Makefile
+++ b/Makefile
@@ -18,7 +18,7 @@ OPTIONS ?=
 TRANS_OPTIONS := -test-trans-units $(OPTIONS)
 SUBDIR :=
 
-# Build the project and test it
+# Build the project, test it and verify the generated files
 .PHONY: build-test-verify
 build-test-verify: build test verify
 
@@ -34,7 +34,7 @@ test: build trans-no_nested_borrows trans-paper \
 	trans-external trans-nll-betree_nll \
 	trans-nll-betree_main
 
-# Verify the translated F* files
+# Verify the F* files generated by the translation
 .PHONY: verify
 verify: build test
 	cd tests && make all
-- 
cgit v1.2.3