[Kernel] Adds the new option -warn-pointer-downcast.

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. *)

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" *)