public class EnhancedForElimination extends ProgramTransformer
Modifier and Type | Field and Description |
---|---|
private static String |
ARR |
private static String |
HAS_NEXT |
private static String |
IT |
private static String |
ITERABLE_CLASS_NAME |
private static String |
ITERATOR |
private static String |
ITERATOR_METH |
private static String |
NEXT |
private static String |
VALUES |
Constructor and Description |
---|
EnhancedForElimination(EnhancedFor forStatement) |
Modifier and Type | Method and Description |
---|---|
private boolean |
isIterable(Expression expression,
Services services)
Checks if an expression is an
Iterable . |
private ProgramElement |
makeArrayForLoop(EnhancedFor enhancedFor,
Services services) |
private StatementBlock |
makeBlock(ProgramVariable itVar,
ProgramVariable valuesVar,
LocalVariableDeclaration lvd,
Statement body) |
private ProgramElement |
makeIterableForLoop(EnhancedFor enhancedFor,
Services services) |
private Statement |
makeValuesUpdate(ProgramVariable valuesVar,
LocalVariableDeclaration lvd) |
private void |
setInvariant(EnhancedFor original,
LoopStatement transformed,
Services services)
Transfer the invariant from
original enhanced loop to the
transformed while or for loop. |
ProgramElement |
transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
An enhanced for loop is executed by transforming it into a "normal" for
loop.
|
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, equals, equalsModRenaming, getArrayPos, hashCode, match, matchChildren
getComments, 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 String IT
private static final String ARR
private static final String VALUES
private static final String ITERABLE_CLASS_NAME
private static final String ITERATOR_METH
private static final String HAS_NEXT
private static final String NEXT
private static final String ITERATOR
public EnhancedForElimination(EnhancedFor forStatement)
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,
de.uka.ilkd.key.java.Services,
de.uka.ilkd.key.rule.inst.SVInstantiations)
private boolean isIterable(Expression expression, Services services)
Iterable
.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.services
-