Parsing of command-line arguments

3 files changed, 28 insertions, 4 deletions

diff --git a/Makefile b/Makefile
index 03444d51..a058bac8 100644
--- a/Makefile
+++ b/Makefile
@@ -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
 
diff --git a/src/dune b/src/dune
index e64c3cb1..eab08028 100644
--- a/src/dune
+++ b/src/dune
@@ -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 ->