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
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
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 - ignoredCopyright © 2003-2019 The KeY-Project.