diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index b96f67f99..59e2182b9 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -167,23 +167,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Conjunction actual_indexes | HilExp.AccessExpression access_expr -> ( let actual_access_path = HilExp.AccessExpression.to_access_path access_expr in - if OwnershipDomain.is_owned actual_access_path caller_astate.ownership then - (* the actual passed to the current callee is owned. drop all the conditional accesses - for that actual, since they're all safe *) - Conjunction actual_indexes - else - let base = fst actual_access_path in - match OwnershipDomain.get_owned (base, []) caller_astate.ownership with - | Owned -> - (* the actual passed to the current callee is owned. drop all the conditional + match OwnershipDomain.get_owned actual_access_path caller_astate.ownership with + | Owned -> + (* the actual passed to the current callee is owned. drop all the conditional accesses for that actual, since they're all safe *) - Conjunction actual_indexes - | OwnedIf formal_indexes -> - (* access path conditionally owned if [formal_indexes] are owned *) - Conjunction (IntSet.union formal_indexes actual_indexes) - | Unowned -> - (* access path not rooted in a formal and not conditionally owned *) - False ) + Conjunction actual_indexes + | OwnedIf formal_indexes -> + (* access path conditionally owned if [formal_indexes] are owned *) + Conjunction (IntSet.union formal_indexes actual_indexes) + | Unowned -> + (* access path not rooted in a formal and not conditionally owned *) + False ) | _ -> (* couldn't find access path, don't know if it's owned. assume not *) False diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index f060152d4..c5eb16208 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -395,14 +395,6 @@ module OwnershipDomain = struct keep_looking access_path astate - let is_owned access_path astate = - match get_owned access_path astate with - | OwnershipAbstractValue.Owned -> - true - | OwnershipAbstractValue.OwnedIf _ | Unowned -> - false - - let rec ownership_of_expr expr ownership = let open HilExp in match expr with diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 64d140122..1a4fd672a 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -151,8 +151,6 @@ module OwnershipDomain : sig val get_owned : AccessPath.t -> t -> OwnershipAbstractValue.t - val is_owned : AccessPath.t -> t -> bool - val propagate_assignment : AccessPath.t -> HilExp.t -> t -> t val propagate_return : AccessPath.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t