de.uka.ilkd.key.java.visitor

Class InnerBreakAndContinueReplacer

java.lang.Object

de.uka.ilkd.key.java.visitor.JavaASTWalker

de.uka.ilkd.key.java.visitor.JavaASTVisitor

de.uka.ilkd.key.java.visitor.InnerBreakAndContinueReplacer

All Implemented Interfaces:

Visitor

public class InnerBreakAndContinueReplacer
extends JavaASTVisitor

This replaces all breaks and continues in a loop with break l, where l is a specified label. It is used in the transformation of a for loop to a while loop.

Author:

lanzinger

See Also:

LoopApplyHeadRule, LoopContractImpl

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	InnerBreakAndContinueReplacer.DefaultAction

Field Summary

Fields

Modifier and Type	Field and Description
private Break	breakInner The break statement used to replace continue statements.
private Break	breakOuter The break statement used to replace break statements.
protected static java.lang.Boolean	CHANGED
private java.util.Stack<MethodFrame>	frames
private int	loopAndSwitchCascadeDepth
private java.util.Stack<Label>	loopLabels
private StatementBlock	result
private java.util.Stack<ExtList>	stack

Fields inherited from class de.uka.ilkd.key.java.visitor.JavaASTVisitor

services

Constructor Summary

Constructors

Constructor and Description
InnerBreakAndContinueReplacer(StatementBlock block, java.lang.Iterable<Label> loopLabels, Label breakLabel, Label continueLabel, Services services)

Method Summary

Modifier and Type	Method and Description
private void	addChild(SourceElement x)
private void	changed()
protected void	doDefaultAction(SourceElement x) the action that is performed just before leaving the node the last time
StatementBlock	getResult()
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)
void	performActionOnFinally(Finally x)
void	performActionOnFor(For x)
void	performActionOnIf(If x)
void	performActionOnLabeledStatement(LabeledStatement x)
void	performActionOnLocalVariableDeclaration(LocalVariableDeclaration x)
void	performActionOnMethodFrame(MethodFrame x)
void	performActionOnStatementBlock(StatementBlock x)
void	performActionOnSwitch(Switch x)
void	performActionOnSynchronizedBlock(SynchronizedBlock x)
void	performActionOnThen(Then x)
void	performActionOnTry(Try x)
void	performActionOnWhile(While x)
StatementBlock	replace() Does the replacement and returns the result.
void	start() Does the replacement.
java.lang.String	toString()
protected void	walk(ProgramElement node) walks through the AST.

Methods inherited from class de.uka.ilkd.key.java.visitor.JavaASTVisitor

doAction, 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, performActionOnSchemaVariable, 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

Methods inherited from class de.uka.ilkd.key.java.visitor.JavaASTWalker

depth, root

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

CHANGED

protected static final java.lang.Boolean CHANGED

breakOuter

private final Break breakOuter

The break statement used to replace break statements.

breakInner

private final Break breakInner

The break statement used to replace continue statements.

stack

private final java.util.Stack<ExtList> stack

loopLabels

private final java.util.Stack<Label> loopLabels

frames

private final java.util.Stack<MethodFrame> frames

loopAndSwitchCascadeDepth

private int loopAndSwitchCascadeDepth

result

private StatementBlock result

Constructor Detail

InnerBreakAndContinueReplacer

public InnerBreakAndContinueReplacer(StatementBlock block,
                                     java.lang.Iterable<Label> loopLabels,
                                     Label breakLabel,
                                     Label continueLabel,
                                     Services services)

Parameters:

block - a block that begins with a loop.

loopLabels - all labels belonging to the loop.

breakLabel - the label used for break statements.

continueLabel - the label used for continue statements.

services - services.

Method Detail

replace

public StatementBlock replace()

Does the replacement and returns the result.

Returns:

the block with all labels in the loop replaced.

See Also:

start()

start

public void start()

Does the replacement.

Overrides:

start in class JavaASTWalker

See Also:

replace()

getResult

public StatementBlock getResult()

walk

protected void walk(ProgramElement node)

Description copied from class: JavaASTWalker

walks through the AST. While keeping track of the current node

Overrides:

walk in class JavaASTVisitor

Parameters:

node - the JavaProgramElement the walker is at

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

doDefaultAction

protected void doDefaultAction(SourceElement x)

Description copied from class: JavaASTVisitor

the action that is performed just before leaving the node the last time

