diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 94c3db9f9b4afadef401dcaceeac2eefa7444d60..c698d489a9ee9c007ef3412ba5c6bfcdb728591d 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 05cb11acdf5f56912840d17278bd154fce97b9b6..250cea5e6850fe529b08ad5c1eb167ab5d11e725 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