diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index e1cfb96425..4192489c3a 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -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.*)