public final class ProgramMethod extends ObserverFunction implements ProgramInLogic, IProgramMethod
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 |
---|---|
int |
arity()
the arity of this operator
|
boolean |
bindVarsAt(int n)
Tells whether the operator binds variables at the n-th subterm.
|
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.
|
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 |
isRigid()
Tells whether the operator is rigid.
|
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.
|
Name |
name()
returns the name of this element
|
void |
prettyPrint(PrettyPrinter w)
Pretty print.
|
void |
validTopLevelException(Term term)
Checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator.
|
void |
visit(Visitor v)
calls the corresponding method of a visitor in order to perform some
action/transformation on this element
|
protected ImmutableArray<java.lang.Boolean> |
whereToBind() |
createName, getContainerType, getHeapCount, getNumParams, getParamType, getParamTypes, getStateCount, getType, isStatic
isSkolemConstant, isUnique, proofToString, rename, toString
additionalValidTopLevel, argSort, argSorts, sort, sort
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, validTopLevelException
isStatic
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)
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
.protected final ImmutableArray<java.lang.Boolean> whereToBind()
public final Name name()
Named
public final int arity()
Operator
public final boolean bindVarsAt(int n)
Operator
bindVarsAt
in interface Operator
public final boolean isRigid()
Operator
public void validTopLevelException(Term term) throws TermCreationException
Operator
validTopLevelException
in interface Operator
TermCreationException
- if a construction error was recogniseCopyright © 2003-2019 The KeY-Project.