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

This StopOperator returns true if there is a state in the reached set covering the input AbstractState.

Constructor Summary

Constructors

Constructor and Description
StopSepOperator(AbstractDomain abstractDomain) Create a join operator from the abstract domain defining the join operator.

Method Summary

Modifier and Type	Method and Description
boolean	stop(AbstractState abstractState, java.util.Collection<? extends AbstractState> reachedAbstractStates, Precision precision) The operator may decide based on the (generalized under the given precision) convergence.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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 given precision) convergence. In this case it needs to look up the abstractState in the reachedAbstractStates. Otherwise, it can return true if sufficient information is collected, e.g., a safety property is violated.

Specified by:

stop in interface StopOperator