diff options
| author | Son Ho | 2023-08-03 00:24:09 +0200 |
|---|---|---|
| committer | Son Ho | 2023-08-03 00:24:09 +0200 |
| commit | fcbb06f1b32c42b42d6bde501a4bc29a661ec23b (patch) | |
| tree | 75ad4da46d41ff82bbc31c75661509fc98da95f1 | |
| parent | c6f0a8c8bfe04e83de4692a389daf8cde47b74d5 (diff) | |
Update the Makefile to add the array test
| -rw-r--r-- | Makefile | 17 |
1 files changed, 16 insertions, 1 deletions
@@ -90,7 +90,8 @@ tests: trans-no_nested_borrows trans-paper \ trans-external trans-constants \ transp-polonius_list transp-betree_main \ test-transp-betree_main \ - trans-loops + trans-loops \ + trans-array # TODO: generalize to all backends # Verify the F* files generated by the translation .PHONY: verify @@ -122,6 +123,20 @@ tlean-paper: SUBDIR := thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows thol4-paper: SUBDIR := misc-paper +trans-array: OPTIONS += -no-state +trans-array: SUBDIR := array +tfstar-array: OPTIONS += +tcoq-array: OPTIONS += +tlean-array: SUBDIR := +tlean-array: OPTIONS += +thol4-array: OPTIONS += + +# TODO: activate the arrays for all the backends +tcoq-array: + echo "Ignoring the array test for Coq" +thol4-array: + echo "Ignoring the array test for HOL4" + trans-loops: OPTIONS += -no-state trans-loops: SUBDIR := misc tfstar-loops: OPTIONS += -decreases-clauses -template-clauses |