Specified by:

doDefaultAction in class JavaASTVisitor

Parameters:

x - the node described above

performActionOnContinue

public void performActionOnContinue(Continue x)

Specified by:

performActionOnContinue in interface Visitor

Overrides:

performActionOnContinue in class JavaASTVisitor

performActionOnBreak

public void performActionOnBreak(Break x)

Specified by:

performActionOnBreak in interface Visitor

Overrides:

performActionOnBreak in class JavaASTVisitor

performActionOnLocalVariableDeclaration

public void performActionOnLocalVariableDeclaration(LocalVariableDeclaration x)

Specified by:

performActionOnLocalVariableDeclaration in interface Visitor

Overrides:

performActionOnLocalVariableDeclaration in class JavaASTVisitor

performActionOnStatementBlock

public void performActionOnStatementBlock(StatementBlock x)

Specified by:

performActionOnStatementBlock in interface Visitor

Overrides:

performActionOnStatementBlock in class JavaASTVisitor

performActionOnWhile

public void performActionOnWhile(While x)

Specified by:

performActionOnWhile in interface Visitor

Overrides:

performActionOnWhile in class JavaASTVisitor

performActionOnFor

public void performActionOnFor(For x)

Specified by:

performActionOnFor in interface Visitor

Overrides:

performActionOnFor in class JavaASTVisitor

performActionOnEnhancedFor

public void performActionOnEnhancedFor(EnhancedFor x)

Specified by:

performActionOnEnhancedFor in interface Visitor

Overrides:

performActionOnEnhancedFor in class JavaASTVisitor

performActionOnDo

public void performActionOnDo(Do x)

Specified by:

performActionOnDo in interface Visitor

Overrides:

performActionOnDo in class JavaASTVisitor

performActionOnIf

public void performActionOnIf(If x)

Specified by:

performActionOnIf in interface Visitor

Overrides:

performActionOnIf in class JavaASTVisitor

performActionOnSwitch

public void performActionOnSwitch(Switch x)

Specified by:

performActionOnSwitch in interface Visitor

Overrides:

performActionOnSwitch in class JavaASTVisitor

performActionOnTry

public void performActionOnTry(Try x)

Specified by:

performActionOnTry in interface Visitor

Overrides:

performActionOnTry in class JavaASTVisitor

performActionOnLabeledStatement

public void performActionOnLabeledStatement(LabeledStatement x)

Specified by:

performActionOnLabeledStatement in interface Visitor

Overrides:

performActionOnLabeledStatement in class JavaASTVisitor

performActionOnMethodFrame

public void performActionOnMethodFrame(MethodFrame x)

Specified by:

performActionOnMethodFrame in interface Visitor

Overrides:

performActionOnMethodFrame in class JavaASTVisitor

performActionOnSynchronizedBlock

public void performActionOnSynchronizedBlock(SynchronizedBlock x)

Specified by:

performActionOnSynchronizedBlock in interface Visitor

Overrides:

performActionOnSynchronizedBlock in class JavaASTVisitor

performActionOnCopyAssignment

public void performActionOnCopyAssignment(CopyAssignment x)

Specified by:

performActionOnCopyAssignment in interface Visitor

Overrides:

performActionOnCopyAssignment in class JavaASTVisitor

performActionOnThen

public void performActionOnThen(Then x)

Specified by:

performActionOnThen in interface Visitor

Overrides:

performActionOnThen in class JavaASTVisitor

performActionOnElse

public void performActionOnElse(Else x)

Specified by:

performActionOnElse in interface Visitor

Overrides:

performActionOnElse in class JavaASTVisitor

performActionOnCase

public void performActionOnCase(Case x)

Specified by:

performActionOnCase in interface Visitor

Overrides:

performActionOnCase in class JavaASTVisitor

performActionOnCatch

public void performActionOnCatch(Catch x)

Specified by:

performActionOnCatch in interface Visitor

Overrides:

performActionOnCatch in class JavaASTVisitor

performActionOnDefault

public void performActionOnDefault(Default x)

Specified by:

performActionOnDefault in interface Visitor

Overrides:

performActionOnDefault in class JavaASTVisitor

performActionOnFinally

public void performActionOnFinally(Finally x)

Specified by:

performActionOnFinally in interface Visitor

Overrides:

performActionOnFinally in class JavaASTVisitor

changed

private void changed()

addChild

private void addChild(SourceElement x)