From 4c30ce449a80bc38c1b26a83c93a8449fcaf7d57 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 25 Mar 2020 15:03:18 +0100
Subject: [PATCH] [Kernel] Adds the new option -warn-pointer-downcast.
---
src/kernel_services/plugin_entry_points/kernel.ml | 11 +++++++++++
src/kernel_services/plugin_entry_points/kernel.mli | 3 +++
2 files changed, 14 insertions(+)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 4dca12b991c..a7ffdfeb730 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 87ffd853c1c..04ef6317f0c 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" *)
--
GitLab