diff options
| author | Son Ho | 2022-06-20 06:21:57 +0200 |
|---|---|---|
| committer | Son Ho | 2022-06-20 06:21:57 +0200 |
| commit | 4c3a164ed570ecfa721255519554911754913271 (patch) | |
| tree | ebb622998a13f79662f92b02c5f2600c928e7f62 /Makefile | |
| parent | f51f4c5d883691ef73094a79b4316255191627b0 (diff) | |
Add makefiles to test the F* files
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 13 |
1 files changed, 9 insertions, 4 deletions
@@ -1,4 +1,4 @@ -all: build-test +all: build-test-verify CHARON_HOME = ../charon CHARON_EXEC = $(CHARON_HOME)/charon @@ -19,21 +19,26 @@ TRANS_OPTIONS := -test-trans-units $(OPTIONS) SUBDIR := # Build the project and test it -.PHONY: build-test -build-test: build test +.PHONY: build-test-verify +build-test-verify: build test verify # Build the project .PHONY: build build: dune build src/main.exe -# Test the project +# Test the project by translating test files to F* .PHONY: test test: build trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ trans-external trans-nll-betree_nll \ trans-nll-betree_main +# Verify the translated F* files +.PHONY: verify +verify: build test + cd tests && make all + # Add specific options to some tests trans-no_nested_borrows trans-paper: \ TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses |