diff --git a/src/logging.ml b/src/logging.ml
index 215a01f2511f43a00d6430d97b4818580c4f6cd1..48652af5d04c0abacdf8d205725a2d0a8097bd8d 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -73,18 +73,28 @@ let setup style_renderer level srcs =
 
 exception Code_error
 
-let code_error ?src f =
-  Logs.err ?src f;
-  Logs.err ?src (fun fmt ->
-    fmt
-      "Unrecoverable error:@ please report@ the issue at@ \
-       https://git.frama-c.com/pub/caisar/issues");
+let code_error ~src f =
+  Logs.err ~src (fun m ->
+    let report_with_msg ?header:_ ?tags:_ fmt =
+      m
+        ("@[<v>" ^^ fmt
+       ^^ "@ @[Unrecoverable error:@ please report@ the issue at@ \
+           https://git.frama-c.com/pub/caisar/issues@]@]")
+    in
+    f report_with_msg);
   raise Code_error
 
 exception User_error
 
-let user_error ?src f =
-  Logs.err ?src f;
+let user_error ?loc f =
+  (match loc with
+  | None -> Logs.err f
+  | Some loc ->
+    Logs.err (fun m ->
+      let report_with_loc ?header:_ ?tags:_ fmt =
+        m ("@[%a:@ " ^^ fmt ^^ "@]") Why3.Loc.pp_position loc
+      in
+      f report_with_loc));
   raise User_error
 
 exception Not_implemented_yet
diff --git a/src/logging.mli b/src/logging.mli
index dc9b09ff09f34676417b893a10fbb7a5586360ca..6410b1a5911380629712fbc874a397d3808b97f6 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -39,10 +39,10 @@ val setup :
 
 val is_debug_level : Logs.src -> bool
 
-val code_error : ?src:Logs.src -> (_, unit) Logs.msgf -> 'b
+val code_error : src:Logs.src -> (_, unit) Logs.msgf -> 'b
 (** Terminate execution with a [code error] message. *)
 
-val user_error : ?src:Logs.src -> (_, unit) Logs.msgf -> 'b
+val user_error : ?loc:Why3.Loc.position -> (_, unit) Logs.msgf -> 'b
 (** Terminate execution with a [user error] message. *)
 
 val not_implemented_yet : ?src:Logs.src -> (_, unit) Logs.msgf -> 'b