diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/dune | 4 | ||||
| -rw-r--r-- | src/main.ml | 26 |
2 files changed, 27 insertions, 3 deletions
@@ -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 -> |