public class EnhancedForElimination extends ProgramTransformer
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
ARR
Name for the array variable.
|
private ExecutionContext |
execContext
Execution context.
|
private IExecutionContext |
execContextSV
Execution context sv.
|
private static java.lang.String |
HAS_NEXT_METHOD_NAME
hasNext method name. |
private StatementBlock |
head |
private static java.lang.String |
INDEX
Name for the
\index variable. |
private ProgramVariable |
indexVariable |
private static java.lang.String |
IT
Name for the iterator variable.
|
private static java.lang.String |
ITERATOR_METHOD_NAME
iterator method name. |
private ProgramVariable |
iteratorVariable |
private LoopStatement |
loop |
private static java.lang.String |
NEXT_METHOD_NAME
next method name. |
private static java.lang.String |
VALUES
Name for the
\values variable. |
private ProgramVariable |
valuesVariable |
Constructor and Description |
---|
EnhancedForElimination(ExecutionContext execContext,
EnhancedFor forStatement)
Creates a new enhaced for-loop elimination.
|
EnhancedForElimination(ProgramSV execContextSV,
EnhancedFor forStatement)
Creates a new enhaced for-loop elimination.
|
body, getChildAt, getChildCount, getDimensions, getExpressionAt, getExpressionCount, getKeYJavaType, getKeYJavaType, getKeYJavaType, getLastElement, getName, getPackageReference, getProgramElementName, getReferencePrefix, getStatementAt, getStatementCount, getTypeReferenceAt, getTypeReferenceCount, name, neededInstantiations, needs, prettyPrint, setReferencePrefix, toString, visit
compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren
getComments, hashCode, prettyPrintMain, reuseSignature
getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getComments, match
private static final java.lang.String IT
getIteratorVariable()
,
Constant Field Valuesprivate static final java.lang.String ARR
private static final java.lang.String INDEX
\index
variable.getIndexVariable()
,
Constant Field Valuesprivate static final java.lang.String VALUES
\values
variable.getValuesVariable()
,
Constant Field Valuesprivate static final java.lang.String ITERATOR_METHOD_NAME
iterator
method name.private static final java.lang.String HAS_NEXT_METHOD_NAME
hasNext
method name.private static final java.lang.String NEXT_METHOD_NAME
next
method name.private ProgramVariable indexVariable
getIndexVariable()
private ProgramVariable valuesVariable
getValuesVariable()
private ProgramVariable iteratorVariable
getIteratorVariable()
private StatementBlock head
getHead()
private LoopStatement loop
getLoop()
private IExecutionContext execContextSV
private ExecutionContext execContext
public EnhancedForElimination(ProgramSV execContextSV, EnhancedFor forStatement)
execContextSV
- the execution context.forStatement
- the enhanced for loop to eliminate.public EnhancedForElimination(ExecutionContext execContext, EnhancedFor forStatement)
execContext
- the execution context.forStatement
- the enhanced for loop to eliminate.public ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations svInst)
Loops over arrays are treated by a taclet without use of this class.
Loops over Iterable-objects are treated by this meta-construct.
The rules which use this meta construct must ensure that exp is of type Iterable.
transform
in class ProgramTransformer
pe
- the ProgramElement on which the execution is performedservices
- the Services with all necessary information
about the java programssvInst
- the instantiations of the schemavariables#makeIterableForLoop(LocalVariableDeclaration, Expression, Statement)
,
ProgramTransformer.transform(de.uka.ilkd.key.java.ProgramElement, Services,
SVInstantiations)
public ProgramVariable getIndexVariable()
\index
.public ProgramVariable getValuesVariable()
\values
.public ProgramVariable getIteratorVariable()
public StatementBlock getHead()
getLoop()
public LoopStatement getLoop()
getHead()
private boolean isArrayType(Expression expression, Services services)
expression
- the expression to checkservices
- the services for lookupsprivate ProgramElement makeArrayForLoop(EnhancedFor enhancedFor, Services services)
private ProgramElement makeIterableForLoop(EnhancedFor enhancedFor, Services services)
private StatementBlock makeBlock(ProgramVariable itVar, ProgramVariable valuesVar, LocalVariableDeclaration lvd, Statement body)
private Statement makeValuesUpdate(ProgramVariable valuesVar, LocalVariableDeclaration lvd)
private void setInvariant(EnhancedFor original, LoopStatement transformed, Services services)
original
enhanced loop to the
transformed
while or for loop.original
- original loop.transformed
- transformed loop.services
- services.