diff options
Diffstat (limited to '')
-rw-r--r-- | src/main.ml | 40 |
1 files changed, 23 insertions, 17 deletions
diff --git a/src/main.ml b/src/main.ml index 4616aadf..f2e6eb06 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,9 +1,11 @@ open CfimOfJson open Logging open Print +open Contexts module T = Types module A = CfimAst module I = Interpreter +module C = Contexts type test = Test [@@deriving show] @@ -13,31 +15,35 @@ 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 +let usage = + Printf.sprintf + {|Aenaes: verification of Rust programs by translation Usage: %s [OPTIONS] FILE -|} Sys.argv.(0);; +|} + Sys.argv.(0) let () = - let spec = [ - ] 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 + let fail () = print_string usage; exit 1 - end; + in + Arg.parse spec + (fun f -> + if not (Filename.check_suffix f ".cfim") then ( + print_string "Unrecognized file extension"; + fail ()) + else if not (Sys.file_exists f) then ( + print_string "File not found"; + fail ()) + else filename := f) + usage; + if !filename = "" then ( + print_string usage; + exit 1); let json = Yojson.Basic.from_file !filename in match cfim_module_of_json json with | Error s -> log#error "error: %s\n" s |