From c6d7c38846869f88a8df62c86f50c0b1f3f86c35 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 6 Sep 2019 10:45:24 +0200
Subject: [PATCH] [Kernel] Adds two warnings categories for ghost code

---
 src/kernel_services/plugin_entry_points/kernel.ml  | 6 ++++++
 src/kernel_services/plugin_entry_points/kernel.mli | 6 ++++++
 2 files changed, 12 insertions(+)

diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 94c3db9f9b4..c698d489a9e 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -132,6 +132,12 @@ let dkey_visitor = register_category "visitor"
 let wkey_annot_error = register_warn_category "annot-error"
 let () = set_warn_status wkey_annot_error Log.Wabort
 
+let wkey_ghost_bad_non_ghost = register_warn_category "ghost:bad-non-ghost"
+let () = set_warn_status wkey_ghost_bad_non_ghost Log.Werror
+
+let wkey_ghost_bad_use = register_warn_category "ghost:bad-use"
+let () = set_warn_status wkey_ghost_bad_use Log.Werror
+
 let wkey_acsl_float_compare = register_warn_category "acsl-float-compare"
 let () = set_warn_status wkey_acsl_float_compare Log.Winactive
 
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 05cb11acdf5..250cea5e685 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -130,6 +130,12 @@ val dkey_visitor: category
 val wkey_annot_error: warn_category
 (** error in annotation. If only a warning, annotation will just be ignored. *)
 
+val wkey_ghost_bad_non_ghost: warn_category
+(** error in non ghost code related to the use of ghost elements *)
+
+val wkey_ghost_bad_use: warn_category
+(** error in ghost code *)
+
 val wkey_acsl_float_compare: warn_category
 
 val wkey_drop_unused: warn_category
-- 
GitLab