diff options
| -rw-r--r-- | Makefile | 19 | ||||
| -rw-r--r-- | src/main.ml | 28 |
2 files changed, 16 insertions, 31 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) 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 |