summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon HO2022-09-22 18:52:15 +0200
committerGitHub2022-09-22 18:52:15 +0200
commitdd75894c85bbaa5dc6aa54d39980e160e5b7777f (patch)
treeece56b01bcadea24a3c373236f0254f47e32a98f /Makefile
parentd8f92140abd7e65b6f1c5dd7e511c0c0aa69e73f (diff)
parent0d5fb87166cc4eb4ddc783d871ad459479fc9fdc (diff)
Merge pull request #1 from AeneasVerif/constants-v2
Implement support for globals
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile12
1 files changed, 10 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 694dc964..db308fbd 100644
--- a/Makefile
+++ b/Makefile
@@ -31,14 +31,19 @@ build:
.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
+ trans-external trans-constants \
+ trans-nll-betree_nll trans-nll-betree_main
# Verify the F* files generated by the translation
.PHONY: verify
verify: build test
cd tests && make all
+# Reformat the project
+.PHONY: format
+format:
+ dune build @fmt && dune promote
+
# Add specific options to some tests
trans-no_nested_borrows trans-paper: \
TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
@@ -53,6 +58,9 @@ trans-hashmap_main: SUBDIR:=hashmap_on_disk
trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
trans-nll-betree_nll: SUBDIR:=misc
+trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
+trans-constants: SUBDIR:=misc
+
trans-external: TRANS_OPTIONS +=
trans-external: SUBDIR:=misc