summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon HO2024-05-27 09:39:39 +0200
committerGitHub2024-05-27 09:39:39 +0200
commitaeff52b13b9b3068efcc4a805a9786bf2053d141 (patch)
tree229e6fc225bf8456a01985cd3b583e510acc3886 /Makefile
parent3ff6d93822fe5b2e233d4b12b88b38839c8533c5 (diff)
parent4971b7edf4538144df735f9fa5327fe4d0e2e003 (diff)
Merge branch 'main' into unsigned-max
Diffstat (limited to '')
-rw-r--r--Makefile14
1 files changed, 7 insertions, 7 deletions
diff --git a/Makefile b/Makefile
index b3dc9f2b..bda88c74 100644
--- a/Makefile
+++ b/Makefile
@@ -47,7 +47,12 @@ build-test-verify: build test verify
# Build the project, without formatting the code
.PHONY: build-dev
+ifdef IN_CI
+build-dev:
+ @true
+else
build-dev: build-bin build-lib build-bin-dir doc
+endif
.PHONY: build-bin
build-bin: check-charon
@@ -154,10 +159,6 @@ verify:
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
@@ -166,14 +167,13 @@ test-all: $(INPUTS_LIST)
ifdef IN_CI
# In CI we do extra sanity checks.
test-%: AENEAS_OPTIONS += -checks
-else
-test-%: check-charon
endif
# Translate the given rust file to available backends. The test runner decides
# which backends to use and sets test-specific options.
+# Note: the tests have the fulle file name: `test-arrays.rs`, `test-loops.rs`, `test-betree`.
.PHONY: test-%
-test-%:
+test-%: build-dev
$(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(INPUTS_DIR)/"$*" $(AENEAS_OPTIONS)
echo "# Test $* done"