diff options
author | Son Ho | 2022-01-05 08:43:24 +0100 |
---|---|---|
committer | Son Ho | 2022-01-05 08:43:24 +0100 |
commit | 05db1377f1b987050e58643b9bf001f62a77e303 (patch) | |
tree | 5e979eec26961ad9f8e2974fb683e2648401c24b /src/main.ml | |
parent | 31ba5d8703e1c5030744e4e2818aec2b6928e30c (diff) |
Introduce the type_context definition
Diffstat (limited to 'src/main.ml')
-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 |