From 304490110509324a20c7c2c3be9bf61931fa3a1c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 17 Dec 2022 10:50:43 +0100
Subject: Make minor modifications and generate code for loops

---
 Makefile | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 797c8861..19ba0b6f 100644
--- a/Makefile
+++ b/Makefile
@@ -89,7 +89,8 @@ tests: trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-constants \
 	transp-polonius_list transp-betree_main \
-	test-transp-betree_main
+	test-transp-betree_main \
+	trans-loops
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -117,6 +118,11 @@ trans-no_nested_borrows trans-paper: \
 trans-no_nested_borrows trans-paper: SUBDIR:=misc
 tfstar-no_nested_borrows tfstar-paper:
 
+trans-loops: OPTIONS += -no-state
+trans-loops: SUBDIR := misc
+tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
+tcoq-loops: OPTIONS += -use-fuel -no-split-files
+
 trans-hashmap: OPTIONS += -no-state
 trans-hashmap: SUBDIR:=hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
-- 
cgit v1.2.3