diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 29 |
1 files changed, 13 insertions, 16 deletions
@@ -145,27 +145,24 @@ test: build-dev test-all betree-tests betree-tests: cd $(INPUTS_DIR)/betree && $(MAKE) test -.PHONY: test-all -test-all: \ - test-arrays \ - test-betree_main \ - test-bitwise \ - test-constants \ - test-demo \ - test-external \ - test-hashmap \ - test-hashmap_main \ - test-loops \ - test-no_nested_borrows \ - test-paper \ - test-polonius_list \ - test-traits - # Verify the F* files generated by the translation .PHONY: verify verify: cd tests && $(MAKE) all +# List the files and directories in `INPUTS_DIR` +INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*) +# Remove the directory prefix, replace with `test-` +INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST)) +# Remove some tests we don't want to run. +# FIXME: move this information to the file itself +INPUTS_LIST := $(filter-out test-hashmap_utils.rs,$(INPUTS_LIST)) +INPUTS_LIST := $(filter-out test-nested_borrows.rs,$(INPUTS_LIST)) + +# Run all the tests we found. +.PHONY: test-all +test-all: $(INPUTS_LIST) + ifdef IN_CI # In CI we do extra sanity checks. test-%: AENEAS_OPTIONS += -checks |