summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon Ho2023-11-29 15:45:27 +0100
committerSon Ho2023-11-29 15:45:27 +0100
commitdc4b11689131bdb41a43e5aca76538556a3a120c (patch)
tree513cd1909faa9b0316a0e6f6be2fa88b7a1e90a7 /Makefile
parent0273fee7f6b74da1d3b66c3c6a2158c012d04197 (diff)
Add support for more bitwise operations and update the extraction
Diffstat (limited to '')
-rw-r--r--Makefile19
1 files changed, 10 insertions, 9 deletions
diff --git a/Makefile b/Makefile
index 88cb7d05..2cce30d9 100644
--- a/Makefile
+++ b/Makefile
@@ -91,7 +91,7 @@ tests: test-no_nested_borrows test-paper \
testp-polonius_list testp-betree_main \
ctest-testp-betree_main \
test-loops \
- test-array test-traits # TODO: generalize to all backends
+ test-array test-traits test-bitwise
# Verify the F* files generated by the translation
.PHONY: verify
@@ -139,14 +139,6 @@ tlean-traits: SUBDIR :=
tlean-traits: OPTIONS +=
thol4-traits: OPTIONS +=
-# TODO: activate the arrays for all the backends
-thol4-array:
- echo "Ignoring the array test for HOL4"
-
-# TODO: activate the traits for all the backends
-thol4-traits:
- echo "Ignoring the traits test for HOL4"
-
test-loops: OPTIONS +=
test-loops: SUBDIR := misc
tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files
@@ -198,6 +190,15 @@ tlean-external: OPTIONS +=
thol4-external: SUBDIR := misc-external
thol4-external: OPTIONS +=
+test-bitwise: OPTIONS += -test-trans-units
+test-bitwise: SUBDIR := misc
+tfstar-bitwise: OPTIONS +=
+tcoq-bitwise: OPTIONS +=
+tlean-bitwise: SUBDIR :=
+tlean-bitwise: OPTIONS +=
+thol4-bitwise: SUBDIR := misc-bitwise
+thol4-bitwise: OPTIONS +=
+
BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
testp-betree_main: SUBDIR:=betree