public class DelegateAbstractDomain<LatticeAbstractStateT extends LatticeAbstractState> extends java.lang.Object implements AbstractDomain
AbstractDomain
operators to the LatticeAbstractState
. Thus, we can keep the CPA algorithm generic without having to cast types
in the domain specific code. Abstract domains defined with LatticeAbstractState
should be
passed as DelegateAbstractDomain
s to the CPA algorithm.Constructor and Description |
---|
DelegateAbstractDomain() |
Modifier and Type | Method and Description |
---|---|
boolean |
isLessOrEqual(AbstractState abstractState1,
AbstractState abstractState2)
Compares two abstract states.
|
AbstractState |
join(AbstractState abstractState1,
AbstractState abstractState2)
Computes the join over two abstract states.
|
public AbstractState join(AbstractState abstractState1, AbstractState abstractState2)
AbstractDomain
join
in interface AbstractDomain
public boolean isLessOrEqual(AbstractState abstractState1, AbstractState abstractState2)
AbstractDomain
isLessOrEqual
in interface AbstractDomain