de.uka.ilkd.key.java.visitor

Class ProgVarReplaceVisitor

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.java.visitor.ProgVarReplaceVisitor

All Implemented Interfaces:

Visitor

public class ProgVarReplaceVisitor
extends CreatingASTVisitor

Walks through a java AST in depth-left-first-order. This visitor replaces a number of program variables by others or new ones.

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
protected boolean	replaceallbynew
protected java.util.Map<ProgramVariable,ProgramVariable>	replaceMap stores the program variables to be replaced as keys and the new program variables as values
private ProgramElement	result

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

CHANGED, preservesPositionInfo, stack

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

services

Constructor Summary

Constructors

Constructor and Description
ProgVarReplaceVisitor(ProgramElement st, java.util.Map<ProgramVariable,ProgramVariable> map, boolean replaceall, Services services) creates a visitor that replaces the program variables in the given statement
ProgVarReplaceVisitor(ProgramElement st, java.util.Map<ProgramVariable,ProgramVariable> map, Services services) creates a visitor that replaces the program variables in the given statement by new ones with the same name

Method Summary

Modifier and Type	Method and Description
static LocationVariable	copy(ProgramVariable pv)
static LocationVariable	copy(ProgramVariable pv, java.lang.String postFix)
private BlockContract	createNewBlockContract(BlockContract oldContract, StatementBlock newBlock, boolean blockChanged)
private LoopContract	createNewLoopContract(LoopContract oldContract, JavaStatement newStatement, boolean blockChanged)
private MergeContract	createNewMergeContract(MergeContract oldContract, MergePointStatement newMps, boolean changed)
protected void	doAction(ProgramElement node) the action that is performed just before leaving the node the last time
void	performActionOnBlockContract(StatementBlock oldBlock, StatementBlock newBlock) Adds block contract for new statement block to block contract of old block statement.
void	performActionOnLocationVariable(LocationVariable x)
void	performActionOnLoopContract(LoopStatement oldLoop, LoopStatement newLoop) Adds loop contract for new loop statement to loop contract of old loop statement.
void	performActionOnLoopContract(StatementBlock oldBlock, StatementBlock newBlock) Adds block contract for new statement block to block contract of old block statement.
void	performActionOnLoopInvariant(LoopStatement oldLoop, LoopStatement newLoop)
void	performActionOnMergeContract(MergeContract oldContract)
protected void	performActionOnMergeContract(MergePointStatement oldMps, MergePointStatement newMps)
void	performActionOnProgramConstant(ProgramConstant x)
void	performActionOnProgramVariable(ProgramVariable pv)
private AuxiliaryContract.Variables	replaceBlockContractVariables(AuxiliaryContract.Variables variables)
private java.util.Map<Label,ProgramVariable>	replaceFlags(java.util.Map<Label,ProgramVariable> flags)
private java.util.Map<LocationVariable,LocationVariable>	replaceRemembranceHeaps(java.util.Map<LocationVariable,LocationVariable> remembranceHeaps)
private java.util.Map<LocationVariable,LocationVariable>	replaceRemembranceLocalVariables(java.util.Map<LocationVariable,LocationVariable> remembranceLocalVariables)
private ProgramVariable	replaceVariable(ProgramVariable variable)
private Term	replaceVariablesInTerm(Term t)
private ImmutableList<InfFlowSpec>	replaceVariablesInTermListTriples(ImmutableList<InfFlowSpec> terms)
private ImmutableList<Term>	replaceVariablesInTerms(ImmutableList<Term> terms)
ProgramElement	result()
void	start() starts the walker
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, performActionOnEnhancedFor, performActionOnEquals, performActionOnExecutionContext, performActionOnFieldReference, performActionOnFinally, performActionOnFor, performActionOnForUpdates, performActionOnGreaterOrEquals, performActionOnGreaterThan, performActionOnGuard, performActionOnIf, performActionOnInstanceof, performActionOnIntersect, performActionOnLabeledStatement, performActionOnLessOrEquals, performActionOnLessThan, performActionOnLocalVariableDeclaration, performActionOnLogicalAnd, performActionOnLogicalNot, performActionOnLogicalOr, performActionOnLoopInit, performActionOnLoopScopeBlock, performActionOnMergePointStatement, performActionOnMetaClassReference, performActionOnMethodBodyStatement, performActionOnMethodFrame, 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, performActionOnWhile, preservesPositionInfo, toString

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

performActionOnAbstractProgramElement, performActionOnAllObjects, performActionOnArrayDeclaration, performActionOnBlockContract, performActionOnBooleanLiteral, performActionOnCatchAllStatement, performActionOnCharLiteral, performActionOnClassDeclaration, performActionOnComment, performActionOnCompilationUnit, performActionOnConstructorDeclaration, performActionOnContextStatementBlock, performActionOnDoubleLiteral, performActionOnEmptyMapLiteral, performActionOnEmptySeqLiteral, performActionOnEmptySetLiteral, performActionOnExactInstanceof, performActionOnExtends, performActionOnFieldDeclaration, performActionOnFieldSpecification, performActionOnFloatLiteral, performActionOnImplements, performActionOnImplicitFieldSpecification, performActionOnImport, performActionOnInterfaceDeclaration, performActionOnIntLiteral, performActionOnIProgramVariable, performActionOnLongLiteral, performActionOnLoopContract, performActionOnLoopInvariant, performActionOnMethod, performActionOnMethodDeclaration, performActionOnModifier, performActionOnNullLiteral, performActionOnProgramElementName, performActionOnProgramMetaConstruct, performActionOnProgramMethod, 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

replaceallbynew

