[rte] New option: ignore functions for initialized

src/plugins/rte/options.ml

@@ -68,7 +68,17 @@ module DoInitialized =
     (struct
       let option_name = "-rte-initialized"
       let help = "when on, annotates local variables and pointers \
-                  reads with initialization tests"
+                  reads of non struct types with initialization tests \
+                  see documentation for more details."
+    end)
+
+module IgnoreInitialized =
+  Kernel_function_set
+    (struct
+      let option_name = "-rte-initialized-ignore"
+      let arg_name = "fct"
+      let help = "list of functions where initialization alarms should not be \
+                  emitted"
     end)
 
 (* annotates invalid memory access (undefined behavior) *)

src/plugins/rte/options.mli

@@ -31,6 +31,8 @@ module DoInitialized : Parameter_sig.Bool
 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

src/plugins/rte/visit.ml

@@ -51,7 +51,9 @@ class annot_visitor kf flags on_alarm = object (self)
     r
 
   method private do_initialized () =
-    flags.Flags.initialized && not (Generator.Initialized.is_computed 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)
@@ -300,7 +302,8 @@ class annot_visitor kf flags on_alarm = object (self)
             self#generate_assertion
               (Rte.lval_assertion ~read_only:Alarms.For_reading) lval
           end;
-          if self#do_initialized () && not (self#must_skip_initialized lval) then begin
+          if self#do_initialized ()
+          && not (self#must_skip_initialized lval) then begin
             Options.debug
               "exp %a is an lval: initialization of potential mem access checked"
               Printer.pp_exp exp;

tests/rte/initialized-ignore-fct.i

+/* run.config
+   OPT: -rte -rte-initialized -print
+   OPT: -rte -rte-initialized -rte-initialized-ignore f1 -print
+*/
+
+int f1(void){
+  int i = 0 ;
+  return i ;
+}
+int f2(void){
+  int i = 0 ;
+  return i ;
+}

tests/rte/oracle/initialized-ignore-fct.0.res.oracle

+[kernel] Parsing tests/rte/initialized-ignore-fct.i (no preprocessing)
+[rte] annotating function f1
+[rte] annotating function f2
+/* Generated by Frama-C */
+int f1(void)
+{
+  int i = 0;
+  /*@ assert rte: initialization: \initialized(&i); */
+  return i;
+}
+
+int f2(void)
+{
+  int i = 0;
+  /*@ assert rte: initialization: \initialized(&i); */
+  return i;
+}
+
+

tests/rte/oracle/initialized-ignore-fct.1.res.oracle

+[kernel] Parsing tests/rte/initialized-ignore-fct.i (no preprocessing)
+[rte] annotating function f1
+[rte] annotating function f2
+/* Generated by Frama-C */
+int f1(void)
+{
+  int i = 0;
+  return i;
+}
+
+int f2(void)
+{
+  int i = 0;
+  /*@ assert rte: initialization: \initialized(&i); */
+  return i;
+}
+
+