Skip to content

Commit

Permalink
Use ptrdiff_ikind instead of ILong for ana.arrayoob checks
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Sep 27, 2024
1 parent f7e4462 commit ea2f616
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/cdomain/value/cdomains/arrayDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -834,7 +834,7 @@ end
let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) (e, v) =
if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
let idx_before_end = Idx.to_bool (Idx.lt v l) (* check whether index is before the end of the array *)
and idx_after_start = Idx.to_bool (Idx.ge v (Idx.of_int Cil.ILong Z.zero)) in (* check whether the index is non-negative *)
and idx_after_start = Idx.to_bool (Idx.ge v (Idx.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero)) in (* check whether the index is non-negative *)
(* For an explanation of the warning types check the Pull Request #255 *)
match(idx_after_start, idx_before_end) with
| Some true, Some true -> (* Certainly in bounds on both sides.*)
Expand Down

0 comments on commit ea2f616

Please sign in to comment.