Handling errors at command line parsing

src/bin/common/parse_command.ml

@@ -37,13 +37,21 @@ exception Error of bool * string
 (* Exception used to exit with corresponding retcode *)
 exception Exit_parse_command of int
 
+let pretty_error msg =
+  match Options.get_output_format () with
+  | Smtlib2 -> Format.asprintf "; %s" msg
+  | _ -> msg
+
 let instantiation_heuristic_parser = function
   | "normal" -> Ok INormal
   | "auto" -> Ok IAuto
   | "greedy" -> Ok IGreedy
   | s ->
-    Error (`Msg ("Option --instantiation-heuristic does not accept\
-                  the argument \"" ^ s))
+    let msg =
+      Format.sprintf "Option --instantiation-heuristic does not accept the \
+                      argument %s" s
+    in
+    Error (`Msg (pretty_error msg))
 
 let instantiation_heuristic_to_string = function
   | INormal -> "normal"
@@ -73,8 +81,11 @@ let format_parser s =
     Ok (List.assoc s formats_list)
   with
     Not_found ->
-    Error (`Msg (Format.sprintf
-                   "The format %s is not accepted as input/output" s))
+    let msg =
+      Format.sprintf
+        "The format %s is not accepted as input/output" s
+    in
+    Error (`Msg (pretty_error msg))
 
 let format_to_string = function
   | Native -> "native"
@@ -91,9 +102,13 @@ let model_type_parser = function
   | "value" -> Ok Value
   | "constraints" -> Ok Constraints
   | s ->
-    Error (`Msg (Format.sprintf
-                   "The model kind %s is invalid. Only \"value\" and \
-                    \"constraints\" are allowed" s))
+    let msg =
+      Format.sprintf
+        "The model kind %s is invalid. Only \"value\" and \"constraints\" are \
+         allowed"
+        s
+    in
+    Error (`Msg (pretty_error msg))
 
 let model_type_printer fmt format =
   Format.fprintf fmt "%s"
@@ -275,8 +290,13 @@ let mk_case_split_opt case_split_policy enable_adts_cs max_split
     | "after-theory-assume" -> Ok(Util.AfterTheoryAssume)
     | "before-matching" -> Ok(Util.BeforeMatching)
     | "after-matching" -> Ok(Util.AfterMatching)
-    | _ -> Error ("Bad value '" ^ case_split_policy ^
-                  "' for option --case-split-policy")
+    | _ ->
+      let msg =
+        Format.sprintf
+          "Bad value '%s' for option --case-split-policy"
+          case_split_policy
+      in
+      Error (pretty_error msg)
   in
   let max_split = Numbers.Q.from_string max_split in
   match res with
@@ -354,7 +374,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
     | None -> d
   in
   if steps_bound < -1 then
-    `Error (false, "--steps-bound argument should be positive")
+    `Error (false, pretty_error "--steps-bound argument should be positive")
   else
     let fm_cross_limit = Numbers.Q.from_string fm_cross_limit in
     let timelimit = set_limit timelimit 0. in
@@ -473,9 +493,14 @@ let halt_opt version_info where =
     let res = match w with
       | "plugins" -> `Ok Config.plugins_locations
       | "preludes" -> `Ok Config.preludes_locations
