public class CreateObject extends ProgramTransformer
new Class(...) occurs, a new object
has to be created, in KeY this is quite similar to take it out of a list of
objects and setting the implicit flag <created> to
true as well as setting all fields of the object to their
default values. For the complete procedure, the method creates the implicit
method <createObject> which on its part calls another
implicit method lt;prepare> for setting the fields values.| Constructor and Description |
|---|
CreateObject(ProgramElement newExpr) |
| Modifier and Type | Method and Description |
|---|---|
ProgramElement[] |
transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
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, visitcompatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildrengetComments, hashCode, prettyPrintMain, reuseSignaturegetEndPosition, getFirstElement, getFirstElementIncludingBlocks, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toStringclone, finalize, getClass, notify, notifyAll, wait, wait, waitgetComments, matchpublic CreateObject(ProgramElement newExpr)
newExpr - The ProgramElementpublic ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations svInst)
ProgramTransformertransform in class ProgramTransformerpe - the ProgramElement on which the execution is performedservices - the Services with all necessary information
about the java programssvInst - the instantiations of the schemavariables