public class WhileLoopTransformation extends JavaASTVisitor
Modifier and Type | Class and Description |
---|---|
private class |
WhileLoopTransformation.DefaultAction |
Modifier and Type | Field and Description |
---|---|
protected Break |
breakInnerLabel
break innerlabel
|
protected Break |
breakOuterLabel
break outerlabel
|
protected static java.lang.Boolean |
CHANGED |
protected static int |
CHECK |
protected SVInstantiations |
instantiations
if run in check mode there are normally schemavaribles, so we need the
instantiations of them
|
protected ExtList |
labelList |
protected java.util.Stack<Label> |
labelStack |
protected java.util.Stack<MethodFrame> |
methodStack |
protected boolean |
needInnerLabel
Indicates if an unlabled continue has been found or if a labelled
continue with a label outside of the loop currently transformed has
been found.
|
protected boolean |
needOuterLabel
indicates if an unlabled break has been found and an outer
label is needed
|
protected int |
newLabels
counts the number of labelled continues with an label outside the
while loop that is transformed
|
protected int |
replaceBreakWithNoLabel
if there is a loop inside the loop the breaks of these inner loops have
not to be replaced.
|
protected ProgramElement |
replacement
the replacement element
|
protected ProgramElement |
result
the result of the transformation
|
protected int |
runMode
there are two modes the visitor can be run.
|
protected java.util.Stack<ExtList> |
stack |
protected static int |
TRANSFORMATION |
services
Constructor and Description |
---|
WhileLoopTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
WhileLoopTransformation(ProgramElement root,
SVInstantiations inst,
Services services)
creates the WhileLoopTransformation for the check mode
|
Modifier and Type | Method and Description |
---|---|
protected void |
addChild(SourceElement x) |
protected void |
changed() |
protected void |
doAction(ProgramElement node)
the action that is performed just before leaving the node the
last time
|
protected void |
doDefaultAction(SourceElement x)
the implemented default action is called if a program element is,
and if it has children all its children too are left unchanged
|
private static Guard |
getForGuard(For x,
ExtList changeList) |
private static Statement[] |
getInnerBlockStatements(IForUpdates updates,
Statement body,
For remainder,
int updateSize) |
boolean |
innerLabelNeeded()
returns true if an inner label is needed
|
boolean |
outerLabelNeeded()
returns true if an outer label is needed
|
void |
performActionOnBreak(Break x) |
void |
performActionOnCase(Case x) |
void |
performActionOnCatch(Catch x) |
void |
performActionOnContinue(Continue x) |
void |
performActionOnCopyAssignment(CopyAssignment x) |
void |
performActionOnDefault(Default x) |
void |
performActionOnDo(Do x) |
void |
performActionOnElse(Else x) |
void |
performActionOnEnhancedFor(EnhancedFor x)
perform the loop transformation on an enhanced for loop (Java5)
If the enhanced for loop is the toplevel loop nothing happens -
return the loop itself, as enhanced for loops cannot be unwound,
a log message is issued.
|
void |
performActionOnFinally(Finally x) |
void |
performActionOnFor(For x)
public void performActionOnFor(For x) {
ExtList changeList = stack.peek();
if (replaceBreakWithNoLabel==0) {
//most outer for loop
if (changeList.getFirst() == CHANGED)
changeList.removeFirst();
LoopInitializer init[] =
new LoopInitializer[x.getInitializers().size()];
Expression[] updates =
new Expression[x.getUpdates().size()];
s
//the unchanged updates need to be extracted to initialize the
//remainding 'for' statement
Expression[] unchangedUpdates =
new Expression[x.getUpdates().size()];
Expression guard = null;
Statement body = null;
ProgramElement element =
(ProgramElement) (changeList.isEmpty() ?
|
void |
performActionOnIf(If x) |
void |
performActionOnLabeledStatement(LabeledStatement x) |
void |
performActionOnLocalVariableDeclaration(LocalVariableDeclaration x) |
void |
performActionOnMethodFrame(MethodFrame x) |
void |
performActionOnSchemaVariable(SchemaVariable sv) |
void |
performActionOnStatementBlock(StatementBlock x) |
void |
performActionOnSwitch(Switch x) |
void |
performActionOnSynchronizedBlock(SynchronizedBlock x) |
void |
performActionOnThen(Then x) |
void |
performActionOnTry(Try x) |
void |
performActionOnWhile(While x)
Performs the unwinding of the loop
Warning: The unwinding does not comply with the rule in the KeY book up to 100%
The difference is revealed by the following example:
Label1:while(c){b}
According to the KeY book the transformation should be
if(c) l':{l'':{p#} Label1:while(c){b}}
This implementation creates however. |
protected boolean |
replaceJumpStatement(LabelJumpStatement x) |
ProgramElement |
result() |
void |
start()
starts the walker
|
java.lang.String |
toString() |
protected void |
walk(ProgramElement node)
walks through the AST.
|
performActionOnAbstractProgramElement, performActionOnAllFields, performActionOnAllObjects, performActionOnArrayDeclaration, performActionOnArrayInitializer, performActionOnArrayLengthReference, performActionOnArrayReference, performActionOnAssert, performActionOnBinaryAnd, performActionOnBinaryAndAssignment, performActionOnBinaryNot, performActionOnBinaryOr, performActionOnBinaryOrAssignment, performActionOnBinaryXOr, performActionOnBinaryXOrAssignment, performActionOnBlockContract, performActionOnBlockContract, performActionOnBooleanLiteral, performActionOnCatchAllStatement, performActionOnCharLiteral, performActionOnClassDeclaration, performActionOnClassInitializer, performActionOnComment, performActionOnCompilationUnit, performActionOnConditional, performActionOnConstructorDeclaration, performActionOnContextStatementBlock, performActionOnDivide, performActionOnDivideAssignment, performActionOnDLEmbeddedExpression, performActionOnDoubleLiteral, performActionOnEmptyMapLiteral, performActionOnEmptySeqLiteral, performActionOnEmptySetLiteral, performActionOnEmptyStatement, performActionOnEquals, performActionOnExactInstanceof, performActionOnExecutionContext, performActionOnExtends, performActionOnFieldDeclaration, performActionOnFieldReference, performActionOnFieldSpecification, performActionOnFloatLiteral, performActionOnForUpdates, performActionOnGreaterOrEquals, performActionOnGreaterThan, performActionOnGuard, performActionOnImplements, performActionOnImplicitFieldSpecification, performActionOnImport, performActionOnInstanceof, performActionOnInterfaceDeclaration, performActionOnIntersect, performActionOnIntLiteral, performActionOnIProgramVariable, performActionOnLessOrEquals, performActionOnLessThan, performActionOnLocationVariable, performActionOnLogicalAnd, performActionOnLogicalNot, performActionOnLogicalOr, performActionOnLongLiteral, performActionOnLoopContract, performActionOnLoopContract, performActionOnLoopContract, performActionOnLoopInit, performActionOnLoopInvariant, performActionOnLoopScopeBlock, performActionOnMergeContract, performActionOnMergePointStatement, performActionOnMetaClassReference, performActionOnMethod, performActionOnMethodBodyStatement, performActionOnMethodDeclaration, performActionOnMethodReference, performActionOnMinus, performActionOnMinusAssignment, performActionOnModifier, performActionOnModulo, performActionOnModuloAssignment, performActionOnNegative, performActionOnNew, performActionOnNewArray, performActionOnNotEquals, performActionOnNullLiteral, performActionOnPackageReference, performActionOnPackageSpecification, performActionOnParameterDeclaration, performActionOnParenthesizedExpression, performActionOnPassiveExpression, performActionOnPlus, performActionOnPlusAssignment, performActionOnPositive, performActionOnPostDecrement, performActionOnPostIncrement, performActionOnPreDecrement, performActionOnPreIncrement, performActionOnProgramConstant, performActionOnProgramElementName, performActionOnProgramMetaConstruct, performActionOnProgramMethod, performActionOnProgramVariable, performActionOnReturn, performActionOnSchematicFieldReference, performActionOnSeqConcat, performActionOnSeqGet, performActionOnSeqIndexOf, performActionOnSeqLength, performActionOnSeqReverse, performActionOnSeqSingleton, performActionOnSeqSub, performActionOnSetMinus, performActionOnSetUnion, performActionOnShiftLeft, performActionOnShiftLeftAssignment, performActionOnShiftRight, performActionOnShiftRightAssignment, performActionOnSingleton, performActionOnStringLiteral, performActionOnSuperArrayDeclaration, performActionOnSuperConstructorReference, performActionOnSuperReference, performActionOnThisConstructorReference, performActionOnThisReference, performActionOnThrow, performActionOnThrows, performActionOnTimes, performActionOnTimesAssignment, performActionOnTransactionStatement, performActionOnTypeCast, performActionOnTypeReference, performActionOnUnsignedShiftRight, performActionOnUnsignedShiftRightAssignment, performActionOnVariableDeclaration, performActionOnVariableReference, performActionOnVariableSpecification
depth, root
protected static final java.lang.Boolean CHANGED
protected static final int TRANSFORMATION
protected static final int CHECK
protected ProgramElement replacement
protected Break breakOuterLabel
protected Break breakInnerLabel
protected ExtList labelList
protected java.util.Stack<ExtList> stack
protected int replaceBreakWithNoLabel
protected int runMode
protected boolean needOuterLabel
protected boolean needInnerLabel
protected int newLabels
protected SVInstantiations instantiations
protected ProgramElement result
protected java.util.Stack<Label> labelStack
protected java.util.Stack<MethodFrame> methodStack
public WhileLoopTransformation(ProgramElement root, ProgramElementName outerLabel, ProgramElementName innerLabel, Services services)
root
- the ProgramElement where to beginouterLabel
- the ProgramElementName of the outer labelinnerLabel
- the ProgramElementName of the inner labelservices
- services instancepublic WhileLoopTransformation(ProgramElement root, SVInstantiations inst, Services services)
root
- the ProgramElement where to begininst
- the SVInstantiations if availableservices
- services instanceprivate static Statement[] getInnerBlockStatements(IForUpdates updates, Statement body, For remainder, int updateSize)
public boolean innerLabelNeeded()
public boolean outerLabelNeeded()
protected void doAction(ProgramElement node)
doAction
in class JavaASTVisitor
node
- respective node as program elementpublic void start()
start
in class JavaASTWalker
public ProgramElement result()
protected void walk(ProgramElement node)
walk
in class JavaASTVisitor
node
- the JavaProgramElement the walker is atpublic java.lang.String toString()
toString
in class java.lang.Object
protected void doDefaultAction(SourceElement x)
doDefaultAction
in class JavaASTVisitor
x
- source elementpublic void performActionOnSchemaVariable(SchemaVariable sv)
performActionOnSchemaVariable
in interface Visitor
performActionOnSchemaVariable
in class JavaASTVisitor
public void performActionOnLocalVariableDeclaration(LocalVariableDeclaration x)
performActionOnLocalVariableDeclaration
in interface Visitor
performActionOnLocalVariableDeclaration
in class JavaASTVisitor
public void performActionOnStatementBlock(StatementBlock x)
performActionOnStatementBlock
in interface Visitor
performActionOnStatementBlock
in class JavaASTVisitor
protected boolean replaceJumpStatement(LabelJumpStatement x)
public void performActionOnBreak(Break x)
performActionOnBreak
in interface Visitor
performActionOnBreak
in class JavaASTVisitor
public void performActionOnContinue(Continue x)
performActionOnContinue
in interface Visitor
performActionOnContinue
in class JavaASTVisitor
public void performActionOnFor(For x)
performActionOnFor
in interface Visitor
performActionOnFor
in class JavaASTVisitor
x
- For loop statementpublic void performActionOnEnhancedFor(EnhancedFor x)
performActionOnEnhancedFor
in interface Visitor
performActionOnEnhancedFor
in class JavaASTVisitor
x
- EnhancedFor loop statementpublic void performActionOnWhile(While x)
Label1:while(c){b}
According to the KeY book the transformation should be
if(c) l':{l'':{p#} Label1:while(c){b}}
This implementation creates however.
Label1:if(c) l':{l'':{p#} while(c){b}}
Check if this is ok when labeled continue statements are involved.performActionOnWhile
in interface Visitor
performActionOnWhile
in class JavaASTVisitor
x
- the while statementpublic void performActionOnDo(Do x)
performActionOnDo
in interface Visitor
performActionOnDo
in class JavaASTVisitor
public void performActionOnIf(If x)
performActionOnIf
in interface Visitor
performActionOnIf
in class JavaASTVisitor
public void performActionOnSwitch(Switch x)
performActionOnSwitch
in interface Visitor
performActionOnSwitch
in class JavaASTVisitor
public void performActionOnTry(Try x)
performActionOnTry
in interface Visitor
performActionOnTry
in class JavaASTVisitor
public void performActionOnLabeledStatement(LabeledStatement x)
performActionOnLabeledStatement
in interface Visitor
performActionOnLabeledStatement
in class JavaASTVisitor
public void performActionOnMethodFrame(MethodFrame x)
performActionOnMethodFrame
in interface Visitor
performActionOnMethodFrame
in class JavaASTVisitor
public void performActionOnSynchronizedBlock(SynchronizedBlock x)
performActionOnSynchronizedBlock
in interface Visitor
performActionOnSynchronizedBlock
in class JavaASTVisitor
public void performActionOnCopyAssignment(CopyAssignment x)
performActionOnCopyAssignment
in interface Visitor
performActionOnCopyAssignment
in class JavaASTVisitor
public void performActionOnThen(Then x)
performActionOnThen
in interface Visitor
performActionOnThen
in class JavaASTVisitor
public void performActionOnElse(Else x)
performActionOnElse
in interface Visitor
performActionOnElse
in class JavaASTVisitor
public void performActionOnCase(Case x)
performActionOnCase
in interface Visitor
performActionOnCase
in class JavaASTVisitor
public void performActionOnCatch(Catch x)
performActionOnCatch
in interface Visitor
performActionOnCatch
in class JavaASTVisitor
public void performActionOnDefault(Default x)
performActionOnDefault
in interface Visitor
performActionOnDefault
in class JavaASTVisitor
public void performActionOnFinally(Finally x)
performActionOnFinally
in interface Visitor
performActionOnFinally
in class JavaASTVisitor
protected void changed()
protected void addChild(SourceElement x)