diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 4dca12b991c27963dddde65a1dce642c4c9e3016..a7ffdfeb73030844ef69826fe1814b3bdced74c7 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1440,6 +1440,17 @@ module UnsignedDowncast =
                   destination range"
     end)
 
+(* Pointer downcasts are undefined behaviors. *)
+let () = Parameter_customize.set_group analysis_options
+let () = Parameter_customize.do_not_reset_on_copy ()
+module PointerDowncast =
+  True
+    (struct
+      let module_name = "PointerDowncast"
+      let option_name = "-warn-pointer-downcast"
+      let help = "generate alarms when a pointer is converted into an integer \
+                  but may not be in the range of the destination type."
+    end)
 
 (* Not finite floats are ok, but might not always be a behavior the programmer
    wants. *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 87ffd853c1c5593cfb4b3ae4153ea6f521e000f2..04ef6317f0c2e63a44f15a244e79a31947ae9b1c 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -540,6 +540,9 @@ module SignedDowncast: Parameter_sig.Bool
 module UnsignedDowncast: Parameter_sig.Bool
 (** Behavior of option "-warn-unsigned-downcast" *)
 
+module PointerDowncast: Parameter_sig.Bool
+(** Behavior of option "-warn-pointer-downcast" *)
+
 module SpecialFloat: Parameter_sig.String
 (** Behavior of option "-warn-special-float" *)