Skip to content

Commit

Permalink
Fix size check in memory_copying
Browse files Browse the repository at this point in the history
Co-authored-by: Michael Schwarz <[email protected]>
  • Loading branch information
mrstanb and michael-schwarz authored Oct 6, 2023
1 parent 22e4df5 commit b9c2134
Showing 1 changed file with 3 additions and 8 deletions.
11 changes: 3 additions & 8 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2139,21 +2139,16 @@ struct
in
let dest_size_equal_n =
match dest_size, n_intdom with
| `Top, `Top -> true
| `Bot, `Bot -> true
| `Lifted ds, `Lifted n ->
let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
let casted_n = ID.cast_to (Cilfacade.ptrdiff_ikind ()) n in
let ds_eq_n =
begin try ID.eq casted_ds casted_n
with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
end
in
begin match ID.to_bool ds_eq_n with
| Some b -> b
| None -> false
end
| _, _ -> false
Option.value ~default:false ID.to_bool ds_eq_n
| _ -> false
in
let dest_a, dest_typ = addr_type_of_exp dst in
let src_lval = mkMem ~addr:(Cil.stripCasts src) ~off:NoOffset in
Expand Down

0 comments on commit b9c2134

Please sign in to comment.