diff options
| author | Son HO | 2023-11-29 16:02:42 +0100 |
|---|---|---|
| committer | GitHub | 2023-11-29 16:02:42 +0100 |
| commit | 789ba1473acd287814a0d659b5f5a0e480e4e9d7 (patch) | |
| tree | 983ad685eb6b3c60b0baa3e3920dedbc6eaa0e57 /Makefile | |
| parent | 90e42e0e1c1889aabfa66283fb15b43a5852a02a (diff) | |
| parent | e732f97d09179fae43fafcb244340f98e3ca9229 (diff) | |
Merge pull request #39 from AeneasVerif/afromher_shifts
Add support for bitshifts
Diffstat (limited to 'Makefile')
| -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 |