public class UnwindLoop extends ProgramTransformer
while ( i<10 ) {
i++
}
becomes if (i<10) l1:{ l2:{ i++; } while (i<10) { i++; } }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 |
---|
UnwindLoop(SchemaVariable innerLabel,
SchemaVariable outerLabel,
LoopStatement loop)
creates an unwind-loop ProgramTransformer
|
Modifier and Type | Method and Description |
---|---|
SchemaVariable |
getInnerLabelSV()
Deprecated.
|
SchemaVariable |
getOuterLabelSV()
Deprecated.
|
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 UnwindLoop(SchemaVariable innerLabel, SchemaVariable outerLabel, LoopStatement loop)
loop
- the LoopStatement contained by the meta constructinnerLabel
- The inner label SVouterLabel
- The outer label SVpublic 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 schemavariables@Deprecated public SchemaVariable getInnerLabelSV()
@Deprecated public SchemaVariable getOuterLabelSV()
public ImmutableList<SchemaVariable> neededInstantiations(SVInstantiations svInst)
neededInstantiations
in class ProgramTransformer
svInst
- the instantiations so far - ignored