protected boolean replaceallbynew

replaceMap

protected java.util.Map<ProgramVariable,ProgramVariable> replaceMap

stores the program variables to be replaced as keys and the new program variables as values

result

private ProgramElement result

Constructor Detail

ProgVarReplaceVisitor

public ProgVarReplaceVisitor(ProgramElement st,
                             java.util.Map<ProgramVariable,ProgramVariable> map,
                             Services services)

creates a visitor that replaces the program variables in the given statement by new ones with the same name

Parameters:

st - the statement where the prog vars are replaced

map - the HashMap with the replacements

services - the services instance

ProgVarReplaceVisitor

public ProgVarReplaceVisitor(ProgramElement st,
                             java.util.Map<ProgramVariable,ProgramVariable> map,
                             boolean replaceall,
                             Services services)

creates a visitor that replaces the program variables in the given statement

Parameters:

st - the statement where the prog vars are replaced

map - the HashMap with the replacements

replaceall - decides if all variables are to be replaced

services - the services instance

Method Detail

copy

public static LocationVariable copy(ProgramVariable pv)

copy

public static LocationVariable copy(ProgramVariable pv,
                                    java.lang.String postFix)

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

doAction

protected void doAction(ProgramElement node)

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

Overrides:

doAction in class JavaASTVisitor

Parameters:

node - the node described above

start

public void start()

starts the walker

Overrides:

start in class JavaASTWalker

result

public ProgramElement result()

performActionOnProgramVariable

public void performActionOnProgramVariable(ProgramVariable pv)

Specified by:

performActionOnProgramVariable in interface Visitor

Overrides:

performActionOnProgramVariable in class JavaASTVisitor

replaceVariablesInTerm

private Term replaceVariablesInTerm(Term t)

replaceVariablesInTerms

private ImmutableList<Term> replaceVariablesInTerms(ImmutableList<Term> terms)

replaceVariablesInTermListTriples

private ImmutableList<InfFlowSpec> replaceVariablesInTermListTriples(ImmutableList<InfFlowSpec> terms)

performActionOnLocationVariable

public void performActionOnLocationVariable(LocationVariable x)

Specified by:

performActionOnLocationVariable in interface Visitor

Overrides:

performActionOnLocationVariable in class JavaASTVisitor

performActionOnProgramConstant

public void performActionOnProgramConstant(ProgramConstant x)

Specified by:

performActionOnProgramConstant in interface Visitor

Overrides:

performActionOnProgramConstant in class JavaASTVisitor

performActionOnBlockContract

public void performActionOnBlockContract(StatementBlock oldBlock,
                                         StatementBlock newBlock)

Description copied from interface: Visitor

Adds block contract for new statement block to block contract of old block statement.

Specified by:

performActionOnBlockContract in interface Visitor

Overrides:

performActionOnBlockContract in class JavaASTVisitor

Parameters:

oldBlock - the old block

newBlock - the new block

performActionOnLoopContract

public void performActionOnLoopContract(StatementBlock oldBlock,
                                        StatementBlock newBlock)

Description copied from interface: Visitor

Adds block contract for new statement block to block contract of old block statement.

Specified by:

performActionOnLoopContract in interface Visitor

Overrides:

performActionOnLoopContract in class JavaASTVisitor

Parameters:

oldBlock - the old block

newBlock - the new block

performActionOnLoopContract

public void performActionOnLoopContract(LoopStatement oldLoop,
                                        LoopStatement newLoop)

Description copied from interface: Visitor

Adds loop contract for new loop statement to loop contract of old loop statement.

Specified by:

performActionOnLoopContract in interface Visitor

Overrides:

performActionOnLoopContract in class JavaASTVisitor

Parameters:

oldLoop - the old loop statement

newLoop - the new loop statement

performActionOnMergeContract

public void performActionOnMergeContract(MergeContract oldContract)

Specified by:

performActionOnMergeContract in interface Visitor

Overrides:

performActionOnMergeContract in class JavaASTVisitor

performActionOnMergeContract

protected void performActionOnMergeContract(MergePointStatement oldMps,
                                            MergePointStatement newMps)

Overrides:

performActionOnMergeContract in class CreatingASTVisitor

createNewMergeContract

private MergeContract createNewMergeContract(MergeContract oldContract,
                                             MergePointStatement newMps,
                                             boolean changed)

createNewBlockContract

private BlockContract createNewBlockContract(BlockContract oldContract,
                                             StatementBlock newBlock,
                                             boolean blockChanged)

createNewLoopContract

private LoopContract createNewLoopContract(LoopContract oldContract,
                                           JavaStatement newStatement,
                                           boolean blockChanged)

replaceBlockContractVariables

private AuxiliaryContract.Variables replaceBlockContractVariables(AuxiliaryContract.Variables variables)

replaceVariable

private ProgramVariable replaceVariable(ProgramVariable variable)

replaceFlags

private java.util.Map<Label,ProgramVariable> replaceFlags(java.util.Map<Label,ProgramVariable> flags)

replaceRemembranceHeaps

private java.util.Map<LocationVariable,LocationVariable> replaceRemembranceHeaps(java.util.Map<LocationVariable,LocationVariable> remembranceHeaps)

replaceRemembranceLocalVariables

private java.util.Map<LocationVariable,LocationVariable> replaceRemembranceLocalVariables(java.util.Map<LocationVariable,LocationVariable> remembranceLocalVariables)

performActionOnLoopInvariant

public void performActionOnLoopInvariant(LoopStatement oldLoop,
                                         LoopStatement newLoop)

Overrides:

performActionOnLoopInvariant in class CreatingASTVisitor