[rte] New initialized behavior

- warns only on fundamental types reads

src/plugins/rte/rte.ml

@@ -106,50 +106,22 @@ let lval_assertion ~read_only ~remove_trivial ~on_alarm lv =
 
 (* assertion for lvalue initialization *)
 let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
-  let rec check_array_initialized default off typ in_struct l =
-    match off with
-    | NoOffset ->
-      begin
-        match typ with
-        | TComp({cstruct = false; cfields; cname} ,_,_) ->
-          (match cfields with
-           | None ->
-             Options.fatal
-               "Access to an object of undefined union %a"
-               Printer.pp_varname cname
-           | Some [] -> () (* empty union, supported by gcc with size 0.
-                              Trivially initialized. *)
-           | Some l ->
-             let llv =
-               List.map
-                 (fun fi -> Cil.addOffsetLval (Field (fi, NoOffset)) lv) l
-             in
-             if default then
-               on_alarm ~invalid:false (Alarms.Uninitialized_union llv))
-        | _ ->
-          if default then
-            on_alarm ~invalid:false (Alarms.Uninitialized lv)
-      end
-    | Field (fi, off) ->
-      (* Mark that we went through a struct field, then recurse *)
-      check_array_initialized default off fi.ftype true l
-    | Index (_e, off) ->
-      match Cil.unrollType typ with
-      | TArray (bt, Some _size, _, _) ->
-        check_array_initialized true off bt in_struct l
-      | TArray (bt, None, _, _) -> check_array_initialized true off bt in_struct l
-      | _ -> assert false
-  in
-
+  let typ = Cil.typeOfLval lv in
   match lv with
-  | Var vi , off ->
-    let loc = fst vi.vdecl in
-    let ignored_cases = vi.vglob || vi.vformal || vi.vtemp in
-    check_array_initialized (not ignored_cases) off vi.vtype false loc
-  | (Mem e as lh), off ->
-    let loc = fst e.eloc in
-    if not (Cil.isFunctionType (Cil.typeOfLval lv)) then
-      check_array_initialized true off (Cil.typeOfLhost lh) false loc
+  | Var vi, NoOffset ->
+    (** Note: here [lv] has structure/union type or fundamental type.
+        We exclude structure and unions. And for fundamental types:
+        - globals (initialized and then only written with initialized values)
+        - formals (checked at function call)
+        - temporary variables (initialized during AST normalization)
+    *)
+    if not (vi.vglob || vi.vformal || vi.vtemp)
+    && not (Cil.isStructOrUnionType typ)
+    then
+      on_alarm ~invalid:false (Alarms.Uninitialized lv)
+  | _ ->
+    if not (Cil.isFunctionType typ || Cil.isStructOrUnionType typ) then
+      on_alarm ~invalid:false (Alarms.Uninitialized lv)
 
 (* assertion for unary minus signed overflow *)
 let uminus_assertion ~remove_trivial ~on_alarm exp =

src/plugins/rte/visit.ml

