public class MethodCallProofReferencesAnalyst extends java.lang.Object implements IProofReferencesAnalyst
Constructor and Description |
---|
MethodCallProofReferencesAnalyst() |
Modifier and Type | Method and Description |
---|---|
java.util.LinkedHashSet<IProofReference<?>> |
computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
protected IProofReference<IProgramMethod> |
createReference(Node node,
Services services,
ExecutionContext context,
MethodReference mr)
Creates an
IProofReference to the called IProgramMethod . |
protected ExecutionContext |
extractContext(Node node,
Services services)
Extracts the
ExecutionContext . |
public java.util.LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services)
IProofReference
for the given Node
which
can be null
or an empty set if the applied rule is not supported by this IProofReferencesAnalyst
.computeReferences
in interface IProofReferencesAnalyst
node
- The Node
to compute its IProofReference
s.services
- The Services
to use.IProofReference
or null
/empty set if the applied rule is not supported.protected ExecutionContext extractContext(Node node, Services services)
ExecutionContext
.node
- The Node
to extract ExecutionContext
from.services
- The Services
to use.ExecutionContext
or null
if not available.protected IProofReference<IProgramMethod> createReference(Node node, Services services, ExecutionContext context, MethodReference mr)
IProofReference
to the called IProgramMethod
.node
- The Node
which caused the reference.services
- The Services
to use.context
- The ExecutionContext
to use.mr
- The MethodReference
.IProofReference
.