diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index a18ad38795dd189971f39328df512a561bc61a45..a749c37f680aa214b88230203b5fb6f3fb94256b 100644
--- a/src/plugins/rte/rte.ml
+++ b/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 =
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index f2a5227810dc1b687e8d281118cea40b62b21a9b..5b502bb9f0feee8519792e63dd7f72f1ce55d3dc 100644
--- a/src/plugins/rte/visit.ml
+++ b/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 _),_) ->
diff --git a/tests/rte/initialized.c b/tests/rte/initialized.c
index 87270a09331052255bf6c90ccfa75b793cc4df95..3f208f11d00e1131daabd191b4af110a61bfeafd 100644
--- a/tests/rte/initialized.c
+++ b/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;
diff --git a/tests/rte/oracle/initialized.res.oracle b/tests/rte/oracle/initialized.res.oracle
index 2fde8033d17766630f1bea74bc9e21b254cfa0b3..826e38c81816d703d4685746dcc89fc59638112d 100644
--- a/tests/rte/oracle/initialized.res.oracle
+++ b/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; */
diff --git a/tests/rte/oracle/initialized_union.0.res.oracle b/tests/rte/oracle/initialized_union.0.res.oracle
index 550af6851cec53470d701c3d2f199ed35c5a03e1..49509af6ee58a9fe8f75d941276db39f1cc397b2 100644
--- a/tests/rte/oracle/initialized_union.0.res.oracle
+++ b/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); */
diff --git a/tests/rte/oracle/initialized_union.1.res.oracle b/tests/rte/oracle/initialized_union.1.res.oracle
index ce2e6dd9cf59727c30be247f90aff0adf9574e0d..d738022aa908c028e71c4adee346f0bedab6ec46 100644
--- a/tests/rte/oracle/initialized_union.1.res.oracle
+++ b/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;