From 0284b45ea621f1a2fbb364bf1ffffbf9884c643e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 27 Feb 2020 11:27:33 +0100
Subject: [PATCH] [Kernel] Adds the new option -warn-invalid-pointer.
---
src/kernel_services/plugin_entry_points/kernel.ml | 9 +++++++++
src/kernel_services/plugin_entry_points/kernel.mli | 3 +++
2 files changed, 12 insertions(+)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index a7ffdfeb730..d437277a6da 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1479,6 +1479,15 @@ module InvalidBool =
_Bool lvalues."
end)
+let () = Parameter_customize.set_group analysis_options
+let () = Parameter_customize.do_not_reset_on_copy ()
+module InvalidPointer =
+ False
+ (struct
+ let module_name = "InvalidPointer"
+ let option_name = "-warn-invalid-pointer"
+ let help = "generate alarms when invalid pointers are created."
+ end)
(* ************************************************************************* *)
(** {2 Sequencing options} *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 04ef6317f0c..b641349af40 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -549,6 +549,9 @@ module SpecialFloat: Parameter_sig.String
module InvalidBool: Parameter_sig.Bool
(** Behavior of option "-warn-invalid-bool" *)
+module InvalidPointer: Parameter_sig.Bool
+(** Behavior of option "-warn-invalid-pointer" *)
+
module AbsoluteValidRange: Parameter_sig.String
(** Behavior of option "-absolute-valid-range" *)
--
GitLab