From dc4b11689131bdb41a43e5aca76538556a3a120c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 29 Nov 2023 15:45:27 +0100
Subject: Add support for more bitwise operations and update the extraction

---
 Makefile | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

(limited to 'Makefile')

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
-- 
cgit v1.2.3