public class MethodBodyStatement extends JavaNonTerminalProgramElement implements Statement, NonTerminalProgramElement
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 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
|
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
|
compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren
getComments, hashCode, prettyPrintMain
getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getComments, match
equalsModRenaming, getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getPositionInfo, getRelativePosition, getStartPosition
private final IProgramVariable resultVar
private final TypeReference bodySource
private final MethodReference methodReference
private IProgramMethod method
private boolean useSpecification
public MethodBodyStatement(TypeReference bodySource, IProgramVariable resultVar, MethodReference methodReference)
bodySource
- exact class where the body is declaredresultVar
- the IProgramVariable to which the method's return value is assignedmethodReference
- the MethodReference encapsulating the method's signaturepublic MethodBodyStatement(ExtList list)
public MethodBodyStatement(IProgramMethod method, ReferencePrefix newContext, IProgramVariable res, ImmutableArray<Expression> args, boolean useSpecification)
public MethodBodyStatement(IProgramMethod method, ReferencePrefix newContext, IProgramVariable res, ImmutableArray<Expression> args, boolean useSpecification, ProgramElement scope)
public MethodBodyStatement(IProgramMethod method, ReferencePrefix newContext, IProgramVariable res, ImmutableArray<Expression> args)
public MethodBodyStatement(IProgramMethod method, ReferencePrefix newContext, IProgramVariable res, ImmutableArray<Expression> args, ProgramElement scope)
private void checkOnlyProgramVarsAsArguments(ImmutableArray<? extends Expression> arguments)
public int getChildCount()
getChildCount
in interface NonTerminalProgramElement
public ReferencePrefix getDesignatedContext()
public ImmutableArray<? extends Expression> getArguments()
public ProgramElement getChildAt(int index)
getChildAt
in interface NonTerminalProgramElement
index
- an index into this node's "virtual" child arrayjava.lang.ArrayIndexOutOfBoundsException
- if index is out
of boundspublic boolean isStatic(Services services)
public void visit(Visitor v)
visit
in interface SourceElement
v
- the Visitorpublic void prettyPrint(PrettyPrinter p) throws java.io.IOException
JavaSourceElement
prettyPrint
in interface SourceElement
prettyPrint
in class JavaProgramElement
p
- a pretty printer.java.io.IOException
- occasionally thrown.public IProgramVariable getResultVariable()
public KeYJavaType getBodySource()
public TypeReference getBodySourceAsTypeReference()
public IProgramMethod getProgramMethod(Services services)
private void resolveMethod(Services services)
public java.lang.String reuseSignature(Services services, ExecutionContext ec)
JavaProgramElement
reuseSignature
in class JavaProgramElement
ec
- TODOpublic MethodReference getMethodReference()
public boolean replaceBySpecification()