public class JvmReferenceTransferRelation extends JvmTransferRelation<SetAbstractState<Reference>>
JvmTransferRelation
propagates reference values, destroys references upon arithmetic
operations, and creates fresh references for return values of intraprocedurally analyzed calls.JvmTransferRelation.InstructionAbstractInterpreter
Constructor and Description |
---|
JvmReferenceTransferRelation() |
Modifier and Type | Method and Description |
---|---|
protected SetAbstractState<Reference> |
calculateArithmeticInstruction(Instruction instruction,
java.util.List<SetAbstractState<Reference>> operands)
Calculates the result of the instruction application.
|
protected SetAbstractState<Reference> |
computeIncrement(SetAbstractState<Reference> state,
int value)
Returns the abstract state of the incremented input
state by value . |
JvmReferenceAbstractState |
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 . |
SetAbstractState<Reference> |
getAbstractDefault()
Returns a default abstract state.
|
void |
invokeMethod(JvmAbstractState<SetAbstractState<Reference>> state,
Call call,
java.util.List<SetAbstractState<Reference>> operands)
The default implementation computes join over its arguments.
|
getAbstractByteConstant, getAbstractDoubleConstant, getAbstractFloatConstant, getAbstractIntegerConstant, getAbstractLongConstant, getAbstractNull, getAbstractReferenceValue, getAbstractReferenceValue, getAbstractReferenceValue, getAbstractShortConstant, getAbstractSuccessorForInstruction, handleCheckCast, isInstanceOf, processCall
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getEdges
generateAbstractSuccessors, wrapAbstractSuccessorInCollection
public JvmReferenceAbstractState generateEdgeAbstractSuccessor(AbstractState abstractState, JvmCfaEdge edge, Precision precision)
generateEdgeAbstractSuccessor
in class JvmTransferRelation<SetAbstractState<Reference>>
public SetAbstractState<Reference> getAbstractDefault()
JvmTransferRelation
getAbstractDefault
in class JvmTransferRelation<SetAbstractState<Reference>>
protected SetAbstractState<Reference> calculateArithmeticInstruction(Instruction instruction, java.util.List<SetAbstractState<Reference>> operands)
JvmTransferRelation
calculateArithmeticInstruction
in class JvmTransferRelation<SetAbstractState<Reference>>
protected SetAbstractState<Reference> computeIncrement(SetAbstractState<Reference> state, int value)
JvmTransferRelation
state
by value
. The default
implementation computes the join.computeIncrement
in class JvmTransferRelation<SetAbstractState<Reference>>
public void invokeMethod(JvmAbstractState<SetAbstractState<Reference>> state, Call call, java.util.List<SetAbstractState<Reference>> operands)
JvmTransferRelation
invokeMethod
in class JvmTransferRelation<SetAbstractState<Reference>>
public java.util.Collection<? extends AbstractState> generateEdgeAbstractSuccessors(AbstractState abstractState, JvmCfaEdge edge, Precision precision)
ProgramLocationDependentTransferRelation
edge
.