de.uka.ilkd.key.rule.metaconstruct

Class SwitchToIf

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.JavaNonTerminalProgramElement

de.uka.ilkd.key.rule.metaconstruct.ProgramTransformer

de.uka.ilkd.key.rule.metaconstruct.SwitchToIf

All Implemented Interfaces:

Expression, ExpressionContainer, ModelElement, NamedModelElement, NamedProgramElement, NonTerminalProgramElement, ProgramElement, Reference, MemberReference, NameReference, PackageReferenceContainer, ReferencePrefix, ReferenceSuffix, TypeReference, TypeReferenceContainer, TypeReferenceInfix, SourceElement, Statement, StatementContainer, SVSubstitute

public class SwitchToIf
extends ProgramTransformer

This class is used to perform program transformations needed for the symbolic execution of a switch-case statement.

Field Summary

Fields

Modifier and Type	Field and Description
static int	labelCount
private boolean	noNewBreak

Constructor Summary

Constructors

Constructor and Description
SwitchToIf(SchemaVariable _switch) creates a switch-to-if ProgramTransformer

Method Summary

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

Methods inherited from class de.uka.ilkd.key.rule.metaconstruct.ProgramTransformer

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

Methods inherited from class de.uka.ilkd.key.java.JavaNonTerminalProgramElement

compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren

Methods inherited from class de.uka.ilkd.key.java.JavaProgramElement

getComments, hashCode, prettyPrintMain, reuseSignature

Methods inherited from class de.uka.ilkd.key.java.JavaSourceElement

getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.java.ProgramElement

getComments, match

Field Detail

labelCount

public static int labelCount

noNewBreak

private boolean noNewBreak

Constructor Detail

SwitchToIf

public SwitchToIf(SchemaVariable _switch)

creates a switch-to-if ProgramTransformer

Parameters:

_switch - the Statement contained by the meta construct

Method Detail

transform

public ProgramElement[] transform(ProgramElement pe,
                                  Services services,
                                  SVInstantiations insts)

Description copied from class: ProgramTransformer

performs the program transformation needed for symbolic program transformation

Specified by:

transform in class ProgramTransformer

Parameters:

pe - the ProgramElement on which the execution is performed

services - the Services with all necessary information about the java programs

insts - the instantiations of the schemavariables

Returns:

the transformated program

mkIfNullCheck

private Statement[] mkIfNullCheck(Services services,
                                  ProgramVariable var)

return a check of the kind if(v == null) throw new NullPointerException();

Returns:

an if-statement that performs a null check, wrapped in a single-element array.

changeBreaks

private Switch changeBreaks(Switch sw,
                            Break b)

Replaces all breaks in sw, whose target is sw, with b

recChangeBreaks

private ProgramElement recChangeBreaks(ProgramElement p,
                                       Break b)

collectStatements

private StatementBlock collectStatements(Switch s,
                                         int count)

Collects the Statements in a switch statement from branch count downward.

Parameters:

s - the switch statement.

count - the branch where the collecting of statements starts.