diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 38bdcb42b..1b23f524b 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -132,12 +132,9 @@ struct fun lhs rhs -> if phys_equal lhs rhs then lhs else - match DConfig.join_policy with - | `NeverJoin -> - List.rev_append rhs lhs - | `UnderApproximateAfter n -> - let lhs_length = List.length lhs in - if lhs_length >= n then lhs else list_rev_append rhs lhs (n - lhs_length) + let (`UnderApproximateAfter n) = DConfig.join_policy in + let lhs_length = List.length lhs in + if lhs_length >= n then lhs else list_rev_append rhs lhs (n - lhs_length) (** check if elements of [disj] appear in [of_] in the same order, using pointer equality on diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 6f79c860d..954197c7c 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -34,7 +34,7 @@ module type MakeHIL = functor (C : ProcCfg.S) -> sig end module type DisjunctiveConfig = sig - val join_policy : [`UnderApproximateAfter of int | `NeverJoin] + val join_policy : [`UnderApproximateAfter of int] val widen_policy : [`UnderApproximateAfterNumIterations of int] end diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 6c99c7805..e6482f508 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -46,8 +46,7 @@ module type DisjunctiveConfig = sig [ `UnderApproximateAfter of int (** When the set of disjuncts gets bigger than [n] then just stop adding new states to it, drop any further states on the floor. This corresponds to an under-approximation/bounded - approach. *) - | `NeverJoin (** keep accumulating states *) ] + approach. *) ] val widen_policy : [`UnderApproximateAfterNumIterations of int] end diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 8bb805539..69e543112 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -294,9 +294,7 @@ module DisjunctiveAnalyzer = AbstractInterpreter.MakeDisjunctive (PulseTransferFunctions) (struct - let join_policy = - match Config.pulse_max_disjuncts with 0 -> `NeverJoin | n -> `UnderApproximateAfter n - + let join_policy = `UnderApproximateAfter Config.pulse_max_disjuncts let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold end)