diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 18bd9157b7d7915331c72ecfdbfce059d8b4501e..3bc8e548a1098d082cc30e5127ebc8675d30b2c7 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9210,9 +9210,14 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
        * that all uses of this function will refer to the renamed
        * function *)
       addGlobalToEnv ghost n (EnvVar !currentFunctionFDEC.svar);
-      if H.mem alreadyDefined !currentFunctionFDEC.svar.vname then
-        Kernel.error ~once:true ~current:true "There is a definition already for %s" n;
-
+      H.find_opt alreadyDefined !currentFunctionFDEC.svar.vname
+      |>
+      (Option.iter
+         (fun loc ->
+            abort_context
+              "There is a definition already for %s \
+               (previous definition was at %a)."
+              n Cil_datatype.Location.pretty loc));
       H.add alreadyDefined !currentFunctionFDEC.svar.vname idloc;
 
 
diff --git a/tests/syntax/double_definition.i b/tests/syntax/double_definition.i
new file mode 100644
index 0000000000000000000000000000000000000000..96ba4263ebb0b42ddc67f774f0188c6fa7c8ce2f
--- /dev/null
+++ b/tests/syntax/double_definition.i
@@ -0,0 +1,9 @@
+/* run.config
+EXIT: 1
+OPT:
+*/
+
+void f() { }
+// error (redefinition of f), but Frama-C shouldn't
+// leave a backtrace for that...
+void f() { }
diff --git a/tests/syntax/oracle/double_definition.res.oracle b/tests/syntax/oracle/double_definition.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7e9bcf46d48381315667c98868f6671ecbe91b88
--- /dev/null
+++ b/tests/syntax/oracle/double_definition.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing double_definition.i (no preprocessing)
+[kernel] double_definition.i:9: User Error: 
+  There is a definition already for f (previous definition was at double_definition.i:6).
+  7     // error (redefinition of f), but Frama-C shouldn't
+  8     // leave a backtrace for that...
+  9     void f() { }
+             ^
+[kernel] Frama-C aborted: invalid user input.