diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 52c465ab2..10db9c475 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -32,6 +32,8 @@ module DO = D_state_option module Sy = Symbols module O = Options +exception Exit_with_code of int + type solver_ctx = { ctx : Commands.sat_tdecl list; local : Commands.sat_tdecl list; @@ -58,10 +60,13 @@ let recoverable_error ?(code = 1) = | Smtlib2 _ -> Printer.print_smtlib_err "%s" msg | _ -> Printer.print_err "%s" msg in - if Options.get_exit_on_error () then exit code) + if Options.get_exit_on_error () then raise (Exit_with_code code)) let fatal_error ?(code = 1) = - Format.kasprintf (fun msg -> recoverable_error ~code "%s" msg; exit code) + Format.kasprintf + (fun msg -> + recoverable_error ~code "%s" msg; + raise (Exit_with_code code)) let exit_as_timeout () = fatal_error ~code:142 "timeout" @@ -252,7 +257,7 @@ let process_source ?selector_inst ~print_status src = | Errors.Error e -> recoverable_error "%a" Errors.report e; st - | Exit -> exit 0 + | Exit -> raise (Exit_with_code 0) | _ as exn -> Printexc.raise_with_backtrace exn bt in let finally ~handle_exn st e = @@ -892,7 +897,9 @@ let process_source ?selector_inst ~print_status src = let main () = let path = Options.get_file () in - if String.equal path "" then - process_source ~print_status:Frontend.print_status `Stdin - else - process_source ~print_status:Frontend.print_status @@ (`File path) + try + if String.equal path "" then + process_source ~print_status:Frontend.print_status `Stdin + else + process_source ~print_status:Frontend.print_status @@ (`File path) + with Exit_with_code code -> exit code diff --git a/src/bin/common/solving_loop.mli b/src/bin/common/solving_loop.mli index 62c107add..03a12e862 100644 --- a/src/bin/common/solving_loop.mli +++ b/src/bin/common/solving_loop.mli @@ -25,6 +25,10 @@ (* *) (**************************************************************************) +exception Exit_with_code of int +(** Exception raised to notify that [process_source] cannot continue. + The integer corresponds to an error code. *) + val main : unit -> unit (** Main function solve the input problem. The processed source is given by the file located at [Options.get_file ()]. *) @@ -36,4 +40,8 @@ val process_source : unit (** [process_source ?selector_inst ~print_status src] processes the input source [src] and call [print_status] on each answers. - The hook [selector_inst] allows to track generated instantiations. *) + The hook [selector_inst] allows to track generated instantiations. + + @raise Exit_with_code c with c <> 0 if a fatal error occurs. + Recovarable errors raise this exception if + [Options.get_exit_on_error ()] is [true]. *) diff --git a/src/bin/js/main_text_js.ml b/src/bin/js/main_text_js.ml index 2dba2f320..45f353b8b 100644 --- a/src/bin/js/main_text_js.ml +++ b/src/bin/js/main_text_js.ml @@ -34,11 +34,6 @@ let parse_cmdline () = with Parse_command.Exit_parse_command i -> exit i let () = - (* Currently, the main function of [Solving_loop] calls the [exit] function in - case of recoverable error, which is not supported in Javascript. We - turn off this feature as we do not support it correctly. See issue - https://github.com/OCamlPro/alt-ergo/issues/1250 *) - AltErgoLib.Options.set_exit_on_error false; parse_cmdline (); AltErgoLib.Printer.init_colors (); AltErgoLib.Printer.init_output_format (); diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index e86915d99..b86340b99 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -146,6 +146,13 @@ let main worker_id filename filecontent = Worker_interface.diagnostic = Some [Format.asprintf "%a" Errors.report e] } + | Solving_loop.Exit_with_code code -> + let res = Worker_interface.init_results () in + let msg = Fmt.str "exit code %d" code in + { res with + Worker_interface.worker_id = worker_id; + Worker_interface.status = Error msg; + } | exn -> let res = Worker_interface.init_results () in let msg = Fmt.str "Unknown error: %s" (Printexc.to_string exn) in @@ -170,7 +177,6 @@ let () = (* Extract options and set them *) let options = Worker_interface.options_from_json json_options in Options_interface.set_options options; - Options.set_exit_on_error false; (* Run the worker on the input file (filecontent) *) let filename = Option.get filename_opt in