public interface ProgramLocationDependentTransferRelation<ContentT extends AbstractState<ContentT>> extends TransferRelation<JvmAbstractState<ContentT>>
TransferRelations that depend on the Cfa location for which the successor can be defined for the edges
of the current location.| Modifier and Type | Method and Description |
|---|---|
default java.util.Collection<JvmAbstractState<ContentT>> |
generateAbstractSuccessors(JvmAbstractState<ContentT> abstractState,
Precision precision)
Returns abstract successor states of the
abstractState under the selected precision. |
java.util.Collection<JvmAbstractState<ContentT>> |
generateEdgeAbstractSuccessors(JvmAbstractState<ContentT> abstractState,
JvmCfaEdge edge,
Precision precision)
Computes the successor states for the CFA
edge. |
java.util.List<JvmCfaEdge> |
getEdges(JvmAbstractState<ContentT> state) |
default java.util.Collection<JvmAbstractState<ContentT>> |
wrapAbstractSuccessorInCollection(JvmAbstractState<ContentT> abstractState) |
java.util.Collection<JvmAbstractState<ContentT>> generateEdgeAbstractSuccessors(JvmAbstractState<ContentT> abstractState, JvmCfaEdge edge, Precision precision)
edge.default java.util.Collection<JvmAbstractState<ContentT>> wrapAbstractSuccessorInCollection(JvmAbstractState<ContentT> abstractState)
default java.util.Collection<JvmAbstractState<ContentT>> generateAbstractSuccessors(JvmAbstractState<ContentT> abstractState, Precision precision)
TransferRelationabstractState under the selected precision.generateAbstractSuccessors in interface TransferRelation<JvmAbstractState<ContentT extends AbstractState<ContentT>>>java.util.List<JvmCfaEdge> getEdges(JvmAbstractState<ContentT> state)