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, 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 final SchemaVariable outerLabel
private final SchemaVariable innerLabel
public UnwindLoop(SchemaVariable innerLabel, SchemaVariable outerLabel, LoopStatement loop)
loop
- the LoopStatement contained by the meta constructpublic ProgramElement transform(ProgramElement pe, Services services, SVInstantiations svInst)
transform
in class ProgramTransformer
services
- the Services with all necessary information
about the java programssvInst
- the instantiations esp. of the inner and outer labelpe
- the ProgramElement on which the execution is performedpublic SchemaVariable getInnerLabelSV()
public SchemaVariable getOuterLabelSV()
public ImmutableList<SchemaVariable> neededInstantiations(SVInstantiations svInst)
neededInstantiations
in class ProgramTransformer
svInst
- the instantiations so far - ignored