de.uka.ilkd.key.rule.metaconstruct

Class ConstructorCall

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.ConstructorCall

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 ConstructorCall
extends ProgramTransformer

The constructor call meta construct is used to handle a allocation expression like 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.

Field Summary

Fields

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.

Constructor Summary

Constructors

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

Method Summary

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

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

CONSTRUCTOR_CALL

private static final java.lang.String CONSTRUCTOR_CALL

See Also:

Constant Field Values

NORMALFORM_IDENTIFIER

private static final java.lang.String NORMALFORM_IDENTIFIER

The normal form identifier.

See Also:

Constant Field Values

newObjectSV

private final SchemaVariable newObjectSV

newObjectVar

private final ProgramVariable newObjectVar

Constructor Detail

ConstructorCall

protected ConstructorCall(Name name,
                          SchemaVariable newObjectSV,
                          ProgramElement consRef)

Parameters:

name - Constructor Name.

newObjectSV - The SchemaVariable

consRef - The constructor reference.

ConstructorCall

public ConstructorCall(SchemaVariable newObjectSV,
                       ProgramElement consRef)

creates the metaconstruct

Parameters:

newObjectSV - TODO

consRef - TODO

ConstructorCall

public ConstructorCall(ProgramVariable pv,
                       New n)

Used to programmatically produce this statement. There is no schema variable instantiation, since we have a concrete variable.

Method Detail

transform

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

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

svInst - the instantiations of the schemavariables

Returns:

the transformated program

constructorCallSequence

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