diff --git a/infer/src/checkers/PurityAnalysis.ml b/infer/src/checkers/PurityAnalysis.ml index fc3aea206..1f591503c 100644 --- a/infer/src/checkers/PurityAnalysis.ml +++ b/infer/src/checkers/PurityAnalysis.ml @@ -6,6 +6,7 @@ *) open! IStd +open AbstractDomain.Types module F = Format module L = Logging module ModifiedVarSet = PrettyPrintable.MakePPSet (Var) @@ -130,9 +131,9 @@ module TransferFunctions = struct (* if the callee is impure, find the parameters that have been modified by the callee *) let find_modified_if_impure inferbo_mem formals args callee_summary = match callee_summary with - | AbstractDomain.Types.Top -> + | Top -> Domain.impure_global - | AbstractDomain.Types.NonTop callee_modified_params -> + | NonTop callee_modified_params -> Domain.( debug "Callee modified params %a \n" ModifiedParamIndices.pp callee_modified_params ; if ModifiedParamIndices.is_empty callee_modified_params then pure @@ -169,7 +170,7 @@ module TransferFunctions = struct | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java *) debug "Unexpected indirect call %a" HilInstr.pp instr ; - AbstractDomain.Types.Top + Top | _ -> astate diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index 9fdff37c2..90305b377 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/infer/src/checkers/loopInvariant.ml @@ -5,6 +5,7 @@ * LICENSE file in the root directory of this source tree. *) open! IStd +open AbstractDomain.Types module L = Logging module InvariantVars = AbstractDomain.FiniteSet (Var) module VarsInLoop = AbstractDomain.FiniteSet (Var) @@ -199,7 +200,7 @@ let get_invalidated_vars_in_loop tenv loop_head ~is_pure_by_default ~get_callee_ let purity = get_purity tenv ~is_pure_by_default ~get_callee_purity callee_pname in PurityDomain.( match purity with - | AbstractDomain.Types.Top -> + | Top -> (* modified global *) (* if one of the callees modifies a global static variable, invalidate all unmodeled function calls + args *) @@ -209,7 +210,7 @@ let get_invalidated_vars_in_loop tenv loop_head ~is_pure_by_default ~get_callee_ (InvalidatedVars.add (Var.of_id id) acc) in InvalidatedVars.union invalidated_args (force all_unmodeled_modified) - | AbstractDomain.Types.NonTop modified_params -> + | NonTop modified_params -> if ModifiedParamIndices.is_empty modified_params then (*pure*) acc else diff --git a/infer/src/checkers/purityDomain.ml b/infer/src/checkers/purityDomain.ml index 53e551902..d7467629e 100644 --- a/infer/src/checkers/purityDomain.ml +++ b/infer/src/checkers/purityDomain.ml @@ -5,24 +5,25 @@ * LICENSE file in the root directory of this source tree. *) open! IStd +open AbstractDomain.Types module F = Format module ModifiedParamIndices = AbstractDomain.FiniteSet (Int) module Domain = AbstractDomain.TopLifted (ModifiedParamIndices) include Domain -let pure = AbstractDomain.Types.NonTop ModifiedParamIndices.empty +let pure = NonTop ModifiedParamIndices.empty -let impure_global = AbstractDomain.Types.Top +let impure_global = Top let is_pure astate = match astate with - | AbstractDomain.Types.Top -> + | Top -> false - | AbstractDomain.Types.NonTop modified_params -> + | NonTop modified_params -> ModifiedParamIndices.is_empty modified_params -let impure_params modified_params = AbstractDomain.Types.NonTop modified_params +let impure_params modified_params = NonTop modified_params let all_params_modified args = List.foldi ~init:ModifiedParamIndices.empty