public final class ProgramSV extends AbstractSV implements ProgramConstruct, UpdateableOperator
Modifier and Type | Field and Description |
---|---|
private static ProgramList |
EMPTY_LIST_INSTANTIATION |
private boolean |
isListSV |
Constructor and Description |
---|
ProgramSV(Name name,
ProgramSVSort s,
boolean isListSV)
creates a new SchemaVariable used as a placeholder for program constructs
|
Modifier and Type | Method and Description |
---|---|
private MatchConditions |
addProgramInstantiation(ProgramElement pe,
MatchConditions matchCond,
Services services)
adds a found mapping from schema variable
var to program
element pe and returns the updated match conditions or null
if mapping is not possible because of violating some variable condition |
private MatchConditions |
addProgramInstantiation(ProgramList list,
MatchConditions matchCond,
Services services)
adds a found mapping from schema variable
var to the list of
program elements list and returns the updated match
conditions or null if mapping is not possible because of violating some
variable condition |
private boolean |
check(ProgramElement match,
ExecutionContext ec,
Services services)
returns true, if the given SchemaVariable can stand for the
ProgramElement
|
ImmutableList<LocationVariable> |
collectParameters() |
boolean |
equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
this method tests on object identity
|
StatementBlock |
getBody() |
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.
|
Comment[] |
getComments()
Get comments.
|
KeYJavaType |
getContainerType()
Returns the container type of this symbol; for non-static observer
symbols, this corresponds to the sort of its second argument.
|
int |
getDimensions() |
Position |
getEndPosition()
Returns the end position of the primary token of this element.
|
Expression |
getExpressionAt(int index) |
int |
getExpressionCount()
Get the number of expressions in this container.
|
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() |
int |
getHeapCount(Services services)
Check the heap count of the declaration, e.g. the base heap and extra heap.
|
ImmutableArray<LoopInitializer> |
getInits() |
KeYJavaType |
getKeYJavaType() |
KeYJavaType |
getKeYJavaType(Services javaServ) |
KeYJavaType |
getKeYJavaType(Services javaServ,
ExecutionContext ec)
returns the
KeYJavaType of an expression |
SourceElement |
getLastElement()
Finds the source element that occurs last in the source.
|
IProgramMethod |
getMethodContext()
returns the program method which is currently active
|
MethodDeclaration |
getMethodDeclaration() |
ImmutableArray<Modifier> |
getModifiers()
Get the modifiers.
|
java.lang.String |
getName()
Return the name of the model element.
|
int |
getNumParams()
Gives the number of parameters of the observer symbol.
|
PackageReference |
getPackageReference()
Get the package reference.
|
ParameterDeclaration |
getParameterDeclarationAt(int index) |
int |
getParameterDeclarationCount() |
ImmutableArray<ParameterDeclaration> |
getParameters() |
KeYJavaType |
getParameterType(int i)
returns the KeYJavaType of the i-th parameter declaration.
|
KeYJavaType |
getParamType(int i)
Gives the type of the i-th parameter of this observer symbol.
|
ImmutableArray<KeYJavaType> |
getParamTypes()
Returns the parameter types of this observer symbol.
|
PositionInfo |
getPositionInfo()
complete position information
|
ProgramElementName |
getProgramElementName()
Get identifier.
|
ReferencePrefix |
getReferencePrefix() |
Position |
getRelativePosition()
Returns the relative position (number of blank heading lines and
columns) of the primary token of this element.
|
KeYJavaType |
getReturnType() |
ReferencePrefix |
getRuntimeInstance()
returns the runtime instance object
|
Position |
getStartPosition()
Returns the start position of the primary token of this element.
|
int |
getStateCount()
Check the state count of the declaration (no_state = 0, two_state = 2, 1 otherwise).
|
Statement |
getStatementAt(int i) |
int |
getStatementCount()
Get the number of statements in this container.
|
Throws |
getThrown() |
KeYJavaType |
getType()
Returns the result type of this symbol.
|
TypeReference |
getTypeReference()
returns the type reference to the next enclosing class
|
TypeReference |
getTypeReferenceAt(int index) |
int |
getTypeReferenceCount()
Get the number of type references in this container.
|
java.lang.String |
getUniqueName() |
ImmutableArray<Expression> |
getUpdates() |
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 |
isListSV() |
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 |
isStatic()
Tells whether the observer symbol is static.
|
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.
|
private MatchConditions |
matchListSV(SourceData source,
MatchConditions matchCond) |
void |
prettyPrint(PrettyPrinter w)
Pretty print.
|
java.lang.String |
proofToString()
Creates a parseable string representation of the declaration of the
schema variable.
|
int |
size() |
java.lang.String |
toString() |
void |
visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
isStrict, toString
additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort
arity, bindVarsAt, isRigid, name, validTopLevel, whereToBind
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevel
private static final ProgramList EMPTY_LIST_INSTANTIATION
private final boolean isListSV
ProgramSV(Name name, ProgramSVSort s, boolean isListSV)
name
- the Name of the SchemaVariable allowed to match a list of
program constructspublic boolean isListSV()
public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat)
equalsModRenaming
in interface SourceElement
public Comment[] getComments()
ProgramElement
getComments
in interface Label
getComments
in interface ProgramElement
public SourceElement getFirstElement()
SourceElement
getFirstElement
in interface Label
getFirstElement
in interface SourceElement
SourceElement.getStartPosition()
public SourceElement getFirstElementIncludingBlocks()
SourceElement
getFirstElementIncludingBlocks
in interface SourceElement
SourceElement.getStartPosition()
public SourceElement getLastElement()
SourceElement
getLastElement
in interface Label
getLastElement
in interface SourceElement
SourceElement.getEndPosition()
public Position getStartPosition()
SourceElement
getFirstElement()
.getStartPosition
in interface Label
getStartPosition
in interface SourceElement
public Position getEndPosition()
SourceElement
getLastElement()
.getEndPosition
in interface Label
getEndPosition
in interface SourceElement
public Position getRelativePosition()
SourceElement
getFirstElement()
.getRelativePosition
in interface Label
getRelativePosition
in interface SourceElement
public PositionInfo getPositionInfo()
SourceElement
getPositionInfo
in interface SourceElement
public ReferencePrefix getReferencePrefix()
getReferencePrefix
in interface ReferencePrefix
getReferencePrefix
in interface TypeReference
public int getDimensions()
getDimensions
in interface TypeReference
public int getTypeReferenceCount()
TypeReferenceContainer
getTypeReferenceCount
in interface TypeReferenceContainer
public TypeReference getTypeReferenceAt(int index)
getTypeReferenceAt
in interface TypeReferenceContainer
public PackageReference getPackageReference()
PackageReferenceContainer
getPackageReference
in interface PackageReferenceContainer
public int getExpressionCount()
ExpressionContainer
getExpressionCount
in interface ExpressionContainer
public Expression getExpressionAt(int index)
getExpressionAt
in interface ExpressionContainer
getExpressionAt
in interface IForUpdates
public int getChildCount()
NonTerminalProgramElement
getChildCount
in interface NonTerminalProgramElement
public ProgramElement getChildAt(int index)
NonTerminalProgramElement
getChildAt
in interface NonTerminalProgramElement
index
- an index into this node's "virtual" child arraypublic int getStatementCount()
StatementContainer
getStatementCount
in interface StatementContainer
public int size()
size
in interface IForUpdates
size
in interface ILoopInit
public ImmutableArray<Expression> getUpdates()
getUpdates
in interface IForUpdates
public ImmutableArray<LoopInitializer> getInits()
public Statement getStatementAt(int i)
getStatementAt
in interface StatementContainer
public ProgramElementName getProgramElementName()
NamedProgramElement
getProgramElementName
in interface NamedProgramElement
getProgramElementName
in interface TypeReference
getProgramElementName
in interface IProgramMethod
public java.lang.String getName()
NamedModelElement
getName
in interface NamedModelElement
getName
in interface TypeReference
getName
in interface IProgramMethod
public void visit(Visitor v)
SourceElement
visit
in interface Label
visit
in interface SourceElement
v
- the Visitorpublic void prettyPrint(PrettyPrinter w) throws java.io.IOException
SourceElement
prettyPrint
in interface Label
prettyPrint
in interface SourceElement
w
- a pretty printer.java.io.IOException
- occasionally thrown.public KeYJavaType getKeYJavaType()
getKeYJavaType
in interface TypeReference
getKeYJavaType
in interface IProgramVariable
public KeYJavaType getKeYJavaType(Services javaServ)
getKeYJavaType
in interface IProgramVariable
public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec)
Expression
KeYJavaType
of an expressiongetKeYJavaType
in interface Expression
getKeYJavaType
in interface IProgramVariable
private MatchConditions addProgramInstantiation(ProgramElement pe, MatchConditions matchCond, Services services)
var
to program
element pe
and returns the updated match conditions or null
if mapping is not possible because of violating some variable conditionpe
- the ProgramElement var
is mapped tomatchCond
- the MatchConditions to be updatedservices
- the Services provide access to the Java modelvar
to pe
or null if some variable condition would be
hurt by the mappingprivate MatchConditions addProgramInstantiation(ProgramList list, MatchConditions matchCond, Services services)
var
to the list of
program elements list
and returns the updated match
conditions or null if mapping is not possible because of violating some
variable conditionlist
- the ProgramList var
is mapped tomatchCond
- the MatchConditions to be updatedservices
- the Services provide access to the Java modelvar
to list
or null if some variable condition would be
hurt by the mappingprivate MatchConditions matchListSV(SourceData source, MatchConditions matchCond)
private boolean check(ProgramElement match, ExecutionContext ec, Services services)
match
- the ProgramElement to be matchedservices
- the Services object encapsulating information about the java
datastructures like (static)types etc.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 java.lang.String toString()
toString
in class AbstractOperator
public java.lang.String proofToString()
SchemaVariable
proofToString
in interface SchemaVariable
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 boolean isConstructor()
IProgramMethod
isConstructor
in interface IProgramMethod
public boolean isModel()
IProgramMethod
isModel
in interface IProgramMethod
public int getStateCount()
IObserverFunction
getStateCount
in interface IObserverFunction
public int getHeapCount(Services services)
IObserverFunction
getHeapCount
in interface IObserverFunction
public boolean isVoid()
isVoid
in interface IProgramMethod
public KeYJavaType getReturnType()
getReturnType
in interface IProgramMethod
public java.lang.String getUniqueName()
getUniqueName
in interface IProgramMethod
public java.lang.String getFullName()
getFullName
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 ImmutableList<LocationVariable> collectParameters()
collectParameters
in interface IProgramMethod
LocationVariable
s passed as parameters to
this IProgramMethod
.public boolean isPrivate()
MemberDeclaration
isPrivate
in interface MemberDeclaration
public boolean isProtected()
MemberDeclaration
isProtected
in interface MemberDeclaration
public boolean isPublic()
MemberDeclaration
isPublic
in interface MemberDeclaration
public boolean isStatic()
IObserverFunction
isStatic
in interface MemberDeclaration
isStatic
in interface IObserverFunction
public boolean isStrictFp()
MemberDeclaration
isStrictFp
in interface MemberDeclaration
public ImmutableArray<Modifier> getModifiers()
Declaration
getModifiers
in interface Declaration
public ImmutableArray<KeYJavaType> getParamTypes()
IObserverFunction
getParamTypes
in interface IObserverFunction
getParamTypes
in interface IProgramMethod
public KeYJavaType getType()
IObserverFunction
getType
in interface IObserverFunction
public KeYJavaType getContainerType()
IObserverFunction
getContainerType
in interface IObserverFunction
public int getNumParams()
IObserverFunction
getNumParams
in interface IObserverFunction
public KeYJavaType getParamType(int i)
IObserverFunction
getParamType
in interface IObserverFunction
public TypeReference getTypeReference()
IExecutionContext
getTypeReference
in interface IExecutionContext
public IProgramMethod getMethodContext()
IExecutionContext
getMethodContext
in interface IExecutionContext
public ReferencePrefix getRuntimeInstance()
IExecutionContext
getRuntimeInstance
in interface IExecutionContext