diff --git a/src/kernel_internals/typing/infer_annotations.ml b/src/kernel_internals/typing/infer_annotations.ml index b6f2e39f836b07024ebfa3d7c0ebc93b4c31c370..596454178f1dc4f5f0d0bdff2797570f30e33d0a 100644 --- a/src/kernel_internals/typing/infer_annotations.ml +++ b/src/kernel_internals/typing/infer_annotations.ml @@ -226,6 +226,7 @@ let populate_funspec_aux kf spec = let warn_if_not_builtin explicit_name name orig_name = if not (is_frama_c_builtin name) then Kernel.warning ~once:true ~current:true + ~wkey:Kernel.wkey_missing_spec "No code nor %s assigns clause for function %a, \ generating default assigns from the %s" explicit_name Kernel_function.pretty kf orig_name