Update the Makefile so as not to generate and check traces anymore

2 files changed, 16 insertions, 31 deletions

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)
diff --git a/src/main.ml b/src/main.ml
index 19f05a4c..ba677361 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -94,21 +94,21 @@ let () =
 
   (* Set up the logging - for now we use default values - TODO: use the
    * command-line arguments *)
-  Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
-  main_log#set_level EL.Debug;
-  pre_passes_log#set_level EL.Debug;
-  interpreter_log#set_level EL.Debug;
-  statements_log#set_level EL.Debug;
-  paths_log#set_level EL.Debug;
-  expressions_log#set_level EL.Debug;
-  expansion_log#set_level EL.Debug;
-  borrows_log#set_level EL.Debug;
+  Easy_logging.Handlers.set_level main_logger_handler EL.Warning;
+  main_log#set_level EL.Warning;
+  pre_passes_log#set_level EL.Warning;
+  interpreter_log#set_level EL.Warning;
+  statements_log#set_level EL.Warning;
+  paths_log#set_level EL.Warning;
+  expressions_log#set_level EL.Warning;
+  expansion_log#set_level EL.Warning;
+  borrows_log#set_level EL.Warning;
   invariants_log#set_level EL.Warning;
-  pure_utils_log#set_level EL.Debug;
-  symbolic_to_pure_log#set_level EL.Debug;
-  pure_micro_passes_log#set_level EL.Debug;
-  pure_to_extract_log#set_level EL.Debug;
-  translate_log#set_level EL.Debug;
+  pure_utils_log#set_level EL.Warning;
+  symbolic_to_pure_log#set_level EL.Warning;
+  pure_micro_passes_log#set_level EL.Warning;
+  pure_to_extract_log#set_level EL.Warning;
+  translate_log#set_level EL.Warning;
   (* Load the module *)
   let json = Yojson.Basic.from_file filename in
   match cfim_module_of_json json with