diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 7a28e4670df8c333f4595f31f9522f61eb8a9809..c40489e5ab1acadb17b27ffd3d965f4e19767196 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -6401,7 +6401,7 @@ and doExp local_env "Function %s is a ghost symbol. \ It cannot be used in non-ghost context. \ Did you forget a /*@@ ghost ... /?" n ; - Kernel.debug ~level:3 + Kernel.debug ~dkey:Kernel.dkey_typing_global "Calling function %s without prototype." n ; let ftype = TFun(intType, None, false, [Attr("missingproto",[])]) in