public final class ProgramMethod extends ObserverFunction implements ProgramInLogic, IProgramMethod
Modifier and Type | Field and Description |
---|---|
private MethodDeclaration |
method |
private PositionInfo |
pi |
private KeYJavaType |
returnType
Return type of the method.
|
Constructor and Description |
---|
ProgramMethod(MethodDeclaration method,
KeYJavaType container,
KeYJavaType kjt,
PositionInfo pi,
Sort heapSort) |
ProgramMethod(MethodDeclaration method,
KeYJavaType container,
KeYJavaType kjt,
PositionInfo pi,
Sort heapSort,
int heapCount) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<LocationVariable> |
collectParameters() |
Expression |
convertToProgram(Term t,
ExtList l) |
boolean |
equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
equals modulo renaming is described in class SourceElement.
|
StatementBlock |
getBody() |
ProgramElement |
getChildAt(int i)
Returns the child at the specified index in this node's "virtual"
child array.
|
int |
getChildCount()
Returns the number of children of this node.
|
Comment[] |
getComments()
Get comments.
|
Position |
getEndPosition()
Returns the end position of the primary token of this element.
|
SourceElement |
getFirstElement()
Finds the source element that occurs first in the source.
|
SourceElement |
getFirstElementIncludingBlocks()
Finds the source element that occurs first in the source.
|
java.lang.String |
getFullName() |
KeYJavaType |
getKJT()
Deprecated.
|
SourceElement |
getLastElement()
Finds the source element that occurs last in the source.
|
MethodDeclaration |
getMethodDeclaration() |
ImmutableArray<Modifier> |
getModifiers()
Get the modifiers.
|
java.lang.String |
getName() |
ParameterDeclaration |
getParameterDeclarationAt(int index) |
int |
getParameterDeclarationCount() |
ImmutableArray<ParameterDeclaration> |
getParameters() |
KeYJavaType |
getParameterType(int i)
returns the KeYJavaType of the i-th parameter declaration.
|
private static ImmutableArray<KeYJavaType> |
getParamTypes(MethodDeclaration md) |
PositionInfo |
getPositionInfo()
complete position information
|
ProgramElementName |
getProgramElementName() |
Position |
getRelativePosition()
Returns the relative position (number of blank heading lines and columns)
of the primary token of this element.
|
KeYJavaType |
getReturnType() |
Position |
getStartPosition()
Returns the start position of the primary token of this element.
|
Throws |
getThrown() |
java.lang.String |
getUniqueName() |
VariableSpecification |
getVariableSpecification(int index)
Returns the variablespecification of the i-th parameterdeclaration
|
boolean |
isAbstract() |
boolean |
isConstructor()
Test whether the declaration is a constructor.
|
boolean |
isFinal() |
boolean |
isImplicit() |
boolean |
isModel()
Test whether the declaration is model.
|
boolean |
isNative() |
boolean |
isPrivate()
Test whether the declaration is private.
|
boolean |
isProtected()
Test whether the declaration is protected.
|
boolean |
isPublic()
Test whether the declaration is public.
|
boolean |
isStrictFp()
Test whether the declaration is strictfp.
|
boolean |
isSynchronized() |
boolean |
isVoid() |
MatchConditions |
match(SourceData source,
MatchConditions matchCond)
matches the source "text" (@link SourceData#getSource()) against the pattern represented
by this object.
|
void |
prettyPrint(PrettyPrinter w)
Pretty print.
|
void |
visit(Visitor v)
calls the corresponding method of a visitor in order to perform some
action/transformation on this element
|
createName, getContainerType, getHeapCount, getNumParams, getParamType, getParamTypes, getStateCount, getType, isStatic
isSkolemConstant, isUnique, proofToString, rename, toString
additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort
arity, bindVarsAt, isRigid, name, validTopLevel, whereToBind
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getParamTypes
getContainerType, getHeapCount, getNumParams, getParamType, getStateCount, getType, isStatic
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevel
isStatic
private final MethodDeclaration method
private final KeYJavaType returnType
private final PositionInfo pi
public ProgramMethod(MethodDeclaration method, KeYJavaType container, KeYJavaType kjt, PositionInfo pi, Sort heapSort)
public ProgramMethod(MethodDeclaration method, KeYJavaType container, KeYJavaType kjt, PositionInfo pi, Sort heapSort, int heapCount)
private static ImmutableArray<KeYJavaType> getParamTypes(MethodDeclaration md)
public MethodDeclaration getMethodDeclaration()
getMethodDeclaration
in interface IProgramMethod
public KeYJavaType getParameterType(int i)
IProgramMethod
getParameterType
in interface IProgramMethod
i
- the int specifying the parameter positionpublic StatementBlock getBody()
getBody
in interface IProgramMethod
public SourceElement getFirstElement()
SourceElement
getFirstElement
in interface SourceElement
SourceElement.getStartPosition()
public SourceElement getFirstElementIncludingBlocks()
SourceElement
getFirstElementIncludingBlocks
in interface SourceElement
SourceElement.getStartPosition()
public SourceElement getLastElement()
SourceElement
getLastElement
in interface SourceElement
SourceElement.getEndPosition()
public Comment[] getComments()
ProgramElement
getComments
in interface ProgramElement
public void prettyPrint(PrettyPrinter w) throws java.io.IOException
SourceElement
prettyPrint
in interface SourceElement
w
- a pretty printer.java.io.IOException
- occasionally thrown.public void visit(Visitor v)
visit
in interface SourceElement
v
- the Visitorpublic Position getStartPosition()
getFirstElement()
.getStartPosition
in interface SourceElement
public Position getEndPosition()
getLastElement()
.getEndPosition
in interface SourceElement
public Position getRelativePosition()
getFirstElement()
.getRelativePosition
in interface SourceElement
public PositionInfo getPositionInfo()
SourceElement
getPositionInfo
in interface SourceElement
public boolean isPrivate()
isPrivate
in interface MemberDeclaration
public boolean isProtected()
isProtected
in interface MemberDeclaration
public boolean isPublic()
isPublic
in interface MemberDeclaration
public boolean isConstructor()
IProgramMethod
isConstructor
in interface IProgramMethod
public boolean isModel()
IProgramMethod
isModel
in interface IProgramMethod
public boolean isStrictFp()
isStrictFp
in interface MemberDeclaration
public boolean isVoid()
isVoid
in interface IProgramMethod
public ImmutableArray<Modifier> getModifiers()
Declaration
getModifiers
in interface Declaration
public int getChildCount()
NonTerminalProgramElement
getChildCount
in interface NonTerminalProgramElement
public ProgramElement getChildAt(int i)
NonTerminalProgramElement
getChildAt
in interface NonTerminalProgramElement
i
- an index into this node's "virtual" child arraypublic boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat)
equalsModRenaming
in interface SourceElement
@Deprecated public KeYJavaType getKJT()
public KeYJavaType getReturnType()
getReturnType
in interface IProgramMethod
public Expression convertToProgram(Term t, ExtList l)
convertToProgram
in interface ProgramInLogic
public ProgramElementName getProgramElementName()
getProgramElementName
in interface IProgramMethod
public java.lang.String getUniqueName()
getUniqueName
in interface IProgramMethod
public java.lang.String getFullName()
getFullName
in interface IProgramMethod
public java.lang.String getName()
getName
in interface IProgramMethod
public boolean isAbstract()
isAbstract
in interface IProgramMethod
public boolean isImplicit()
isImplicit
in interface IProgramMethod
public boolean isNative()
isNative
in interface IProgramMethod
public boolean isFinal()
isFinal
in interface IProgramMethod
public boolean isSynchronized()
isSynchronized
in interface IProgramMethod
public Throws getThrown()
getThrown
in interface IProgramMethod
public ParameterDeclaration getParameterDeclarationAt(int index)
getParameterDeclarationAt
in interface IProgramMethod
public VariableSpecification getVariableSpecification(int index)
IProgramMethod
getVariableSpecification
in interface IProgramMethod
public int getParameterDeclarationCount()
getParameterDeclarationCount
in interface IProgramMethod
public ImmutableArray<ParameterDeclaration> getParameters()
getParameters
in interface IProgramMethod
public MatchConditions match(SourceData source, MatchConditions matchCond)
ProgramElement
MatchConditions
with
the found instantiations of the schemavariables. If the match
failed, null is returned instead.match
in interface ProgramElement
source
- the SourceData with the program element to matchmatchCond
- the MatchConditions found up to this pointpublic ImmutableList<LocationVariable> collectParameters()
collectParameters
in interface IProgramMethod
LocationVariable
s passed as parameters to
this IProgramMethod
.