de.uka.ilkd.key.java.statement

Class MethodBodyStatement

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.JavaNonTerminalProgramElement

de.uka.ilkd.key.java.statement.MethodBodyStatement

All Implemented Interfaces:

ModelElement, NonTerminalProgramElement, ProgramElement, SourceElement, Statement, SVSubstitute

public class MethodBodyStatement
extends JavaNonTerminalProgramElement
implements Statement, NonTerminalProgramElement

A shortcut-statement for a method body, i.e. no dynamic dispatching any longer.

Please take care: only the method name plus the class in which class the method is implemented is part of the syntax representation of such a statement, but not the methods complete syntax. If there are two methods with an equal name, but different signature (i.e. parameter types), the pure syntax is ambigious. In fact the concrete body this method body statement represents depends on the static type of its arguments.

Therefore: Transformation of a method body statement MUST keep the static type of the arguments unchanged.

Field Summary

Fields

Modifier and Type	Field and Description
private TypeReference	bodySource This type reference determines the class where the represented method has to be implemented.
private IProgramMethod	method cache resolved method
private MethodReference	methodReference the reference describing the method signature
private IProgramVariable	resultVar the variable the result of the method execution is assigned to if the method is declared void or the result not assigned to a variable or field, this value is null.
private boolean	useSpecification indicates whether this stands for the specification of a method rather than the concrete body

Constructor Summary

Constructors

Constructor and Description
MethodBodyStatement(ExtList list)
MethodBodyStatement(IProgramMethod method, ReferencePrefix newContext, IProgramVariable res, ImmutableArray<Expression> args)
MethodBodyStatement(IProgramMethod method, ReferencePrefix newContext, IProgramVariable res, ImmutableArray<Expression> args, boolean useSpecification)
MethodBodyStatement(IProgramMethod method, ReferencePrefix newContext, IProgramVariable res, ImmutableArray<Expression> args, boolean useSpecification, ProgramElement scope)
MethodBodyStatement(IProgramMethod method, ReferencePrefix newContext, IProgramVariable res, ImmutableArray<Expression> args, ProgramElement scope)
MethodBodyStatement(TypeReference bodySource, IProgramVariable resultVar, MethodReference methodReference) Construct a method body shortcut

Method Summary

Modifier and Type	Method and Description
private void	checkOnlyProgramVarsAsArguments(ImmutableArray<? extends Expression> arguments)
ImmutableArray<? extends Expression>	getArguments()
Statement	getBody(Services services) Get method body.
KeYJavaType	getBodySource()
TypeReference	getBodySourceAsTypeReference()
ProgramElement	getChildAt(int index) Returns the child at the specified index in this node's "virtual" child array.
int	getChildCount() Returns the number of children of this node.
ReferencePrefix	getDesignatedContext()
MethodReference	getMethodReference()
IProgramMethod	getProgramMethod(Services services)
IProgramVariable	getResultVariable()
boolean	isStatic(Services services)
void	prettyPrint(PrettyPrinter p) Pretty printing the source element.
boolean	replaceBySpecification()
private void	resolveMethod(Services services)
java.lang.String	reuseSignature(Services services, ExecutionContext ec) this is the default implementation of the signature, which is used to determine program similarity.
void	visit(Visitor v) calls the corresponding method of a visitor in order to perform some action/transformation on this element

Methods inherited from class de.uka.ilkd.key.java.JavaNonTerminalProgramElement

compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren

Methods inherited from class de.uka.ilkd.key.java.JavaProgramElement

getComments, hashCode, prettyPrintMain

Methods inherited from class de.uka.ilkd.key.java.JavaSourceElement

getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.java.ProgramElement

getComments, match

Methods inherited from interface de.uka.ilkd.key.java.SourceElement

equalsModRenaming, getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getPositionInfo, getRelativePosition, getStartPosition

Field Detail

resultVar

private final IProgramVariable resultVar

