public class ConstructorCall extends ProgramTransformer
new Class(...)
. Thereby it replaces the allocation
expression by a method reference to an implict method called
<init>
that is mainly the constructor but in its
normalform.Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
CONSTRUCTOR_CALL |
private SchemaVariable |
newObjectSV |
private ProgramVariable |
newObjectVar |
private static java.lang.String |
NORMALFORM_IDENTIFIER
The normal form identifier.
|
Modifier | Constructor and Description |
---|---|
protected |
ConstructorCall(Name name,
SchemaVariable newObjectSV,
ProgramElement consRef) |
|
ConstructorCall(ProgramVariable pv,
New n)
Used to programmatically produce this statement.
|
|
ConstructorCall(SchemaVariable newObjectSV,
ProgramElement consRef)
creates the metaconstruct
|
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Statement> |
constructorCallSequence(New constructorReference,
KeYJavaType classType,
SVInstantiations svInst,
Services services)
returns a sequence of statements modelling the Java constructor call
semantics explicitly
|
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, 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
private static final java.lang.String CONSTRUCTOR_CALL
private static final java.lang.String NORMALFORM_IDENTIFIER
private final SchemaVariable newObjectSV
private final ProgramVariable newObjectVar
protected ConstructorCall(Name name, SchemaVariable newObjectSV, ProgramElement consRef)
name
- Constructor Name.newObjectSV
- The SchemaVariable
consRef
- The constructor reference.public ConstructorCall(SchemaVariable newObjectSV, ProgramElement consRef)
newObjectSV
- TODOconsRef
- TODOpublic ConstructorCall(ProgramVariable pv, New n)
public ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations svInst)
ProgramTransformer
transform
in class ProgramTransformer
pe
- the ProgramElement on which the execution is performedservices
- the Services with all necessary information
about the java programssvInst
- the instantiations of the schemavariablesprotected java.util.List<Statement> constructorCallSequence(New constructorReference, KeYJavaType classType, SVInstantiations svInst, Services services)