summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon Ho2022-01-26 23:34:31 +0100
committerSon Ho2022-01-26 23:34:31 +0100
commit29602c3fb6523d3699b85ca447aa92521a7f60d3 (patch)
treee3570ddca5953670c27cb0218f1b911c824c55d0 /Makefile
parentdb1ebd1f10eaba7627d50272ec3191f470089ee3 (diff)
Change the test file to no_nested_borrows.cfim
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile11
1 files changed, 8 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index a5bdb4ce..a9b24400 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,10 @@
all: build-run-check-trace
+CHARON_HOME=../charon/charon
+CHARON_TESTS_DIR=$(CHARON_HOME)/tests
+RS_TEST_FILE=tests/no_nested_borrows.rs
+CFIM_TEST_FILE=$(CHARON_TESTS_DIR)/no_nested_borrows.cfim
+
# Build the project and run the executable
.PHONY: build-run
build-run:
@@ -11,7 +16,7 @@ build-run:
.PHONY: build-run-check-trace
build-run-check-trace: generate-cfim
dune build src/main.exe && \
- dune exec src/main.exe ../charon/charon/tests/test1.cfim > tests/trace_current.txt && \
+ dune exec src/main.exe $(CFIM_TEST_FILE) > tests/trace_current.txt && \
cmp tests/trace_reference.txt tests/trace_current.txt && \
rm tests/trace_current.txt
@@ -19,13 +24,13 @@ build-run-check-trace: generate-cfim
.PHONY: regen-trace
regen-trace: generate-cfim
dune build src/main.exe && \
- dune exec src/main.exe ../charon/charon/tests/test1.cfim > tests/trace_current.txt && \
+ dune exec src/main.exe $(CFIM_TEST_FILE) > tests/trace_current.txt && \
rm tests/trace_reference.txt && \
mv tests/trace_current.txt tests/trace_reference.txt
.PHONY: generate-cfim
generate-cfim:
- cd ../charon/charon && cargo run tests/test1.rs
+ cd ../charon/charon && cargo run $(RS_TEST_FILE)
doc:
dune build @doc