de.uka.ilkd.key.rule.metaconstruct

Class ReplaceWhileLoop

java.lang.Object

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

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

de.uka.ilkd.key.java.visitor.CreatingASTVisitor

de.uka.ilkd.key.rule.metaconstruct.ReplaceWhileLoop

All Implemented Interfaces:

Visitor

public class ReplaceWhileLoop
extends CreatingASTVisitor

This visitor is used to identify and replace the while loop in invariant rule. It can be applied to EnhancedFors also.

See Also:

WhileInvariantTransformer, WhileInvariantTransformation

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.java.visitor.CreatingASTVisitor

CreatingASTVisitor.DefaultAction

Field Summary

Fields

Modifier and Type	Field and Description
private int	currentMethodFrame
private int	firstLoopPos
private boolean	firstWhileFound
protected SVInstantiations	instantiations if run in check mode there are normally schemavaribles, so we need the instantiations of them
private int	lastMethodFrameBeforeLoop
private boolean	replaced
protected ProgramElement	result the result of the transformation
private KeYJavaType	returnType
private LoopStatement	theLoop
private StatementBlock	toInsert

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

CHANGED, stack

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

services

Constructor Summary

Constructors

Constructor and Description
ReplaceWhileLoop(ProgramElement root, StatementBlock toInsert, Services services) creates the WhileLoopTransformation for the transformation mode
ReplaceWhileLoop(ProgramElement root, SVInstantiations inst, StatementBlock toInsert, Services services) creates the WhileLoopTransformation for the check mode

Method Summary

Modifier and Type	Method and Description
Statement	getTheLoop()
void	performActionOnEnhancedFor(EnhancedFor x)
void	performActionOnMethodFrame(MethodFrame x)
void	performActionOnWhile(While x)
ProgramElement	result()
KeYJavaType	returnType()
void	start() starts the walker
java.lang.String	toString()
protected void	walk(ProgramElement node) walks through the AST.

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

addChild, addChildren, addToTopOfStack, changed, doDefaultAction, getPosition, performActionOnAllFields, performActionOnArrayInitializer, performActionOnArrayLengthReference, performActionOnArrayReference, performActionOnAssert, performActionOnBinaryAnd, performActionOnBinaryAndAssignment, performActionOnBinaryNot, performActionOnBinaryOr, performActionOnBinaryOrAssignment, performActionOnBinaryXOr, performActionOnBinaryXOrAssignment, performActionOnBreak, performActionOnCase, performActionOnCatch, performActionOnClassInitializer, performActionOnConditional, performActionOnContinue, performActionOnCopyAssignment, performActionOnDefault, performActionOnDivide, performActionOnDivideAssignment, performActionOnDLEmbeddedExpression, performActionOnDo, performActionOnElse, performActionOnEmptyStatement, performActionOnEquals, performActionOnExecutionContext, performActionOnFieldReference, performActionOnFinally, performActionOnFor, performActionOnForUpdates, performActionOnGreaterOrEquals, performActionOnGreaterThan, performActionOnGuard, performActionOnIf, performActionOnInstanceof, performActionOnIntersect, performActionOnLabeledStatement, performActionOnLessOrEquals, performActionOnLessThan, performActionOnLocalVariableDeclaration, performActionOnLogicalAnd, performActionOnLogicalNot, performActionOnLogicalOr, performActionOnLoopInit, performActionOnLoopInvariant, performActionOnLoopScopeBlock, performActionOnMergeContract, performActionOnMergePointStatement, performActionOnMetaClassReference, performActionOnMethodBodyStatement, performActionOnMethodReference, performActionOnMinus, performActionOnMinusAssignment, performActionOnModulo, performActionOnModuloAssignment, performActionOnNegative, performActionOnNew, performActionOnNewArray, performActionOnNotEquals, performActionOnPackageReference, performActionOnPackageSpecification, performActionOnParameterDeclaration, performActionOnParenthesizedExpression, performActionOnPassiveExpression, performActionOnPlus, performActionOnPlusAssignment, performActionOnPositive, performActionOnPostDecrement, performActionOnPostIncrement, performActionOnPreDecrement, performActionOnPreIncrement, performActionOnReturn, performActionOnSchematicFieldReference, performActionOnSeqConcat, performActionOnSeqLength, performActionOnSeqReverse, performActionOnSeqSingleton, performActionOnSeqSub, performActionOnSetMinus, performActionOnSetUnion, performActionOnShiftLeft, performActionOnShiftLeftAssignment, performActionOnShiftRight, performActionOnShiftRightAssignment, performActionOnSingleton, performActionOnStatementBlock, performActionOnSuperConstructorReference, performActionOnSuperReference, performActionOnSwitch, performActionOnSynchronizedBlock, performActionOnThen, performActionOnThisConstructorReference, performActionOnThisReference, performActionOnThrow, performActionOnTimes, performActionOnTimesAssignment, performActionOnTry, performActionOnTypeCast, performActionOnTypeReference, performActionOnUnsignedShiftRight, performActionOnUnsignedShiftRightAssignment, performActionOnVariableSpecification, preservesPositionInfo

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

