diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /lib/backtrace.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'lib/backtrace.ml')
-rw-r--r-- | lib/backtrace.ml | 116 |
1 files changed, 116 insertions, 0 deletions
diff --git a/lib/backtrace.ml b/lib/backtrace.ml new file mode 100644 index 00000000..b3b8bdea --- /dev/null +++ b/lib/backtrace.ml @@ -0,0 +1,116 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +type raw_frame = +| Known_location of bool (* is_raise *) + * string (* filename *) + * int (* line number *) + * int (* start char *) + * int (* end char *) +| Unknown_location of bool (*is_raise*) + +type location = { + loc_filename : string; + loc_line : int; + loc_start : int; + loc_end : int; +} + +type frame = { frame_location : location option; frame_raised : bool; } + +external get_exception_backtrace: unit -> raw_frame array option + = "caml_get_exception_backtrace" + +type t = raw_frame array list +(** List of partial raw stack frames, in reverse order *) + +let empty = [] + +let of_raw = function +| Unknown_location r -> + { frame_location = None; frame_raised = r; } +| Known_location (r, file, line, st, en) -> + let loc = { + loc_filename = file; + loc_line = line; + loc_start = st; + loc_end = en; + } in + { frame_location = Some loc; frame_raised = r; } + +let rec repr_aux accu = function +| [] -> accu +| fragment :: stack -> + let len = Array.length fragment in + let rec append accu i = + if i = len then accu + else append (of_raw fragment.(i) :: accu) (succ i) + in + repr_aux (append accu 0) stack + +let repr bt = repr_aux [] (List.rev bt) + +let push stack = match get_exception_backtrace () with +| None -> [] +| Some frames -> frames :: stack + +(** Utilities *) + +let print_frame frame = + let raise = if frame.frame_raised then "raise" else "frame" in + match frame.frame_location with + | None -> Printf.sprintf "%s @ unknown" raise + | Some loc -> + Printf.sprintf "%s @ file \"%s\", line %d, characters %d-%d" + raise loc.loc_filename loc.loc_line loc.loc_start loc.loc_end + +(** Exception manipulation *) + +let backtrace : t Exninfo.t = Exninfo.make () + +let is_recording = ref false + +let record_backtrace b = + let () = Printexc.record_backtrace b in + is_recording := b + +let get_backtrace e = + Exninfo.get e backtrace + +let add_backtrace e = + if !is_recording then + (** This must be the first function call, otherwise the stack may be + destroyed *) + let current = get_exception_backtrace () in + let info = Exninfo.info e in + begin match current with + | None -> (e, info) + | Some fragment -> + let bt = match get_backtrace info with + | None -> [] + | Some bt -> bt + in + let bt = fragment :: bt in + (e, Exninfo.add info backtrace bt) + end + else + let info = Exninfo.info e in + (e, info) + +let app_backtrace ~src ~dst = + if !is_recording then + match get_backtrace src with + | None -> dst + | Some bt -> + match get_backtrace dst with + | None -> + Exninfo.add dst backtrace bt + | Some nbt -> + let bt = bt @ nbt in + Exninfo.add dst backtrace bt + else dst |