Package proguard.analysis.cpa.defaults
Class StopSepOperator
- java.lang.Object
-
- proguard.analysis.cpa.defaults.StopSepOperator
-
- All Implemented Interfaces:
StopOperator
public final class StopSepOperator extends java.lang.Object implements StopOperator
ThisStopOperator
returns true if there is a state in the reached set covering the inputAbstractState
.
-
-
Constructor Summary
Constructors Constructor Description StopSepOperator(AbstractDomain abstractDomain)
Create a join operator from the abstract domain defining the join operator.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description boolean
stop(AbstractState abstractState, java.util.Collection<? extends AbstractState> reachedAbstractStates, Precision precision)
The operator may decide based on the (generalized under the givenprecision
) convergence.
-
-
-
Constructor Detail
-
StopSepOperator
public StopSepOperator(AbstractDomain abstractDomain)
Create a join operator from the abstract domain defining the join operator.- Parameters:
abstractDomain
- abstract domain
-
-
Method Detail
-
stop
public boolean stop(AbstractState abstractState, java.util.Collection<? extends AbstractState> reachedAbstractStates, Precision precision)
Description copied from interface:StopOperator
The operator may decide based on the (generalized under the givenprecision
) convergence. In this case it needs to look up theabstractState
in thereachedAbstractStates
. Otherwise, it can returntrue
if sufficient information is collected, e.g., a safety property is violated.- Specified by:
stop
in interfaceStopOperator
-
-