summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile29
1 files changed, 13 insertions, 16 deletions
diff --git a/Makefile b/Makefile
index fccca9b1..8a7701cc 100644
--- a/Makefile
+++ b/Makefile
@@ -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