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 |
---|---|
private ProgramElement |
doBreak(NonTerminalProgramElement block,
Label breakLabel,
Break b)
a helper method to perform the symbolic execution of the doBreak
metaconstruct.
|
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 constructprivate ProgramElement doBreak(NonTerminalProgramElement block, Label breakLabel, Break b)
block
- the NonTerminalProgramElement to go through and look for the
labelbreakLabel
- the Label the break statement markedpublic 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 schemavariables