Quelle exninfo.mli Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** Additional information worn by exceptions. *)

type 'a t
(** Information containing a given type. *)

type info
(** All information *)

type iexn = exn * info
(** Information-wearing exceptions *)

val make : string -> 'a t
(** Create a new piece of information. *)

val null : info
(** No information *)

val add : info -> 'a t -> 'a -> info
(** Add information to an exception. *)

val get : info -> 'a t -> 'a option
(** Get information worn by an exception. Returns [None] if undefined. *)

val info : exn -> info
(** Retrieve the information of the last exception raised. *)

type backtrace

val get_backtrace : info -> backtrace option
(** [get_backtrace info] does get the backtrace associated to info *)

val backtrace_to_string : backtrace -> string
(** [backtrace_to_string info] does get the backtrace associated to info *)

val record_backtrace : bool -> unit

val capture : exn -> iexn
(** Add the current backtrace information and other meta-data to the
    given exception.

    The intended use case is to re-raise an exception while preserving
    the meta-data:
    {[

    try foo
    with
    | Bar -> bar
    | My_exn _ as exn ->
      let (exn, info) = Exninfo.capture err in
      ...
      let info = ... in
      Exninfo.iraise (exn, info)

    | exn when CErrors.noncritical exn ->
      let iexn = Exninfo.capture err in
      ...
      Exninfo.iraise iexn

    ]}

    where [baz] should re-raise using [iraise] below.

    WARNING: any intermediate code between the [with] and the handler may
    modify the backtrace. Yes, that includes [when] clauses. Ideally, what you
    should do is something like:
    {[

    try foo
    with exn when CErrors.noncritical exn ->
      let (err, info) = Exninfo.capture exn in
      match err with
      | exception Bar -> ...
      | err -> ...

    ]}

    I admit that's a bit heavy, but there is not much to do...

*)

val iraise : iexn -> 'a
(** Raise the given enriched exception. *)

val reify : unit -> info

quality97%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.