public class CompositeHeapTransferRelation extends java.lang.Object implements WrapperTransferRelation, ProgramLocationDependentForwardTransferRelation<JvmCfaNode,JvmCfaEdge,MethodSignature>
JvmTransferRelation
s applying them elementwise to CompositeHeapJvmAbstractState
s. The CompositeHeapJvmAbstractState.REFERENCE_STATE_INDEX
th transfer relation must be JvmReferenceTransferRelation
to match the structure of CompositeHeapTransferRelation
.Constructor and Description |
---|
CompositeHeapTransferRelation(java.util.List<JvmTransferRelation<? extends AbstractState>> jvmTransferRelations)
Create a composite transfer relation from a list of transfer relations.
|
Modifier and Type | Method and Description |
---|---|
CompositeHeapJvmAbstractState |
generateEdgeAbstractSuccessor(AbstractState abstractState,
JvmCfaEdge edge,
Precision precision) |
java.util.Collection<? extends AbstractState> |
generateEdgeAbstractSuccessors(AbstractState abstractState,
JvmCfaEdge edge,
Precision precision)
Computes the successor states for the CFA
edge . |
java.lang.Iterable<? extends TransferRelation> |
getWrappedTransferRelations()
Returns wrapped transfer relations.
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getEdges
generateAbstractSuccessors, wrapAbstractSuccessorInCollection
public CompositeHeapTransferRelation(java.util.List<JvmTransferRelation<? extends AbstractState>> jvmTransferRelations)
jvmTransferRelations
- a list of JvmTransferRelation
s, the CompositeHeapJvmAbstractState.REFERENCE_INDEX
th transfer relation must be JvmReferenceTransferRelation
public java.lang.Iterable<? extends TransferRelation> getWrappedTransferRelations()
WrapperTransferRelation
getWrappedTransferRelations
in interface WrapperTransferRelation
public CompositeHeapJvmAbstractState generateEdgeAbstractSuccessor(AbstractState abstractState, JvmCfaEdge edge, Precision precision)
public java.util.Collection<? extends AbstractState> generateEdgeAbstractSuccessors(AbstractState abstractState, JvmCfaEdge edge, Precision precision)
ProgramLocationDependentTransferRelation
edge
.generateEdgeAbstractSuccessors
in interface ProgramLocationDependentTransferRelation<JvmCfaNode,JvmCfaEdge,MethodSignature>