diff options
| author | Sidney Congard | 2022-06-30 14:54:15 +0200 |
|---|---|---|
| committer | Sidney Congard | 2022-06-30 14:54:15 +0200 |
| commit | fdbbb82ff89b1d5141ec63bc2385936da3de3616 (patch) | |
| tree | d48e3fa933280e8a275d2cfdab8f126e920e5f13 /Makefile | |
| parent | 47691de8fe3dc32a29663d4d8343eb415ce1d81e (diff) | |
| parent | 4f33892c81cdaf6aefaad9b7cef1456dcfead67c (diff) | |
Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2
Complete the constants extraction by making all functions fail
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 15 |
1 files changed, 10 insertions, 5 deletions
@@ -1,4 +1,4 @@ -all: build-test +all: build-test-verify CHARON_HOME = ../charon CHARON_EXEC = $(CHARON_HOME)/charon @@ -18,22 +18,27 @@ OPTIONS ?= TRANS_OPTIONS := -test-trans-units $(OPTIONS) SUBDIR := -# Build the project and test it -.PHONY: build-test -build-test: build test +# Build the project, test it and verify the generated files +.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-constants \ trans-nll-betree_nll trans-nll-betree_main \ +# Verify the F* files generated by the translation +.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 |