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. *)