Add unit tests for CLI parsing

src/params.ml

@@ -102,7 +102,7 @@ type exec = executable ref
 let path_prefix =
   sprintf "PATH='%s';" Paths.backend_path_string
 
-let get_exec e =
+let get_exec err e =
   match !e with
   | Unchecked (exec, cmd, vers) ->
     (*
@@ -131,7 +131,7 @@ let get_exec e =
           else "."
         in
         let msg = msg1 ^ msg2 in
-        eprintf "%s" msg;
+        Format.fprintf err "%s" msg;
         e := NotFound msg;
         failwith msg;
      end;
@@ -450,14 +450,14 @@ let stats        = ref false
 
 let solve_cmd cmd file =
   if Sys.os_type = "Cygwin" then
-    sprintf "file=%s; winfile=\"`cygpath -a -w \"%s\"`\"; %s" file file (get_exec cmd)
+    sprintf "file=%s; winfile=\"`cygpath -a -w \"%s\"`\"; %s" file file (get_exec Format.err_formatter cmd)
   else
-    sprintf "file=%s; %s" file (get_exec cmd)
+    sprintf "file=%s; %s" file (get_exec Format.err_formatter cmd)
 
 
-let external_tool_config force (name, tool) =
+let external_tool_config (err : Format.formatter) force (name, tool) =
   if force then begin
-    try ignore (get_exec tool) with Failure _ -> ()
+    try ignore (get_exec err tool) with Failure _ -> ()
   end;
   match !tool with
   | Checked (cmd, []) ->
@@ -470,7 +470,7 @@ let external_tool_config force (name, tool) =
   | _ -> []
 
 
-let configuration toolbox force =
+let configuration err toolbox force =
   let library_path = (match stdlib_path with
   | Some path -> "\"" ^ (String.escaped path) ^ "\"";
   | None -> "N/A")
@@ -494,7 +494,7 @@ let configuration toolbox force =
           first_line :: mid_lines @ [last_line]
         end
       end
-    @ List.flatten (List.map (external_tool_config force)
+    @ List.flatten (List.map (external_tool_config err force)
                              [("Isabelle", isabelle);
                               ("zenon", zenon);
                               ("CVC4", cvc4);
@@ -517,17 +517,17 @@ let configuration toolbox force =
   header @ lines @ footer
 
 
-let printconfig force =
-  String.concat "\n" (configuration false force)
+let printconfig err force =
+  String.concat "\n" (configuration err false force)
 
 let print_config_toolbox force =
-  String.concat "\n" (configuration true force)
+  String.concat "\n" (configuration Format.err_formatter true force)
 
 
 let zenon_version = ref None
 
 let check_zenon_ver () =
-  let zen = get_exec zenon in
+  let zen = get_exec Format.err_formatter zenon in
   match get_version zenon with
   | [] -> ()
   | ret :: _ ->
@@ -543,7 +543,7 @@ let get_zenon_verfp () = if !zenon_version = None then check_zenon_ver ();
 let isabelle_version = ref None
 
 let check_isabelle_ver () =
-  (try ignore (get_exec isabelle) with Failure _ -> ());
+  (try ignore (get_exec Format.err_formatter isabelle) with Failure _ -> ());
   match get_version isabelle with
   | [] -> ()
   | ret :: _ ->

src/params.mli

@@ -66,7 +66,7 @@ val safefp: bool ref
 val fp_deb: bool ref
 
 (* util/util.ml *)
-val configuration: bool -> bool -> string list
+val configuration: Format.formatter -> bool -> bool -> string list
 
 (* module/save.ml *)
 val stdlib_search_paths : string list
@@ -97,7 +97,7 @@ val suppress_all: bool ref
 val set_smt_logic: string -> unit
 val set_smt_solver: string -> unit
 val set_tlapm_cache_dir: string -> unit
-val printconfig: bool -> string
+val printconfig: Format.formatter -> bool -> string
 val print_config_toolbox: bool -> string
 val check_zenon_ver: unit -> unit
 val fpf_out: string option ref

src/tlapm_args.ml

@@ -6,11 +6,9 @@ open Ext
 open Params
 
 
-let show_config = ref false
-let show_version () =
-  print_endline (rawversion ()) ;
-  exit 0
-
+let show_version formatter terminate =
+  Format.fprintf formatter "%s\n" (rawversion ());
+  terminate 0
 
 let set_debug_flags flgs =
   let flgs = Ext.split flgs ',' in
@@ -52,24 +50,23 @@ let set_default_method meth =
   with Failure msg -> raise (Arg.Bad ("--method: " ^ msg))
 
 
-(* FIXME use Arg.parse instead *)
-let parse_args args opts mods usage_fmt =
+let parse_args executable_name args opts mods usage_fmt err terminate =
   try
-    Arg.parse_argv (Array.of_list args) opts (fun mfile -> mods := mfile :: !mods)
-      (Printf.sprintf usage_fmt (Filename.basename Sys.executable_name))
+    Arg.current := 0;
+    Arg.parse_argv args opts (fun mfile -> mods := mfile :: !mods)
+      (Printf.sprintf usage_fmt (Filename.basename executable_name))
   with Arg.Bad msg ->
-    print_endline msg ;
-    flush stdout ;
-    exit 2
+    Format.fprintf err "%s\n" msg;
+    terminate 2
 
-let show_where () =
+let show_where out terminate =
   match stdlib_path with
   | Some path  ->
-    Printf.printf "%s\n" path;
-    exit 0
+    Format.fprintf out "%s\n" path;
+    terminate 0
   | None ->
-    Printf.printf "N/A\n";
-    exit 1
+    Format.fprintf out "N/A\n";
+    terminate 1
 
 let set_nofp_start s =
   nofp_sl := s
@@ -134,7 +131,8 @@ let quote_if_needed s =
   end
 
 
-let init () =
+let init ?(out=Format.std_formatter) ?(err=Format.err_formatter) ?(terminate=exit) (executable_name : string) (args : string array) =
+  let show_config = ref false in
   let mods = ref [] in
   let helpfn = ref (fun () -> ()) in
   let show_help () = !helpfn () in
@@ -147,11 +145,11 @@ let init () =
     blank;
     "--help", Arg.Unit show_help, " show this help message and exit" ;
     "-help", Arg.Unit show_help, " (same as --help)" ;
-    "--version", Arg.Unit show_version, " show version number and exit" ;
+    "--version", Arg.Unit (fun () -> show_version out terminate), " show version number and exit" ;
     "--verbose", Arg.Set verbose, " produce verbose messages" ;
     "-v", Arg.Set verbose, " (same as --verbose)" ;
     blank;
-    "--where", Arg.Unit show_where,
+    "--where", Arg.Unit (fun () -> show_where out terminate),
                " show location of standard library and exit" ;
     "--config", Arg.Set show_config, " show configuration and exit" ;
     "--summary", Arg.Set summary,
@@ -245,44 +243,44 @@ let init () =
     format_of_string "Usage: %s <options> FILE ...\noptions are:"
   in
   helpfn := begin fun () ->
-    Arg.usage opts
-      (Printf.sprintf usage_fmt (Filename.basename Sys.executable_name)) ;
-    exit 0
+    Arg.usage_string opts
+      (Printf.sprintf usage_fmt (Filename.basename executable_name))
+      |> Format.fprintf err "%s";
+    terminate 0
   end ;
-  let args = Array.to_list Sys.argv in
-  parse_args args opts mods usage_fmt ;
+  parse_args executable_name args opts mods usage_fmt err terminate;
   if !show_config || !verbose then begin
-    print_endline (printconfig true) ;
-    flush stdout
+    Format.fprintf out "%s\n" (printconfig err true);
   end ;
-  if !show_config then exit 0 ;
+  if !show_config then terminate 0 ;
   if !mods = [] then begin
-    Arg.usage opts
+    Arg.usage_string opts
       (Printf.sprintf "Need at least one module file.\n\n\
                        Usage: %s <options> FILE ...\noptions are:"
-         (Filename.basename Sys.executable_name)) ;
-    exit 2
+         (Filename.basename executable_name))
+         |> Format.fprintf err "%s";
+    terminate 2
   end ;
   if !summary then begin
     suppress_all := true ;
     check := false ;
   end ;
   check_zenon_ver () ;
   if !Params.toolbox then begin
-    Printf.printf "\n\\* TLAPM version %s\n"
+    Format.fprintf out "\n\\* TLAPM version %s\n"
                   (Params.rawversion ());
     let tm = Unix.localtime (Unix.gettimeofday ()) in
-    Printf.printf "\\* launched at %04d-%02d-%02d %02d:%02d:%02d"
+    Format.fprintf out "\\* launched at %04d-%02d-%02d %02d:%02d:%02d"
                   (tm.Unix.tm_year + 1900) (tm.Unix.tm_mon + 1) tm.Unix.tm_mday
                   tm.Unix.tm_hour tm.Unix.tm_min tm.Unix.tm_sec;
-    Printf.printf " with command line:\n\\*";
-    Array.iter (fun s -> Printf.printf " %s" (quote_if_needed s)) Sys.argv;
-    Printf.printf "\n\n%!"
+    Format.fprintf out " with command line:\n\\*";
+    Array.iter (fun s -> Format.fprintf out " %s" (quote_if_needed s)) args;
+    Format.fprintf out "\n\n%!"
   end;
   if !use_stdin && (List.length !mods) <> 1 then begin
     Arg.usage opts
       "Exactly 1 module has to be specified if TLAPM is invoked with\
        the --stdin option." ;
-    exit 2
+    terminate 2
   end;
   !mods

src/tlapm_args.mli

@@ -2,4 +2,11 @@
 
 Copyright (C) 2011  INRIA and Microsoft Corporation
 *)
-val init: unit -> string list
+
+(** Given the executable name and an array of command-line arguments, parses
+    those arguments then either sets associated values in the Params module
+    or directly takes action such as printing out file contents or deleting
+    directories. Returns a list of files for proof checking. The optional
+    arguments are used for unit tests.
+*)
+val init: ?out:Format.formatter -> ?err:Format.formatter -> ?terminate:(int -> unit) -> string -> string array -> string list

src/tlapm_lib.ml

@@ -586,9 +586,9 @@ let init () =
   Printexc.record_backtrace true;
   Format.pp_set_max_indent Format.err_formatter 35;
   if Params.debugging "main" then
-    main (Tlapm_args.init ())
+    main (Tlapm_args.init Sys.executable_name Sys.argv)
   else
-    try main (Tlapm_args.init ()) with
+    try main (Tlapm_args.init Sys.executable_name Sys.argv) with
     | Errors.Fatal ->
        Util.eprintf "tlapm: Exiting because of the above error.";
        exit 0;

src/util/util.ml

@@ -117,7 +117,7 @@ let bug ?at msg =
       "Please file a bug report, including as much information" ;
       "as you can. Mention the following in your report: " ;
       "" ]
-      @ Params.configuration false false
+      @ Params.configuration Format.err_formatter false false
     in
     String.concat "\n" lines ^ "\n"
   in