public class SynchronizedBlock extends JavaStatement implements StatementContainer, ExpressionContainer, ProgramPrefix
Modifier and Type | Field and Description |
---|---|
protected StatementBlock |
body
Body.
|
protected Expression |
expression
Expression.
|
private MethodFrame |
innerMostMethodFrame |
private int |
prefixLength |
Constructor and Description |
---|
SynchronizedBlock(Expression e,
StatementBlock body)
Synchronized block.
|
SynchronizedBlock(ExtList children)
Synchronized block.
|
SynchronizedBlock(StatementBlock body)
Synchronized block.
|
Modifier and Type | Method and Description |
---|---|
private boolean |
expressionWithoutSideffects()
The method checks whether the expression in the synchronized
prefix is either a local variable or a meta class reference
(as local variables of this type are not supported by KeY,
see return value for
MetaClassReference.getKeYJavaType(Services, ExecutionContext) . |
StatementBlock |
getBody()
Get body.
|
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.
|
Expression |
getExpression()
Get expression.
|
Expression |
getExpressionAt(int index) |
int |
getExpressionCount()
Get the number of expressions in this container.
|
PosInProgram |
getFirstActiveChildPos()
returns the position of the first active child
|
SourceElement |
getFirstElement()
Finds the source element that occurs first in the source.
|
MethodFrame |
getInnerMostMethodFrame()
returns the inner most
MethodFrame |
ProgramPrefix |
getLastPrefixElement()
return the last prefix element
|
ProgramPrefix |
getNextPrefixElement()
return the next prefix element
if no next prefix element is available an IndexOutOfBoundsException is thrown
|
ImmutableArray<ProgramPrefix> |
getPrefixElements()
returns an array with all prefix elements starting at
this element
|
int |
getPrefixLength()
returns the length of the prefix
|
Statement |
getStatementAt(int index) |
int |
getStatementCount()
Get the number of statements in this container.
|
boolean |
hasNextPrefixElement()
return true if there is a next prefix element
|
void |
prettyPrint(PrettyPrinter p)
Pretty printing the source element.
|
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, reuseSignature
getEndPosition, getFirstElementIncludingBlocks, getLastElement, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getComments, match
equalsModRenaming, getEndPosition, getFirstElementIncludingBlocks, getLastElement, getPositionInfo, getRelativePosition, getStartPosition
protected final Expression expression
protected final StatementBlock body
private final MethodFrame innerMostMethodFrame
private final int prefixLength
public SynchronizedBlock(StatementBlock body)
body
- a statement block.public SynchronizedBlock(Expression e, StatementBlock body)
e
- an expression.body
- a statement block.public SynchronizedBlock(ExtList children)
children
- a list with all childrenpublic boolean hasNextPrefixElement()
ProgramPrefix
hasNextPrefixElement
in interface ProgramPrefix
public ProgramPrefix getNextPrefixElement()
ProgramPrefix
getNextPrefixElement
in interface ProgramPrefix
public ProgramPrefix getLastPrefixElement()
ProgramPrefix
getLastPrefixElement
in interface ProgramPrefix
public int getPrefixLength()
ProgramPrefix
getPrefixLength
in interface ProgramPrefix
public MethodFrame getInnerMostMethodFrame()
ProgramPrefix
MethodFrame
getInnerMostMethodFrame
in interface ProgramPrefix
public ImmutableArray<ProgramPrefix> getPrefixElements()
ProgramPrefix
getPrefixElements
in interface ProgramPrefix
private boolean expressionWithoutSideffects()
MetaClassReference.getKeYJavaType(Services, ExecutionContext)
.public PosInProgram getFirstActiveChildPos()
ProgramPrefix
getFirstActiveChildPos
in interface ProgramPrefix
public int getExpressionCount()
getExpressionCount
in interface ExpressionContainer
public Expression getExpressionAt(int index)
getExpressionAt
in interface ExpressionContainer
public Expression getExpression()
public int getChildCount()
getChildCount
in interface NonTerminalProgramElement
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 StatementBlock getBody()
public int getStatementCount()
getStatementCount
in interface StatementContainer
public Statement getStatementAt(int index)
getStatementAt
in interface StatementContainer
public SourceElement getFirstElement()
JavaSourceElement
getFirstElement
in interface SourceElement
getFirstElement
in class JavaSourceElement
JavaSourceElement.toSource()
,
JavaSourceElement.getStartPosition()
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.