summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 7 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 0807e092..93ac5b2e 100644
--- a/Makefile
+++ b/Makefile
@@ -2,9 +2,13 @@ all: build-run-check-trace
CHARON_HOME=../charon/charon
CHARON_TESTS_DIR=$(CHARON_HOME)/tests/src
+DEST_DIR=tests/
+
RS_TEST_FILE1=tests/src/no_nested_borrows.rs
CFIM_TEST_FILE1=$(CHARON_TESTS_DIR)/no_nested_borrows.cfim
-DEST_DIR=tests/
+
+RS_TEST_FILE2=tests/src/hashmap.rs
+CFIM_TEST_FILE2=$(CHARON_TESTS_DIR)/hashmap.cfim
# Build the project
.PHONY: build
@@ -15,6 +19,7 @@ build:
.PHONY: build-run
build-run: build
dune exec -- src/main.exe $(CFIM_TEST_FILE1) -dest $(DEST_DIR) -test-units -test-trans-units > tests/trace_current.txt
+ dune exec -- src/main.exe $(CFIM_TEST_FILE2) -dest $(DEST_DIR)
# Build the project and run the executable, then check that the behaviour
# of the interpreter didn't change by comparing the newly generated trace
@@ -34,6 +39,7 @@ regen-trace: generate-cfim build-run
.PHONY: generate-cfim
generate-cfim:
cd ../charon/charon && cargo run $(RS_TEST_FILE1)
+ cd ../charon/charon && cargo run $(RS_TEST_FILE2)
doc:
dune build @doc