summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Makefile8
1 files changed, 7 insertions, 1 deletions
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