Skip to content
Snippets Groups Projects
Commit e070818b authored by Andre Maroneze's avatar Andre Maroneze Committed by Patrick Baudin
Browse files

[Kernel] add wkey to warning about missing assigns

parent 9ff28151
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/kernel_internals/typing/infer_annotations.ml
+ 1
− 0
View file @ e070818b
...@@ -226,6 +226,7 @@ let populate_funspec_aux kf spec = ...@@ -226,6 +226,7 @@ let populate_funspec_aux kf spec =
let warn_if_not_builtin explicit_name name orig_name = let warn_if_not_builtin explicit_name name orig_name =
if not (is_frama_c_builtin name) then if not (is_frama_c_builtin name) then
Kernel.warning ~once:true ~current:true Kernel.warning ~once:true ~current:true
~wkey:Kernel.wkey_missing_spec
"No code nor %s assigns clause for function %a, \ "No code nor %s assigns clause for function %a, \
generating default assigns from the %s" generating default assigns from the %s"
explicit_name Kernel_function.pretty kf orig_name explicit_name Kernel_function.pretty kf orig_name
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment