From e070818b68dceb1cabe1ee969c3ce4f8f93e6337 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 9 Sep 2021 09:54:09 +0200
Subject: [PATCH] [Kernel] add wkey to warning about missing assigns
---
src/kernel_internals/typing/infer_annotations.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/kernel_internals/typing/infer_annotations.ml b/src/kernel_internals/typing/infer_annotations.ml
index b6f2e39f836..596454178f1 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
--
GitLab