public class ProgramVariableReferencesAnalyst extends java.lang.Object implements IProofReferencesAnalyst
IProgramVariable
) via assignments.Constructor and Description |
---|
ProgramVariableReferencesAnalyst() |
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 void |
listReferences(Node node,
ProgramElement pe,
ProgramVariable arrayLength,
java.util.LinkedHashSet<IProofReference<?>> toFill,
boolean includeExpressionContainer)
Extracts the proof references recursive.
|
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 void listReferences(Node node, ProgramElement pe, ProgramVariable arrayLength, java.util.LinkedHashSet<IProofReference<?>> toFill, boolean includeExpressionContainer)
node
- The node.pe
- The current ProgramElement
.arrayLength
- The ProgramVariable
used for array length which is ignored.toFill
- The LinkedHashSet
to fill.includeExpressionContainer
- Include ExpressionContainer
?