Parsing of command-line arguments

1 files changed, 25 insertions, 1 deletions

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 ->