@@ -139,12 +139,7 @@ class annot_visitor kf flags on_alarm = object (self)
       Cil.ChangeDoChildrenPost (s', fun _ -> s)
     | _ -> Cil.DoChildren
 
-  method private treat_call ret_opt args =
-    let check_arg = function
-      | { enode = Lval lv } when Cil.isStructOrUnionType (Cil.typeOfLval lv) ->
-        self#mark_to_skip_initialized lv
-      | _ -> ()
-    in List.iter check_arg args ;
+  method private treat_call ret_opt =
     match ret_opt, self#do_mem_access () with
     | None, _ | Some _, false -> ()
     | Some ret, true ->
@@ -188,7 +183,7 @@ class annot_visitor kf flags on_alarm = object (self)
       if is_builtin
       then Cil.SkipChildren
       else begin
-        self#treat_call ret_opt argl;
+        self#treat_call ret_opt;
         (* Alarm if the call is through a pointer. Done in DoChildrenPost to get a
            more pleasant ordering of annotations. *)
         let do_ptr () =
@@ -200,7 +195,7 @@ class annot_visitor kf flags on_alarm = object (self)
         Cil.DoChildrenPost (fun res -> do_ptr (); res)
       end
     | Local_init (v,ConsInit(f,args,kind),loc) ->
-      let do_call lv _e args _loc = self#treat_call lv args in
+      let do_call lv _e _args _loc = self#treat_call lv in
       Cil.treat_constructor_as_func do_call v f args kind loc;
       Cil.DoChildren
     | Local_init (v,AssignInit (SingleInit _),_) ->

tests/rte/initialized.c

@@ -163,7 +163,7 @@ int main() {
   v = p.val;
   v = p.tq[i0][i1].v;
 
-  /** Note: Frama-C is stricter than ISO C : potentiel indeterminate values are
+  /** Note: Frama-C is stricter than ISO C : potential indeterminate values are
    *  considered as alarms even for types without trap representation.
    */
   c1 = c2;

tests/rte/oracle/initialized.res.oracle

@@ -85,9 +85,10 @@ int f(struct P ***pppp_0, struct P **ppp_0, struct P *pp_0, struct P p_0,
   /*@ assert rte: index_bound: i3_0 < 5; */
   /*@ assert rte: initialization: \initialized(&p_0.id[i3_0]); */
   p_0.id[i1_0] = p_0.id[i3_0];
+  /*@ assert rte: initialization: \initialized(&p_0.next); */
   /*@ assert rte: mem_access: \valid_read(p_0.next); */
-  /*@ assert rte: initialization: \initialized(p_0.next); */
   struct P np = *(p_0.next);
+  /*@ assert rte: initialization: \initialized(&p_0.next); */
   struct P *npp = p_0.next;
   /*@ assert rte: initialization: \initialized(&npp); */
   p_0.next = npp;
@@ -189,6 +190,7 @@ int f(struct P ***pppp_0, struct P **ppp_0, struct P *pp_0, struct P p_0,
         \initialized(&((p_0.nexts[i1_0][i2_0])->nexts[i3_0][*i_0])->id[i4_0]);
   */
   v_0 = ((p_0.nexts[i1_0][i2_0])->nexts[i3_0][*i_0])->id[i4_0];
+  /*@ assert rte: initialization: \initialized(&p_0.q.v); */
   v_0 = p_0.q.v;
   /*@ assert rte: index_bound: 0 ≤ i4_0; */
   /*@ assert rte: index_bound: i4_0 < 12; */
@@ -225,6 +227,7 @@ int f(struct P ***pppp_0, struct P **ppp_0, struct P *pp_0, struct P p_0,
   /*@ assert rte: mem_access: \valid_read(&pp_0->tq[i3_0][i1_0].v); */
   /*@ assert rte: initialization: \initialized(&pp_0->tq[i3_0][i1_0].v); */
   v_0 = pp_0->tq[i3_0][i1_0].v;
+  /*@ assert rte: initialization: \initialized(&p_0.znexts); */
   /*@ assert rte: mem_access: \valid_read(p_0.znexts + i0_0); */
   /*@ assert rte: initialization: \initialized(p_0.znexts + i0_0); */
   /*@ assert rte: mem_access: \valid_read(*(p_0.znexts + i0_0) + i1_0); */
@@ -243,7 +246,6 @@ int f(struct P ***pppp_0, struct P **ppp_0, struct P *pp_0, struct P p_0,
   /*@ assert rte: index_bound: i0_0 < 10; */
   /*@ assert rte: index_bound: 0 ≤ i1_0; */
   /*@ assert rte: index_bound: i1_0 < 11; */
-  /*@ assert rte: initialization: \initialized(&p_0.tq[i0_0][i1_0]); */
   q_0 = p_0.tq[i0_0][i1_0];
   /*@ assert rte: index_bound: 0 ≤ i0_0; */
   /*@ assert rte: index_bound: i0_0 < 10; */
@@ -258,6 +260,7 @@ int f(struct P ***pppp_0, struct P **ppp_0, struct P *pp_0, struct P p_0,
   /*@ assert rte: mem_access: \valid_read(&pp_0->val); */
   /*@ assert rte: initialization: \initialized(&pp_0->val); */
   v_0 = pp_0->val;
+  /*@ assert rte: initialization: \initialized(&p_0.val); */
   v_0 = p_0.val;
   /*@ assert rte: index_bound: 0 ≤ i0_0; */
   /*@ assert rte: index_bound: i0_0 < 10; */
@@ -329,9 +332,10 @@ int main(void)
   /*@ assert rte: index_bound: i3 < 5; */
   /*@ assert rte: initialization: \initialized(&p.id[i3]); */
   p.id[i1] = p.id[i3];
+  /*@ assert rte: initialization: \initialized(&p.next); */
   /*@ assert rte: mem_access: \valid_read(p.next); */
-  /*@ assert rte: initialization: \initialized(p.next); */
   struct P np = *(p.next);
+  /*@ assert rte: initialization: \initialized(&p.next); */
   struct P *npp = p.next;
   /*@ assert rte: initialization: \initialized(&p.id[3]); */
   v = p.id[3];
@@ -422,6 +426,7 @@ int main(void)
         \initialized(&((p.nexts[i1][i2])->nexts[i3][*i])->id[i4]);
   */
   v = ((p.nexts[i1][i2])->nexts[i3][*i])->id[i4];
+  /*@ assert rte: initialization: \initialized(&p.q.v); */
   v = p.q.v;
   /*@ assert rte: index_bound: 0 ≤ i4; */
   /*@ assert rte: index_bound: i4 < 12; */
@@ -456,6 +461,7 @@ int main(void)
   /*@ assert rte: mem_access: \valid_read(&pp->tq[i3][i1].v); */
   /*@ assert rte: initialization: \initialized(&pp->tq[i3][i1].v); */
   v = pp->tq[i3][i1].v;
+  /*@ assert rte: initialization: \initialized(&p.znexts); */
   /*@ assert rte: mem_access: \valid_read(p.znexts + i0); */
   /*@ assert rte: initialization: \initialized(p.znexts + i0); */
   /*@ assert rte: mem_access: \valid_read(*(p.znexts + i0) + i1); */
@@ -472,7 +478,6 @@ int main(void)
   /*@ assert rte: index_bound: i0 < 10; */
   /*@ assert rte: index_bound: 0 ≤ i1; */
   /*@ assert rte: index_bound: i1 < 11; */
-  /*@ assert rte: initialization: \initialized(&p.tq[i0][i1]); */
   q = p.tq[i0][i1];
   /*@ assert rte: index_bound: 0 ≤ i0; */
   /*@ assert rte: index_bound: i0 < 10; */
@@ -485,6 +490,7 @@ int main(void)
   /*@ assert rte: mem_access: \valid_read(&pp->val); */
   /*@ assert rte: initialization: \initialized(&pp->val); */
   v = pp->val;
+  /*@ assert rte: initialization: \initialized(&p.val); */
   v = p.val;
   /*@ assert rte: index_bound: 0 ≤ i0; */
   /*@ assert rte: index_bound: i0 < 10; */

tests/rte/oracle/initialized_union.0.res.oracle

@@ -30,37 +30,15 @@ int main(void)
   struct S s1;
   struct S s2;
   u_local1.c = (char)1;
-  /*@ assert
-      rte: initialization_of_union:
-        \initialized(&u_local1.c) ∨ \initialized(&u_local1.i) ∨
-        \initialized(&u_local1.f);
-  */
   u_local2 = u_local1;
   /*@ assert rte: initialization: \initialized(&u_local1.i); */
   u2_local1.i2 = u_local1.i;
-  /*@ assert
-      rte: initialization_of_union:
-        \initialized(&u2_local1.i1) ∨ \initialized(&u2_local1.i2);
-  */
   u2_local2 = u2_local1;
-  /*@ assert
-      rte: initialization_of_union:
-        \initialized(&u_local1.c) ∨ \initialized(&u_local1.i) ∨
-        \initialized(&u_local1.f);
-  */
   u3_local1.u = u_local1;
-  /*@ assert
-      rte: initialization_of_union:
-        \initialized(&u3_local1.u) ∨ \initialized(&u3_local1.u2);
-  */
   u3_local2 = u3_local1;
+  /*@ assert rte: initialization: \initialized(&u_global.f); */
   double f = u_global.f;
   s1.u.c = (char)'a';
-  /*@ assert
-      rte: initialization_of_union:
-        \initialized(&s1.u.c) ∨ \initialized(&s1.u.i) ∨
-        \initialized(&s1.u.f);
-  */
   s2.u = s1.u;
   __retres = 0;
   /*@ assert rte: initialization: \initialized(&__retres); */

tests/rte/oracle/initialized_union.1.res.oracle

@@ -34,37 +34,15 @@ int main(void)
   struct S s1;
   struct S s2;
   u_local1.c = (char)1;
-  /*@ assert
-      rte: initialization_of_union:
-        \initialized(&u_local1.c) ∨ \initialized(&u_local1.i) ∨
-        \initialized(&u_local1.f);
-  */
   u_local2 = u_local1;
   /*@ assert rte: initialization: \initialized(&u_local1.i); */
   u2_local1.i2 = u_local1.i;
-  /*@ assert
-      rte: initialization_of_union:
-        \initialized(&u2_local1.i1) ∨ \initialized(&u2_local1.i2);
-  */
   u2_local2 = u2_local1;
-  /*@ assert
-      rte: initialization_of_union:
-        \initialized(&u_local1.c) ∨ \initialized(&u_local1.i) ∨
-        \initialized(&u_local1.f);
-  */
   u3_local1.u = u_local1;
-  /*@ assert
-      rte: initialization_of_union:
-        \initialized(&u3_local1.u) ∨ \initialized(&u3_local1.u2);
-  */
   u3_local2 = u3_local1;
+  /*@ assert rte: initialization: \initialized(&u_global.f); */
   double f = u_global.f;
   s1.u.c = (char)'a';
-  /*@ assert
-      rte: initialization_of_union:
-        \initialized(&s1.u.c) ∨ \initialized(&s1.u.i) ∨
-        \initialized(&s1.u.f);
-  */
   s2.u = s1.u;
   union empty e1 = e;
   __retres = 0;