public class ForToWhile extends ProgramTransformer
ForToWhileTransformation
to create a transformed
loop body which is then put into the corresponding context.
for (int i = 0; i < 100; i++) { if (i == 2) continue; if (i == 3) break; }is translated to
_label1: { int i = 0; while (i < 100) { _label0: { if (i == 2) break _label0; if (i == 3) break _label1; } i++; } }
ForToWhileTransformation
Modifier and Type | Field and Description |
---|---|
private SchemaVariable |
innerLabel
the inner label ('l2')
|
private SchemaVariable |
outerLabel
the outer label that is used to leave the while loop ('l1')
|
Constructor and Description |
---|
ForToWhile(SchemaVariable innerLabel,
SchemaVariable outerLabel,
Statement loop)
creates an loop to while - ProgramTransformer
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<SchemaVariable> |
neededInstantiations(SVInstantiations svInst)
return a list of the SV that are relevant to this UnwindLoop
|
ProgramElement[] |
transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic
program transformation
|
body, getChildAt, getChildCount, getDimensions, getExpressionAt, getExpressionCount, getKeYJavaType, getKeYJavaType, getKeYJavaType, getLastElement, getName, getPackageReference, getProgramElementName, getReferencePrefix, getStatementAt, getStatementCount, getTypeReferenceAt, getTypeReferenceCount, name, 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 final SchemaVariable outerLabel
private final SchemaVariable innerLabel
public ForToWhile(SchemaVariable innerLabel, SchemaVariable outerLabel, Statement loop)
loop
- the LoopStatement contained by the meta constructinnerLabel
- the label used to handle continueouterLabel
- the label used to handle break (only needed for
do-while-loops)public ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations svInst)
ProgramTransformer
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 schemavariablespublic ImmutableList<SchemaVariable> neededInstantiations(SVInstantiations svInst)
neededInstantiations
in class ProgramTransformer
svInst
- the instantiations so far - ignored