Module IBase.Exception

The restart scheduler and biabduction use exceptions for control flow (restarts/timeouts respectively). Functions here abstract away the semantics of when an exception can be ignored.

type failure_kind =
  1. | FKtimeout
    (*

    max time exceeded

    *)
  2. | FKsymops_timeout of int
    (*

    max symop's exceeded

    *)
  3. | FKcrash of string
    (*

    uncaught exception or failed assertion

    *)

types of biabduction failure due to timeouts

val pp_failure_kind : Stdlib.Format.formatter -> failure_kind -> unit
exception Analysis_failure_exe of failure_kind

Timeout exception

val exn_not_failure : exn -> bool

check that the exception is not a biabduction timeout or restart scheduler exception

val try_finally : f:(unit -> 'a) -> finally:(unit -> unit) -> 'a

try_finally ~f ~finally executes f and then finally even if f raises an exception. Biabduction timeouts and restart scheduler exceptions are handled as necessary.