diff --git a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml index e38ebce79..92e4cd12f 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml @@ -853,27 +853,29 @@ module Make (Manager : Manager_S) = struct let itv_of sym itv = - if Itv.is_empty itv then empty - else - let lb, ub = (Itv.lb itv, Itv.ub itv) in - Option.value_map (SymExp.of_sym sym) ~default:empty ~f:(fun sym_exp -> - let tcons_lb = - Option.map (Itv.Bound.is_const lb) ~f:(fun lb -> - let sym_minus_lb = SymExp.minus sym_exp (SymExp.of_big_int lb) in - Tcons1.make sym_minus_lb Tcons1.SUPEQ ) - in - let tcons_ub = - Option.map (Itv.Bound.is_const ub) ~f:(fun ub -> - let ub_minus_sym = SymExp.minus (SymExp.of_big_int ub) sym_exp in - Tcons1.make ub_minus_sym Tcons1.SUPEQ ) - in - match (tcons_lb, tcons_ub) with - | Some tcons_lb, Some tcons_ub -> - doubleton tcons_lb tcons_ub - | Some tcons, None | None, Some tcons -> - singleton tcons - | None, None -> - empty ) + match itv with + | Bottom -> + empty + | NonBottom itv_pure -> + let lb, ub = (Itv.ItvPure.lb itv_pure, Itv.ItvPure.ub itv_pure) in + Option.value_map (SymExp.of_sym sym) ~default:empty ~f:(fun sym_exp -> + let tcons_lb = + Option.map (Itv.Bound.is_const lb) ~f:(fun lb -> + let sym_minus_lb = SymExp.minus sym_exp (SymExp.of_big_int lb) in + Tcons1.make sym_minus_lb Tcons1.SUPEQ ) + in + let tcons_ub = + Option.map (Itv.Bound.is_const ub) ~f:(fun ub -> + let ub_minus_sym = SymExp.minus (SymExp.of_big_int ub) sym_exp in + Tcons1.make ub_minus_sym Tcons1.SUPEQ ) + in + match (tcons_lb, tcons_ub) with + | Some tcons_lb, Some tcons_ub -> + doubleton tcons_lb tcons_ub + | Some tcons, None | None, Some tcons -> + singleton tcons + | None, None -> + empty ) let of_raw_symexp re typ = singleton (Tcons1.make (SymExp.of_raw re) typ) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index afbcb11b2..e2647d19f 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -10,7 +10,6 @@ open! IStd open! AbstractDomain.Types module F = Format -module L = Logging module Bound = Bounds.Bound open Ints module SymbolPath = Symb.SymbolPath @@ -443,20 +442,6 @@ let bot : t = Bottom let top : t = NonBottom ItvPure.top -let lb : t -> Bound.t = function - | NonBottom x -> - ItvPure.lb x - | Bottom -> - L.(die InternalError) "lower bound of bottom" - - -let ub : t -> Bound.t = function - | NonBottom x -> - ItvPure.ub x - | Bottom -> - L.(die InternalError) "upper bound of bottom" - - let get_bound itv (be : Symb.BoundEnd.t) = match (itv, be) with | Bottom, _ -> diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 64a17daa2..33bbc7064 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -139,10 +139,6 @@ val is_one : t -> bool val is_mone : t -> bool -val lb : t -> Bound.t - -val ub : t -> Bound.t - val get_bound : t -> Symb.BoundEnd.t -> Bound.t bottom_lifted val is_false : t -> bool