public class MethodBodyStatement extends JavaNonTerminalProgramElement implements Statement, NonTerminalProgramElement
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 |
---|---|
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() |
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
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)
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)
public java.lang.String reuseSignature(Services services, ExecutionContext ec)
JavaProgramElement
reuseSignature
in class JavaProgramElement
ec
- TODOpublic MethodReference getMethodReference()
public boolean replaceBySpecification()
Copyright © 2003-2019 The KeY-Project.