diff options
| author | Son Ho | 2022-02-09 02:00:54 +0100 |
|---|---|---|
| committer | Son Ho | 2022-02-09 02:00:54 +0100 |
| commit | 5c9019003187f14797ba4d4514fec1cf2ac03d65 (patch) | |
| tree | e60326b2d8501b0dc695e1dbec46002fb8c89394 | |
| parent | 342a5d80381e77acb3cc451bc6e49976ccd49282 (diff) | |
Make minor modifications with regards to unit tests
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 7 |
2 files changed, 5 insertions, 4 deletions
@@ -19,7 +19,7 @@ build: .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_FILE2) -dest $(DEST_DIR) + 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 diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 5bf33677..0c77f48b 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -1026,7 +1026,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) let sg = def.signature in if sg.type_params = [] - && sg.inputs = [ unit_ty ] + && (sg.inputs = [ unit_ty ] || sg.inputs = []) && sg.outputs = [ mk_result_ty unit_ty ] then ( (* Add a break before *) @@ -1045,8 +1045,9 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "("; let fun_name = ctx_get_local_function def.def_id def.back_id ctx in F.pp_print_string fmt fun_name; - F.pp_print_space fmt (); - F.pp_print_string fmt "()"; + if sg.inputs <> [] then ( + F.pp_print_space fmt (); + F.pp_print_string fmt "()"); F.pp_print_space fmt (); F.pp_print_string fmt "="; F.pp_print_space fmt (); |