doAction, performActionOnAbstractProgramElement, performActionOnAllObjects, performActionOnArrayDeclaration, performActionOnBlockContract, performActionOnBlockContract, performActionOnBooleanLiteral, performActionOnCatchAllStatement, performActionOnCharLiteral, performActionOnClassDeclaration, performActionOnComment, performActionOnCompilationUnit, performActionOnConstructorDeclaration, performActionOnContextStatementBlock, performActionOnDoubleLiteral, performActionOnEmptyMapLiteral, performActionOnEmptySeqLiteral, performActionOnEmptySetLiteral, performActionOnExactInstanceof, performActionOnExtends, performActionOnFieldDeclaration, performActionOnFieldSpecification, performActionOnFloatLiteral, performActionOnImplements, performActionOnImplicitFieldSpecification, performActionOnImport, performActionOnInterfaceDeclaration, performActionOnIntLiteral, performActionOnIProgramVariable, performActionOnLocationVariable, performActionOnLongLiteral, performActionOnLoopContract, performActionOnLoopContract, performActionOnLoopContract, performActionOnLoopInvariant, performActionOnMergeContract, performActionOnMethod, performActionOnMethodDeclaration, performActionOnModifier, performActionOnNullLiteral, performActionOnProgramConstant, performActionOnProgramElementName, performActionOnProgramMetaConstruct, performActionOnProgramMethod, performActionOnProgramVariable, performActionOnSchemaVariable, performActionOnSeqGet, performActionOnSeqIndexOf, performActionOnStringLiteral, performActionOnSuperArrayDeclaration, performActionOnThrows, performActionOnTransactionStatement, performActionOnVariableDeclaration, performActionOnVariableReference

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

firstWhileFound

private boolean firstWhileFound

replaced

private boolean replaced

toInsert

private StatementBlock toInsert

theLoop

private LoopStatement theLoop

lastMethodFrameBeforeLoop

private int lastMethodFrameBeforeLoop

returnType

private KeYJavaType returnType

currentMethodFrame

private int currentMethodFrame

firstLoopPos

private int firstLoopPos

instantiations

protected SVInstantiations instantiations

if run in check mode there are normally schemavaribles, so we need the instantiations of them

result

protected ProgramElement result

the result of the transformation

Constructor Detail

ReplaceWhileLoop

public ReplaceWhileLoop(ProgramElement root,
                        StatementBlock toInsert,
                        Services services)

creates the WhileLoopTransformation for the transformation mode

Parameters:

root - the ProgramElement where to begin

ReplaceWhileLoop

public ReplaceWhileLoop(ProgramElement root,
                        SVInstantiations inst,
                        StatementBlock toInsert,
                        Services services)

creates the WhileLoopTransformation for the check mode

Parameters:

root - the ProgramElement where to begin

inst - the SVInstantiations if available

Method Detail

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 CreatingASTVisitor

Parameters:

node - the JavaProgramElement the walker is at

start

public void start()

Description copied from class: JavaASTWalker

starts the walker

Overrides:

start in class JavaASTWalker

result

public ProgramElement result()

returnType

public KeYJavaType returnType()

getTheLoop

public Statement getTheLoop()

toString

public java.lang.String toString()

Overrides:

toString in class CreatingASTVisitor

performActionOnMethodFrame

public void performActionOnMethodFrame(MethodFrame x)

Specified by:

performActionOnMethodFrame in interface Visitor

Overrides:

performActionOnMethodFrame in class CreatingASTVisitor

performActionOnWhile

public void performActionOnWhile(While x)

Specified by:

performActionOnWhile in interface Visitor

Overrides:

performActionOnWhile in class CreatingASTVisitor

performActionOnEnhancedFor

public void performActionOnEnhancedFor(EnhancedFor x)

Specified by:

performActionOnEnhancedFor in interface Visitor

Overrides:

performActionOnEnhancedFor in class CreatingASTVisitor