public class SwitchToIf extends ProgramTransformer
Modifier and Type | Field and Description |
---|---|
static int |
labelCount |
private boolean |
noNewBreak |
Constructor and Description |
---|
SwitchToIf(SchemaVariable _switch)
creates a switch-to-if ProgramTransformer
|
Modifier and Type | Method and Description |
---|---|
private Switch |
changeBreaks(Switch sw,
Break b)
Replaces all breaks in
sw , whose target is sw, with
b |
private StatementBlock |
collectStatements(Switch s,
int count)
Collects the Statements in a switch statement from branch
count downward. |
private Statement[] |
mkIfNullCheck(Services services,
ProgramVariable var)
return a check of the kind
if(v == null) throw new NullPointerException(); |
private ProgramElement |
recChangeBreaks(ProgramElement p,
Break b) |
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 SwitchToIf(SchemaVariable _switch)
_switch
- the Statement contained by the meta constructpublic ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations insts)
ProgramTransformer
transform
in class ProgramTransformer
pe
- the ProgramElement on which the execution is performedservices
- the Services with all necessary information
about the java programsinsts
- the instantiations of the schemavariablesprivate Statement[] mkIfNullCheck(Services services, ProgramVariable var)
if(v == null) throw new NullPointerException();
private Switch changeBreaks(Switch sw, Break b)
sw
, whose target is sw, with
b
private ProgramElement recChangeBreaks(ProgramElement p, Break b)
private StatementBlock collectStatements(Switch s, int count)
count
downward.s
- the switch statement.count
- the branch where the collecting of statements starts.