-      | _ -> `Error
-               ("Option --where does not accept the argument \"" ^ w ^
-                "\"\nAccepted options are plugins or preludes")
+      | _ ->
+        let msg =
+          Format.sprintf
+            "Option --where does not accept the argument %s \"\nAccepted \
+             options are plugins or preludes"
+            w
+        in
+        `Error msg
     in
     match res with
     | `Ok paths ->
@@ -498,8 +523,9 @@ let halt_opt version_info where =
     | Some w -> handle_where w; `Ok true
     | None -> if version_info then (handle_version_info version_info; `Ok true)
       else `Ok false
-  with Failure f -> `Error (false, f)
-     | Error (b, m) -> `Error (b, m)
+  with
+  | Failure f -> `Error (false, pretty_error f) (* S: dead code? *)
+  | Error (b, m) -> `Error (b, pretty_error m)
 
 let get_verbose_t =
   let doc = "Set the verbose mode." in
@@ -639,7 +665,8 @@ let parse_execution_opt =
         Ok ()
       with
         Errors.Error e ->
-        Error (Format.asprintf "%a" Errors.report e)
+        let err_str = Format.asprintf "%a" Errors.report e in
+        Error (pretty_error err_str)
     in
     let load_parsers verbose paths =
       List.fold_left
@@ -657,10 +684,11 @@ let parse_execution_opt =
   in
 
   let preludes =
-    let parse_prelude p =
+    let parse_prelude p=
       if Sys.file_exists p then
         if Sys.is_directory p then
-          Fmt.error "'%s' is a directory" p
+          let msg = pretty_error (Format.sprintf "'%s' is a directory" p) in
+          ((Error msg) : _ result)
         else
           Ok p
       else
@@ -683,10 +711,12 @@ let parse_execution_opt =
 
           Ok p'
         | None ->
-          Error (
+          let msg =
             Format.asprintf
               "cannot load prelude '%s': no such file"
-              p)
+              p
+          in
+          Error (pretty_error msg)
     in
     let prelude =
       Arg.(conv' (parse_prelude, conv_printer string))
@@ -966,8 +996,10 @@ let parse_output_opt =
         | "tableaux-CDCL" | "Tableaux-cdcl" ->
           Ok Util.Tableaux_CDCL
         | sat_solver ->
-          Error ("Args parsing error: unkown SAT solver " ^ sat_solver)
-
+          let msg =
+            Format.sprintf "Args parsing error: unkown SAT solver %s" sat_solver
+          in
+          Error (pretty_error msg)
       in
       Arg.(conv' (parse, Util.pp_sat_solver))
     in
@@ -1294,7 +1326,7 @@ let parse_theory_opt =
             "'inequalities' reasoner (FM module)";
           Ok ()
         with Errors.Error e ->
-          Error (Format.asprintf "%a" Errors.report e)
+          Error (pretty_error (Format.asprintf "%a" Errors.report e))
     in
     let arg =
       let doc =
@@ -1404,12 +1436,16 @@ let parse_theory_opt =
     let preludes enable_theories disable_theories =
       let theories = Theories.default in
       let rec aux th en dis =
-        let theories =
+        let theories : _ result =
           match en, dis with
           | _ :: _, [] -> aux (List.rev_append en th) [] []
           | e :: _, d :: _ when e = d ->
-            Fmt.error_msg "theory prelude '%a' cannot be both enabled and
-            disabled" Theories.pp e
+            let msg =
+              Format.asprintf
+                "theory prelude '%a' cannot be both enabled and disabled"
+                Theories.pp
+                e
+            in Error (`Msg (pretty_error msg))
           | e :: en, d :: _ when e < d -> aux (e :: th) en dis
           | _ , d :: dis -> aux (List.filter ((<>) d) th) en dis
           | [], [] -> Ok th
@@ -1423,7 +1459,9 @@ let parse_theory_opt =
             ) dis then
             Ok Theories.(Prelude Nra :: Prelude Ria :: theories)
           else
-            Fmt.error_msg "theory prelude fpa requires both ria and nra"
+            Error (
+              `Msg (pretty_error "theory prelude fpa requires both ria and nra")
+            )
         else Ok th
       in
       aux

src/bin/common/solving_loop.ml

@@ -56,15 +56,14 @@ let custom_error
     err_code
     (msg : ('a, Format.formatter, unit, unit, unit, a) format6)
   : 'a =
-  let pp_reporter =
-    match Options.get_output_format () with
-    | Options.Smtlib2 -> Printer.print_smtlib_err ~flushed:true
-    | _ ->
-      Printer.print_err ~flushed:true ~header:true ~error:true
-  in
   Format.kasprintf
     ( fun msg ->
-        if msg <> "" then pp_reporter "%s" msg;
+        let () =
+          if msg <> "" then
+            match Options.get_output_format () with
+            | Smtlib2 -> Printer.print_smtlib_err "%s" msg
+            | _ -> Printer.print_err "%s" msg
+        in
         if Options.get_exit_on_error () then
           exit err_code
         else

src/lib/structures/errors.ml

@@ -240,24 +240,20 @@ let report_run_error fmt = function
 
 let report fmt = function
   | Parser_error s ->
-    Options.pp_comment fmt
-      (Format.sprintf "Parser Error: %s" s);
+    Format.fprintf fmt "Parser Error: %s" s;
   | Lexical_error (l,s) ->
     Loc.report fmt l;
-    Options.pp_comment fmt
-      (Format.sprintf "Lexical Error: %s" s);
+    Format.fprintf fmt "Lexical Error: %s" s;
   | Syntax_error (l,s) ->
     Loc.report fmt l;
-    Options.pp_comment fmt
-      (Format.sprintf "Syntax Error: %s" s);
+    Format.fprintf fmt "Syntax Error: %s" s;
   | Typing_error (l,e) ->
     Loc.report fmt l;
-    Options.pp_comment fmt "Typing Error: ";
+    Format.fprintf fmt "Typing Error: ";
     report_typing_error fmt e
   | Run_error e ->
-    Options.pp_comment fmt "Fatal Error: ";
+    Format.fprintf fmt "Fatal Error: ";
     report_run_error fmt e
   | Dolmen_error (code, descr) ->
-    Options.pp_comment fmt
-      (Format.sprintf "Error %s (code %i)" descr code);
+    Format.fprintf fmt "Error %s (code %i)" descr code;
   | Warning_as_error -> ()

tests/smtlib/testfile-push-pop1.err.dolmen.expected

@@ -2,3 +2,4 @@
 unknown
 
 unknown
+(error "Error on typing errors (code 4)")