This class is used to perform program transformations needed
for the symbolic execution of a loop. It unwinds the loop:
e.g.
while ( i<10 ) {
i++
}
becomes
l1: {
if (i<10) { i++}
else break l1;
l2: {
while ( i<10 ) {
i++
}
}}
becomes
symbolicExecution(ProgramElement pe, Services services, SVInstantiations svInst) performs the program transformation needed for symbolic
program transformation
Parameters: services - the Services with all necessary information about the java programs Parameters: svInst - the instantiations esp.
performs the program transformation needed for symbolic
program transformation
Parameters: services - the Services with all necessary information about the java programs Parameters: svInst - the instantiations esp. of the inner and outer label the transformated program
Methods inherited from de.uka.ilkd.key.rule.metaconstruct.ProgramMetaConstruct