Skip to content

Commit 3014833

Browse files
committed
Fix offset used for lval type calculation in base set_mval
to_cil_offset is specific for partitioned arrays and drops indices. Thus, it can compute an incorrect type which doesn't match the actual offset.
1 parent cc6efe6 commit 3014833

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

src/analyses/base.ml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1675,7 +1675,7 @@ struct
16751675
* not include the flag. *)
16761676
let set_mval ~(man: _ man) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (st: store) ((x, offs): Addr.Mval.t) (lval_type: Cil.typ) (value: value): store =
16771677
let ask = Analyses.ask_of_man man in
1678-
let cil_offset = Offs.to_cil_offset offs in
1678+
let cil_offset = Offs.to_cil_offset offs in (* Only for partitioned arrays! Drops indices. *)
16791679
let t = match t_override with
16801680
| Some t -> t
16811681
| None ->
@@ -1685,11 +1685,11 @@ struct
16851685
lval_type
16861686
else
16871687
try
1688-
Cilfacade.typeOfLval (Var x, cil_offset)
1689-
with Cilfacade.TypeOfError _ ->
1688+
Offs.type_of ~base:x.vtype offs
1689+
with Offset.Type_of_error _ ->
16901690
(* If we cannot determine the correct type here, we go with the one of the LVal *)
16911691
(* This will usually lead to a type mismatch in the ValueDomain (and hence supertop) *)
1692-
M.debug ~category:Analyzer "Cilfacade.typeOfLval failed Could not obtain the type of %a" d_lval (Var x, cil_offset);
1692+
M.debug ~category:Analyzer "Could not obtain the type of %a" Addr.Mval.pretty (x, offs);
16931693
lval_type
16941694
in
16951695
let update_offset old_value =
@@ -1708,7 +1708,7 @@ struct
17081708
else
17091709
new_value
17101710
in
1711-
if M.tracing then M.tracel "set" "update_one_addr: start with '%a' (type '%a') \nstate:%a" AD.pretty (AD.of_mval (x,offs)) d_type x.vtype D.pretty st;
1711+
if M.tracing then M.tracel "set" "update_one_addr: start with '%a' (type '%a') \nstate:%a" Addr.Mval.pretty (x,offs) d_type t D.pretty st;
17121712
if isFunctionType x.vtype then begin
17131713
if M.tracing then M.tracel "set" "update_one_addr: returning: '%a' is a function type " d_type x.vtype;
17141714
st

0 commit comments

Comments
 (0)