diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 43a277767..07eece71b 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -301,9 +301,9 @@ module Val = struct let minus_a = lift_itv Itv.minus - let get_iterator_itv : t -> t = + let get_range_of_iterator : t -> t = fun i -> - let itv = Itv.get_iterator_itv i.itv in + let itv = Itv.get_range_of_iterator i.itv in of_itv itv ~traces:i.traces @@ -1053,7 +1053,7 @@ module AliasTargets = struct let exists2 f x y = exists (fun k v -> exists (f k v) y) x - let find_first_simple_zero_alias x = + let find_simple_alias x = let exception Found of KeyRhs.t in let is_simple_zero rhs = function | AliasTarget.Simple {i} when IntLit.iszero i -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index b9f5af642..1800de989 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -100,7 +100,7 @@ module Val : sig val get_array_blk : t -> ArrayBlk.t - val get_iterator_itv : t -> t + val get_range_of_iterator : t -> t (** Get a range of an iterator value, for example, if iterator value is [\[lb,ub\]], it returns [\[0,ub\]]. *) @@ -332,7 +332,7 @@ module AliasTargets : sig val exists2 : (key -> value -> key -> value -> bool) -> t -> t -> bool - val find_first_simple_zero_alias : t -> key option + val find_simple_alias : t -> key option (** Find a simple alias from the set of aliases *) val subst : subst_loc:(key -> key option) -> t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 90b8322d6..ed3ccfd29 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -305,7 +305,7 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t = fun integer_type_widths exp mem -> match exp with | Exp.Var id -> - let alias_loc = AliasTargets.find_first_simple_zero_alias (Mem.find_alias_id id mem) in + let alias_loc = AliasTargets.find_simple_alias (Mem.find_alias_id id mem) in Option.value_map alias_loc ~default:Val.bot ~f:(fun loc -> Mem.find loc mem) | Exp.Lvar pvar -> Mem.find (Loc.of_pvar pvar) mem @@ -484,7 +484,7 @@ let mk_eval_sym_cost = mk_eval_sym_mode ~mode:EvalCost let conservative_array_length ?traces arr_locs mem = let accum_add arr_loc acc = Mem.find arr_loc mem |> Val.array_sizeof |> Itv.plus acc in PowLoc.fold accum_add arr_locs Itv.zero - |> Val.of_itv ?traces |> Val.get_iterator_itv |> Val.set_itv_updated_by_addition + |> Val.of_itv ?traces |> Val.get_range_of_iterator |> Val.set_itv_updated_by_addition let eval_array_locs_length arr_locs mem = diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 1392bfa45..1cc3f5590 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -149,7 +149,7 @@ module ItvPure = struct let zero_one = (Bound.zero, Bound.one) - let get_iterator_itv = set_lb_zero + let get_range_of_iterator = set_lb_zero let true_sem = one @@ -723,7 +723,7 @@ let set_lb lb = lift1 (ItvPure.set_lb lb) let set_lb_zero = lift1 ItvPure.set_lb_zero -let get_iterator_itv : t -> t = lift1 ItvPure.get_iterator_itv +let get_range_of_iterator : t -> t = lift1 ItvPure.get_range_of_iterator let get_const : t -> Z.t option = bind1zo ItvPure.get_const diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index bfa013d33..55939f109 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -149,7 +149,7 @@ val zero_one : t val unknown_bool : t (** [0, 1] *) -val get_iterator_itv : t -> t +val get_range_of_iterator : t -> t val of_bool : Boolean.t -> t