Merge pull request #1619 from goblint/issue-1616

Print innermost backtrace mark for uncaught exception even with backtrace printing off

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
     )

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