diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 99658f1077bb93a12ba10c08a4b8eb72c4d70a5c..16ab1a0a5cb8b889b7df6868556313aaa273af74 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -664,8 +664,13 @@ let find_alarm_in_emitters tbl alarm =
 (** Converts an alarm to a code annotation. Returns the code annotation,
     whether said code annotation is new, and the table in which the code annot
     is/should be inserted. *)
-let to_annot_aux kinstr ?(loc=Kinstr.loc kinstr) alarm =
+let to_annot_aux kinstr ?loc alarm =
   (*  Kernel.debug "registering alarm %a" D.pretty alarm;*)
+  let loc = match loc, kinstr with
+    | Some l, _ -> l
+    | None, Kstmt stmt -> Stmt.loc stmt
+    | None, Kglobal -> Location.unknown
+  in
   let add alarm =
     let pred = create_predicate ~loc alarm in
     let pred = Logic_const.toplevel_predicate pred in
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index e1dd788e464816e66292b3f669c1509e55cc8294..0e02f014f613b5d8ee32410a1782e1f38d46961c 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -363,10 +363,6 @@ module Kinstr = struct
           | Kstmt s -> Stmt.pretty fmt s
       end)
 
-  let loc = function
-    | Kstmt st -> Stmt.loc st
-    | Kglobal -> assert false
-
   let kinstr_of_opt_stmt = function
     | None -> Kglobal
     | Some s -> Kstmt s
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index e0d2eb8b9b9d38d53a342d16fdcafb3e0fa496e6..e0ec107637898d4245ade58eff2fa24e337e131c 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -200,7 +200,6 @@ module Kinstr: sig
   val kinstr_of_opt_stmt: stmt option -> kinstr
   (** @since Nitrogen-20111001. *)
 
-  val loc: t -> location
 end
 
 module Label: S_with_collections_pretty with type t = label
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index 202e2e46c035d780484e2fb6775aa72ba8bf0b72..b44b715ecd4f3ee957426eb5dddf4fb77e1191f7 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -621,7 +621,7 @@ let compute_func_aux stack call_site kf init_state =
           let source =
             match call_site with
             | Kglobal -> None
-            | Kstmt _ -> Some (fst (Cil_datatype.Kinstr.loc call_site))
+            | Kstmt stmt -> Some (fst (Cil_datatype.Stmt.loc stmt))
           in
           Aorai_option.warning ?source
             "Call to %a does not follow automaton's specification. \
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index b90145463ac52c3a3064272a5e153041a46e8733..09a3b4d353b06d83d8a5a5c13396a4b28c90765f 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -252,11 +252,15 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
      specification or body according to [target]. If [-eva-show-progress] is
      true, the callstack and additional information are printed. *)
   let compute_using_spec_or_body target kinstr call state =
-    if kinstr <> Kglobal && Parameters.ValShowProgress.get () then
-      Self.feedback
-        "@[computing for function %a.@\nCalled from %a.@]"
-        Callstack.pretty_short call.callstack
-        Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc kinstr);
+    begin
+      match kinstr with
+      | Kstmt stmt when Parameters.ValShowProgress.get () ->
+        Self.feedback
+          "@[computing for function %a.@\nCalled from %a.@]"
+          Callstack.pretty_short call.callstack
+          Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc stmt)
+      | _ -> ()
+    end;
     let compute, kind =
       match target with
       | `Body (fundec, save_results) ->