public class DoBreak extends ProgramTransformer
l1:l2:{l3:{l4:{break l3;}} ...}
becomes
l1:l2:{...}
Constructor and Description |
---|
DoBreak(LabeledStatement labeledBreak)
creates a do-break ProgramTransformer
|
Modifier and Type | Method and Description |
---|---|
ProgramElement[] |
transform(ProgramElement pe,
Services services,
SVInstantiations insts)
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, neededInstantiations, 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 DoBreak(LabeledStatement labeledBreak)
labeledBreak
- the LabeledStatement contained by the meta constructpublic ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations insts)
transform
in class ProgramTransformer
services
- the Services with all necessary information about the java
programspe
- the ProgramElement on which the execution is performedinsts
- the instantiations of the schemavariablesCopyright © 2003-2019 The KeY-Project.