Add backtrace marks for global initializers

Author: sim642

src/framework/constraints.ml

@@ -9,6 +9,15 @@ open Goblint_constraint.ConstrSys
 open GobConfig
 
 
+type Goblint_backtrace.mark += TfLocation of location
+
+let () = Goblint_backtrace.register_mark_printer (function
+    | TfLocation loc ->
+      Some ("transfer function at " ^ CilType.Location.show loc)
+    | _ -> None (* for other marks *)
+  )
+
+
 module type Increment =
 sig
   val increment: increment_data option
@@ -343,14 +352,6 @@ struct
       | Skip           -> tf_skip var edge prev_node
     end getl sidel demandl getg sideg d
 
-  type Goblint_backtrace.mark += TfLocation of location
-
-  let () = Goblint_backtrace.register_mark_printer (function
-      | TfLocation loc ->
-        Some ("transfer function at " ^ CilType.Location.show loc)
-      | _ -> None (* for other marks *)
-    )
-
   let tf var getl sidel demandl getg sideg prev_node (_,edge) d (f,t) =
     let old_loc  = !Goblint_tracing.current_loc in
     let old_loc2 = !Goblint_tracing.next_loc in

src/framework/control.ml

@@ -341,6 +341,13 @@ struct
           res'
         | _                       -> failwith "Unsupported global initializer edge"
       in
+      let transfer_func st (loc, edge) =
+        Goblint_backtrace.protect ~mark:(fun () -> Constraints.TfLocation loc) ~finally:(fun () ->
+            ()
+          ) (fun () ->
+            transfer_func st (loc, edge)
+          )
+      in
       let with_externs = do_extern_inits man file in
       (*if (get_bool "dbg.verbose") then Printf.printf "Number of init. edges : %d\nWorking:" (List.length edges);    *)
       let old_loc = !Goblint_tracing.current_loc in