diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | src/dune | 4 | ||||
| -rw-r--r-- | src/main.ml | 26 |
3 files changed, 28 insertions, 4 deletions
@@ -11,7 +11,7 @@ build-run: .PHONY: build-run-check-trace build-run-check-trace: dune build src/main.exe && \ - dune exec src/main.exe > tests/trace_current.txt && \ + dune exec src/main.exe ../charon/charon/tests/test1.cfim > tests/trace_current.txt && \ cmp tests/trace_reference.txt tests/trace_current.txt && \ rm tests/trace_current.txt @@ -8,13 +8,13 @@ :standard -safe-string -g - -dsource + ;-dsource -warn-error -9-11-33-20-21-26-27-39 )) (release (flags :standard -safe-string -g - -dsource + ;-dsource -warn-error -9-11-33-20-21-26-27-39 ))) diff --git a/src/main.ml b/src/main.ml index da8f71ff..4616aadf 100644 --- a/src/main.ml +++ b/src/main.ml @@ -13,8 +13,32 @@ let _ = show_test Test * reason, the -g option doesn't work *) let () = Printexc.record_backtrace true +let usage = Printf.sprintf {|Aenaes: verification of Rust programs by translation + +Usage: %s [OPTIONS] FILE +|} Sys.argv.(0);; + let () = - let json = Yojson.Basic.from_file "../charon/charon/tests/test1.cfim" in + let spec = [ + ] in + let spec = Arg.align spec in + let filename = ref "" in + let fail () = print_string usage; exit 1 in + Arg.parse spec (fun f -> + if not (Filename.check_suffix f ".cfim") then begin + print_string "Unrecognized file extension"; + fail () + end else if not (Sys.file_exists f) then begin + print_string "File not found"; + fail () + end else + filename := f + ) usage; + if !filename = "" then begin + print_string usage; + exit 1 + end; + let json = Yojson.Basic.from_file !filename in match cfim_module_of_json json with | Error s -> log#error "error: %s\n" s | Ok m -> |