diff --git a/src/plugins/rte/flags.ml b/src/plugins/rte/flags.ml
index 36198afe973c165629266594f7690e1093b2c23f..d452b81ad736a37d46dcded3d3a4e97cfbe09dd5 100644
--- a/src/plugins/rte/flags.ml
+++ b/src/plugins/rte/flags.ml
@@ -26,7 +26,7 @@
type t = {
remove_trivial: bool;
- initialized: bool;
+ initialized: Kernel_function.Set.t ;
mem_access: bool;
div_mod: bool;
shift: bool;
@@ -44,9 +44,10 @@ type t = {
bool_value: bool;
}
-let all = {
+let all () = {
remove_trivial = true;
- initialized = true;
+ initialized =
+ Globals.Functions.fold Kernel_function.Set.add Kernel_function.Set.empty;
mem_access = true;
div_mod = true;
shift = true;
@@ -66,7 +67,7 @@ let all = {
let none = {
remove_trivial = false;
- initialized = false;
+ initialized = Kernel_function.Set.empty;
mem_access = false;
div_mod = false;
shift = false;
@@ -87,7 +88,7 @@ let none = {
(* Which annotations should be added,
from local options, or deduced from the options of RTE and the kernel *)
-let option (get : unit -> bool) = function None -> get () | Some flag -> flag
+let option get = function None -> get () | Some flag -> flag
let default
?remove_trivial
diff --git a/src/plugins/rte/flags.mli b/src/plugins/rte/flags.mli
index f294c8f49d5b3a34650919af663909c3ec8d8cd8..b36711a37e01b07ee90e856f2847359654c8d673 100644
--- a/src/plugins/rte/flags.mli
+++ b/src/plugins/rte/flags.mli
@@ -28,7 +28,7 @@
a category of alarms will be visited or not. *)
type t = {
remove_trivial: bool;
- initialized: bool;
+ initialized: Kernel_function.Set.t ;
mem_access: bool;
div_mod: bool;
shift: bool;
@@ -49,7 +49,7 @@ type t = {
(** Defaults flags are taken from the Kernel and RTE plug-in options. *)
val default :
?remove_trivial:bool ->
- ?initialized:bool ->
+ ?initialized:Kernel_function.Set.t ->
?mem_access:bool ->
?div_mod:bool ->
?shift:bool ->
@@ -67,10 +67,10 @@ val default :
?bool_value:bool ->
unit -> t
-(** All flags set to [true]. *)
-val all : t
+(** All flags set to [true], [@all] for [initialized] *)
+val all : unit -> t
-(** All flags set to [false]. *)
+(** All flags set to [false], [empty] for [initialized] *)
val none : t
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/rte/options.ml b/src/plugins/rte/options.ml
index 98d4a4285b28afad820c8e639ac20a1e630c8e29..f71174581b31229d33a658c10c2789095ed0c250 100644
--- a/src/plugins/rte/options.ml
+++ b/src/plugins/rte/options.ml
@@ -64,21 +64,13 @@ module DoFloatToInt =
(* annotates local variables and pointers read (aside from globals) initialization *)
module DoInitialized =
- False
- (struct
- let option_name = "-rte-initialized"
- let help = "when on, annotates local variables and pointers \
- reads of non struct or union types with initialization tests \
- see documentation for more details."
- end)
-
-module IgnoreInitialized =
Kernel_function_set
(struct
- let option_name = "-rte-initialized-ignore"
+ let option_name = "-rte-initialized"
let arg_name = "fct"
- let help = "list of functions where initialization alarms should not be \
- emitted"
+ let help = "annotates local variables and pointers reads of non struct \
+ or union types with initialization tests for functions in \
+ 'fct', see documentation for more details."
end)
(* annotates invalid memory access (undefined behavior) *)
diff --git a/src/plugins/rte/options.mli b/src/plugins/rte/options.mli
index feda52fab770cd161f12ab7c280e667141fa4176..d2d78c6e139f56faf130d6bc25c0ebfb93421905 100644
--- a/src/plugins/rte/options.mli
+++ b/src/plugins/rte/options.mli
@@ -27,12 +27,10 @@ module Enabled: Parameter_sig.Bool
module DoShift : Parameter_sig.Bool
module DoDivMod : Parameter_sig.Bool
module DoFloatToInt : Parameter_sig.Bool
-module DoInitialized : Parameter_sig.Bool
+module DoInitialized : Parameter_sig.Kernel_function_set
module DoMemAccess : Parameter_sig.Bool
module DoPointerCall : Parameter_sig.Bool
-module IgnoreInitialized : Parameter_sig.Kernel_function_set
-
module Trivial : Parameter_sig.Bool
module Warn : Parameter_sig.Bool
module FunctionSelection: Parameter_sig.Kernel_function_set
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 984734d10d4f48c9efec18dca89db440091b85c0..75b8dba172cb181233de116ec621dbbb86fb436c 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -28,7 +28,7 @@
function *)
let do_all_rte kf =
let flags =
- { Flags.all with
+ { (Flags.all ()) with
Flags.signed_downcast = false;
unsigned_downcast = false; }
in
@@ -38,7 +38,7 @@ let do_all_rte kf =
function *)
let do_rte kf =
let flags =
- { Flags.all with
+ { (Flags.all ()) with
Flags.unsigned_overflow = false;
signed_downcast = false;
unsigned_downcast = false; }
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 429e058da38ad2f54f3a4ea0e419532d8ab1b011..d7778383f58cd0e596b43f7e09d75669a43adb54 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -51,9 +51,8 @@ class annot_visitor kf flags on_alarm = object (self)
r
method private do_initialized () =
- flags.Flags.initialized
+ Kernel_function.Set.mem kf flags.Flags.initialized
&& not (Generator.Initialized.is_computed kf)
- && not (Options.IgnoreInitialized.mem kf)
method private do_mem_access () =
flags.Flags.mem_access && not (Generator.Mem_access.is_computed kf)
@@ -454,7 +453,8 @@ let annotate ?flags kf =
let (|||) a b = a || b in
let open Generator in
let open Flags in
- if comp Initialized.accessor flags.initialized |||
+ if comp Initialized.accessor
+ (not @@ Kernel_function.Set.is_empty flags.initialized) |||
comp Mem_access.accessor flags.mem_access |||
comp Pointer_value.accessor flags.pointer_value |||
comp Pointer_call.accessor flags.pointer_call |||
diff --git a/tests/rte/initialized-ignore-fct.i b/tests/rte/initialized-ignore-fct.i
index c8424d88c9cb88f3fbec8ea1470133893364721d..af2e03209b9f14dba64a1a48c7c00dd2a8fa6f0a 100644
--- a/tests/rte/initialized-ignore-fct.i
+++ b/tests/rte/initialized-ignore-fct.i
@@ -1,6 +1,6 @@
/* run.config
- OPT: -rte -rte-initialized -print
- OPT: -rte -rte-initialized -rte-initialized-ignore f1 -print
+ OPT: -rte -rte-initialized="@all" -print
+ OPT: -rte -rte-initialized="@all,-f1" -print
*/
int f1(void){
diff --git a/tests/rte/initialized.c b/tests/rte/initialized.c
index 3f208f11d00e1131daabd191b4af110a61bfeafd..ea9c6ed25e034a6a793d9bb3ddcc78d1bd87009e 100644
--- a/tests/rte/initialized.c
+++ b/tests/rte/initialized.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -rte -rte-initialized -warn-signed-overflow -print
+ OPT: -rte -rte-initialized="@all" -warn-signed-overflow -print
*/
struct R {
diff --git a/tests/rte/initialized_union.c b/tests/rte/initialized_union.c
index 9f7b960688c1a9ace5860925922cd5b8e7dc032c..666907264d3d2227cd1ab0c80ac51d140e3cae86 100644
--- a/tests/rte/initialized_union.c
+++ b/tests/rte/initialized_union.c
@@ -1,6 +1,6 @@
/* run.config
- OPT: -rte -rte-initialized -warn-signed-overflow -print
- OPT: -cpp-extra-args="-DEMPTY" -machdep gcc_x86_64 -rte -rte-initialized -warn-signed-overflow -print
+ OPT: -rte -rte-initialized="@all" -warn-signed-overflow -print
+ OPT: -cpp-extra-args="-DEMPTY" -machdep gcc_x86_64 -rte -rte-initialized="@all" -warn-signed-overflow -print
*/
union U {