public final class MergeJoinOperator extends java.lang.Object implements MergeOperator
MergeOperator
applies the join operator to its arguments.Constructor and Description |
---|
MergeJoinOperator(AbstractDomain abstractDomain)
Create a merge operator from an abstract domain defining the join operator.
|
Modifier and Type | Method and Description |
---|---|
AbstractState |
merge(AbstractState abstractState1,
AbstractState abstractState2,
Precision precision)
The operator uses the
abstractState1 to weaken abstractState2 depending on
precision . |
public MergeJoinOperator(AbstractDomain abstractDomain)
abstractDomain
- abstract domainpublic AbstractState merge(AbstractState abstractState1, AbstractState abstractState2, Precision precision)
MergeOperator
abstractState1
to weaken abstractState2
depending on
precision
. Thus, it is asymmetric regarding its first two parameters. E.g., return
abstractState2
for no merging. To guarantee the correct behavior of the algorithm
implementations must have no side effects.merge
in interface MergeOperator