From 0db8f2688d03d3030ed3c8e21216e8d34643302e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 16 Apr 2021 09:49:02 +0200
Subject: [PATCH] [rte] Removed -initialized-ignore, -initialized is a Kf set
---
src/plugins/rte/flags.ml | 11 ++++++-----
src/plugins/rte/flags.mli | 10 +++++-----
src/plugins/rte/options.ml | 16 ++++------------
src/plugins/rte/options.mli | 4 +---
src/plugins/rte/register.ml | 4 ++--
src/plugins/rte/visit.ml | 6 +++---
tests/rte/initialized-ignore-fct.i | 4 ++--
tests/rte/initialized.c | 2 +-
tests/rte/initialized_union.c | 4 ++--
9 files changed, 26 insertions(+), 35 deletions(-)
diff --git a/src/plugins/rte/flags.ml b/src/plugins/rte/flags.ml
index 36198afe973..d452b81ad73 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 f294c8f49d5..b36711a37e0 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 98d4a4285b2..f71174581b3 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 feda52fab77..d2d78c6e139 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 984734d10d4..75b8dba172c 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 429e058da38..d7778383f58 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 c8424d88c9c..af2e03209b9 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 3f208f11d00..ea9c6ed25e0 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 9f7b960688c..666907264d3 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 {
--
GitLab