From fcbb06f1b32c42b42d6bde501a4bc29a661ec23b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Aug 2023 00:24:09 +0200
Subject: Update the Makefile to add the array test

---
 Makefile | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 1b11592f..8865746d 100644
--- a/Makefile
+++ b/Makefile
@@ -90,7 +90,8 @@ tests: trans-no_nested_borrows trans-paper \
 	trans-external trans-constants \
 	transp-polonius_list transp-betree_main \
 	test-transp-betree_main \
-	trans-loops
+	trans-loops \
+	trans-array # TODO: generalize to all backends
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -122,6 +123,20 @@ tlean-paper: SUBDIR :=
 thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows
 thol4-paper: SUBDIR := misc-paper
 
+trans-array: OPTIONS += -no-state
+trans-array: SUBDIR := array
+tfstar-array: OPTIONS +=
+tcoq-array: OPTIONS +=
+tlean-array: SUBDIR :=
+tlean-array: OPTIONS +=
+thol4-array: OPTIONS +=
+
+# TODO: activate the arrays for all the backends
+tcoq-array:
+	echo "Ignoring the array test for Coq"
+thol4-array:
+	echo "Ignoring the array test for HOL4"
+
 trans-loops: OPTIONS += -no-state
 trans-loops: SUBDIR := misc
 tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
-- 
cgit v1.2.3