[Kernel] Adds two warnings categories for ghost code

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
 

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