de.uka.ilkd.key.proof_references.analyst

Class MethodCallProofReferencesAnalyst

java.lang.Object

de.uka.ilkd.key.proof_references.analyst.MethodCallProofReferencesAnalyst

All Implemented Interfaces:

IProofReferencesAnalyst

public class MethodCallProofReferencesAnalyst
extends java.lang.Object
implements IProofReferencesAnalyst

Extracts called methods.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
MethodCallProofReferencesAnalyst()

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

Methods inherited from class java.lang.Object

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

Constructor Detail

MethodCallProofReferencesAnalyst

public MethodCallProofReferencesAnalyst()

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.

extractContext

protected ExecutionContext extractContext(Node node,
                                          Services services)

Extracts the ExecutionContext.

Parameters:

node - The Node to extract ExecutionContext from.

services - The Services to use.

Returns:

The found ExecutionContext or null if not available.

createReference

protected IProofReference<IProgramMethod> createReference(Node node,
                                                          Services services,
                                                          ExecutionContext context,
                                                          MethodReference mr)

Creates an IProofReference to the called IProgramMethod.

Parameters:

node - The Node which caused the reference.

services - The Services to use.

context - The ExecutionContext to use.

mr - The MethodReference.

Returns:

The created IProofReference.