diff options
| author | Son Ho | 2022-02-09 10:58:34 +0100 |
|---|---|---|
| committer | Son Ho | 2022-02-09 10:58:34 +0100 |
| commit | 1ff4a1b9cd931dc7cf20f7f5619b110a097e3b3a (patch) | |
| tree | 11b7d8eca2eef64ba1afda27e047437844e68bb1 /Makefile | |
| parent | 8dba05c8d50e42fa100952bae6a9da110040ac94 (diff) | |
Update the Makefile so as not to generate and check traces anymore
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 19 |
1 files changed, 2 insertions, 17 deletions
@@ -1,4 +1,4 @@ -all: build-run-check-trace +all: build-run CHARON_HOME=../charon/charon CHARON_TESTS_DIR=$(CHARON_HOME)/tests/src @@ -18,24 +18,9 @@ build: # Build the project and run the executable .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_FILE1) -dest $(DEST_DIR) -test-units -test-trans-units dune exec -- src/main.exe $(CFIM_TEST_FILE2) -dest $(DEST_DIR) -test-trans-units -# Build the project and run the executable, then check that the behaviour -# of the interpreter didn't change by comparing the newly generated trace -# with a reference. -.PHONY: build-run-check-trace -build-run-check-trace: generate-cfim build-run - cmp tests/trace_reference.txt tests/trace_current.txt && \ - cp fstar/Primitives.fst $(DEST_DIR) - -# Build the project and update the trace -.PHONY: regen-trace -regen-trace: generate-cfim build-run - rm -f tests/trace_reference.txt && \ - cp tests/trace_current.txt tests/trace_reference.txt && \ - cp fstar/Primitives.fst $(DEST_DIR) - .PHONY: generate-cfim generate-cfim: cd ../charon/charon && cargo run $(RS_TEST_FILE1) |