the variable the result of the method execution is assigned to if the method is declared void or the result not assigned to a variable or field, this value is null.

bodySource

private final TypeReference bodySource

This type reference determines the class where the represented method has to be implemented.

methodReference

private final MethodReference methodReference

the reference describing the method signature

method

private IProgramMethod method

cache resolved method

useSpecification

private boolean useSpecification

indicates whether this stands for the specification of a method rather than the concrete body

Constructor Detail

MethodBodyStatement

public MethodBodyStatement(TypeReference bodySource,
                           IProgramVariable resultVar,
                           MethodReference methodReference)

Construct a method body shortcut

Parameters:

bodySource - exact class where the body is declared

resultVar - the IProgramVariable to which the method's return value is assigned

methodReference - the MethodReference encapsulating the method's signature

MethodBodyStatement

public MethodBodyStatement(ExtList list)

MethodBodyStatement

public MethodBodyStatement(IProgramMethod method,
                           ReferencePrefix newContext,
                           IProgramVariable res,
                           ImmutableArray<Expression> args,
                           boolean useSpecification)

MethodBodyStatement

public MethodBodyStatement(IProgramMethod method,
                           ReferencePrefix newContext,
                           IProgramVariable res,
                           ImmutableArray<Expression> args,
                           boolean useSpecification,
                           ProgramElement scope)

MethodBodyStatement

public MethodBodyStatement(IProgramMethod method,
                           ReferencePrefix newContext,
                           IProgramVariable res,
                           ImmutableArray<Expression> args)

MethodBodyStatement

public MethodBodyStatement(IProgramMethod method,
                           ReferencePrefix newContext,
                           IProgramVariable res,
                           ImmutableArray<Expression> args,
                           ProgramElement scope)

Method Detail

checkOnlyProgramVarsAsArguments

private void checkOnlyProgramVarsAsArguments(ImmutableArray<? extends Expression> arguments)

getBody

public Statement getBody(Services services)

Get method body.

Returns:

the Statement

getChildCount

public int getChildCount()

Returns the number of children of this node.

Specified by:

getChildCount in interface NonTerminalProgramElement

Returns:

an int giving the number of children of this node

getDesignatedContext

public ReferencePrefix getDesignatedContext()

getArguments

public ImmutableArray<? extends Expression> getArguments()

getChildAt

public ProgramElement getChildAt(int index)

Returns the child at the specified index in this node's "virtual" child array.

Specified by:

getChildAt in interface NonTerminalProgramElement

Parameters:

index - an index into this node's "virtual" child array

Returns:

the program element at the given position

Throws:

java.lang.ArrayIndexOutOfBoundsException - if index is out of bounds

isStatic

public boolean isStatic(Services services)

visit

public void visit(Visitor v)

calls the corresponding method of a visitor in order to perform some action/transformation on this element

Specified by:

visit in interface SourceElement

Parameters:

v - the Visitor

prettyPrint

public void prettyPrint(PrettyPrinter p)
                 throws java.io.IOException

Description copied from class: JavaSourceElement

Pretty printing the source element.

Specified by:

prettyPrint in interface SourceElement

Overrides:

prettyPrint in class JavaProgramElement

Parameters:

p - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.

getResultVariable

public IProgramVariable getResultVariable()

getBodySource

public KeYJavaType getBodySource()

getBodySourceAsTypeReference

public TypeReference getBodySourceAsTypeReference()

getProgramMethod

public IProgramMethod getProgramMethod(Services services)

resolveMethod

private void resolveMethod(Services services)

reuseSignature

public java.lang.String reuseSignature(Services services,
                                       ExecutionContext ec)

Description copied from class: JavaProgramElement

this is the default implementation of the signature, which is used to determine program similarity.

Overrides:

reuseSignature in class JavaProgramElement

ec - TODO

getMethodReference

public MethodReference getMethodReference()

replaceBySpecification

public boolean replaceBySpecification()