From 1ff4a1b9cd931dc7cf20f7f5619b110a097e3b3a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Feb 2022 10:58:34 +0100
Subject: Update the Makefile so as not to generate and check traces anymore

---
 Makefile | 19 ++-----------------
 1 file changed, 2 insertions(+), 17 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index e17d4197..2089f6b8 100644
--- a/Makefile
+++ b/Makefile
@@ -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)
-- 
cgit v1.2.3