From f7184c06244e8919638a3870a7922fd37a1e817b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 4 Nov 2024 11:08:17 +0200 Subject: [PATCH] Print innermost backtrace mark for uncaught exception even with backtrace printing off --- src/util/backtrace/goblint_backtrace.ml | 9 ++++++++- src/util/backtrace/goblint_backtrace.mli | 5 +++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/util/backtrace/goblint_backtrace.ml b/src/util/backtrace/goblint_backtrace.ml index 513753bddb..21d150a470 100644 --- a/src/util/backtrace/goblint_backtrace.ml +++ b/src/util/backtrace/goblint_backtrace.ml @@ -76,12 +76,19 @@ let print_marktrace oc e = Printf.fprintf oc "Marked with %s\n" (mark_to_string m) ) ms +let print_innermost_mark oc e = + match find_marks e with + | m :: _ -> Printf.fprintf oc "Marked with %s\n" (mark_to_string m) + | [] -> () + let () = Printexc.set_uncaught_exception_handler (fun e bt -> (* Copied & modified from Printexc.default_uncaught_exception_handler. *) Printf.eprintf "Fatal error: exception %s\n" (Printexc.to_string e); (* nosemgrep: print-not-logging *) if Printexc.backtrace_status () then - print_marktrace stderr e; + print_marktrace stderr e + else + print_innermost_mark stderr e; Printexc.print_raw_backtrace stderr bt; flush stderr ) diff --git a/src/util/backtrace/goblint_backtrace.mli b/src/util/backtrace/goblint_backtrace.mli index e53bfd826a..ee7052122e 100644 --- a/src/util/backtrace/goblint_backtrace.mli +++ b/src/util/backtrace/goblint_backtrace.mli @@ -32,5 +32,10 @@ val print_marktrace: out_channel -> exn -> unit Used by default for uncaught exceptions. *) +val print_innermost_mark: out_channel -> exn -> unit +(** Print innermost mark of an exception. + + Used by default for uncaught exceptions. *) + val find_marks: exn -> mark list (** Find all marks of an exception. *)