diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 19 |
1 files changed, 10 insertions, 9 deletions
@@ -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 |