de.uka.ilkd.key.proof_references.analyst

Class ProgramVariableReferencesAnalyst

java.lang.Object

de.uka.ilkd.key.proof_references.analyst.ProgramVariableReferencesAnalyst

All Implemented Interfaces:

IProofReferencesAnalyst

public class ProgramVariableReferencesAnalyst
extends java.lang.Object
implements IProofReferencesAnalyst

Extracts read and write access to fields (IProgramVariable) via assignments.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
ProgramVariableReferencesAnalyst()

Method Summary

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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ProgramVariableReferencesAnalyst

public ProgramVariableReferencesAnalyst()

Method Detail

computeReferences

public 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.

Specified by:

computeReferences in interface IProofReferencesAnalyst

Parameters:

node - The Node to compute its IProofReferences.

services - The Services to use.

Returns:

The found IProofReference or null/empty set if the applied rule is not supported.

listReferences

protected void listReferences(Node node,
                              ProgramElement pe,
                              ProgramVariable arrayLength,
                              java.util.LinkedHashSet<IProofReference<?>> toFill,
                              boolean includeExpressionContainer)

Extracts the proof references recursive.

Parameters:

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?