From e7da100caaab8aec3040ac38debdf9131cab4b82 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 9 Oct 2024 16:00:47 +0200 Subject: [PATCH] review changes --- src/bin/common/solving_loop.ml | 10 +++++----- src/bin/common/solving_loop.mli | 7 ++++--- src/bin/js/worker_js.ml | 2 +- src/lib/structures/errors.ml | 3 --- src/lib/structures/errors.mli | 1 - 5 files changed, 10 insertions(+), 13 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 48aca8b89..10db9c475 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -32,7 +32,7 @@ module DO = D_state_option module Sy = Symbols module O = Options -exception Exit_on_error of int +exception Exit_with_code of int type solver_ctx = { ctx : Commands.sat_tdecl list; @@ -60,13 +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 raise (Exit_on_error 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; - raise (Exit_on_error code)) + raise (Exit_with_code code)) let exit_as_timeout () = fatal_error ~code:142 "timeout" @@ -257,7 +257,7 @@ let process_source ?selector_inst ~print_status src = | Errors.Error e -> recoverable_error "%a" Errors.report e; st - | Exit -> raise (Exit_on_error 0) + | Exit -> raise (Exit_with_code 0) | _ as exn -> Printexc.raise_with_backtrace exn bt in let finally ~handle_exn st e = @@ -902,4 +902,4 @@ let main () = process_source ~print_status:Frontend.print_status `Stdin else process_source ~print_status:Frontend.print_status @@ (`File path) - with Exit_on_error code -> exit code + with Exit_with_code code -> exit code diff --git a/src/bin/common/solving_loop.mli b/src/bin/common/solving_loop.mli index cbbf6e36b..03a12e862 100644 --- a/src/bin/common/solving_loop.mli +++ b/src/bin/common/solving_loop.mli @@ -25,7 +25,7 @@ (* *) (**************************************************************************) -exception Exit_on_error of int +exception Exit_with_code of int (** Exception raised to notify that [process_source] cannot continue. The integer corresponds to an error code. *) @@ -42,5 +42,6 @@ val process_source : input source [src] and call [print_status] on each answers. The hook [selector_inst] allows to track generated instantiations. - @raise Exit_on_error if a fatal error occurs. Recovarable errors - raise this exception if [Options.get_exit_on_error ()] is [true]. *) + @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/worker_js.ml b/src/bin/js/worker_js.ml index 4c8ed72c0..b86340b99 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -146,7 +146,7 @@ let main worker_id filename filecontent = Worker_interface.diagnostic = Some [Format.asprintf "%a" Errors.report e] } - | Solving_loop.Exit_on_error code -> + | Solving_loop.Exit_with_code code -> let res = Worker_interface.init_results () in let msg = Fmt.str "exit code %d" code in { res with diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml index e551599f0..e5bc26035 100644 --- a/src/lib/structures/errors.ml +++ b/src/lib/structures/errors.ml @@ -82,7 +82,6 @@ type run_error = | Unsupported_feature of string | Dynlink_error of string | Stack_underflow - | Exit_on_error of int type mode_error = | Invalid_set_option of string @@ -251,8 +250,6 @@ let report_run_error fmt = function fprintf fmt "[Dynlink] %s" s | Stack_underflow -> fprintf fmt "The stack of the assertion levels is empty" - | Exit_on_error code -> - Fmt.pf fmt "error code %d" code let report_mode_error fmt = function | Invalid_set_option s -> diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli index 60b470d27..7f1794c17 100644 --- a/src/lib/structures/errors.mli +++ b/src/lib/structures/errors.mli @@ -89,7 +89,6 @@ type run_error = | Unsupported_feature of string | Dynlink_error of string | Stack_underflow - | Exit_on_error of int (** Errors raised when performing actions forbidden in some modes. *) type mode_error =