de.uka.ilkd.key.java.recoderext

Class CreateObjectBuilder

java.lang.Object

recoder.kit.Transformation

recoder.kit.TwoPassTransformation

de.uka.ilkd.key.java.recoderext.RecoderModelTransformer

de.uka.ilkd.key.java.recoderext.CreateObjectBuilder

public class CreateObjectBuilder
extends RecoderModelTransformer

If an allocation expression 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$gt; which on its part calls another implicit method lt;prepare> for setting the fields default values.

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.java.recoderext.RecoderModelTransformer

RecoderModelTransformer.FinalOuterVarsCollector, RecoderModelTransformer.TransformerCache

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.HashMap<ClassDeclaration,Identifier>	class2identifier
static java.lang.String	IMPLICIT_OBJECT_CREATE
static java.lang.String	NEW_OBJECT_VAR_NAME

Fields inherited from class de.uka.ilkd.key.java.recoderext.RecoderModelTransformer

cache, services

Fields inherited from class recoder.kit.Transformation

EQUIVALENCE, IDENTITY, NO_PROBLEM

Constructor Summary

Constructors

Constructor and Description
CreateObjectBuilder(CrossReferenceServiceConfiguration services, RecoderModelTransformer.TransformerCache cache)

Method Summary

Modifier and Type	Method and Description
ProblemReport	analyze()
private StatementBlock	createBody(ClassDeclaration recoderClass) Creates the body of the static <createObject> method.
MethodDeclaration	createMethod(ClassDeclaration type) creates the implicit static <createObject> method that takes the object to be created out of the pool
protected void	makeExplicit(TypeDeclaration td) entry method for the constructor normalform builder
private TypeReference	makeTyRef(ClassDeclaration recoderClass)

Methods inherited from class de.uka.ilkd.key.java.recoderext.RecoderModelTransformer

assign, attach, attribute, classDeclarations, containingClass, containingMethod, declare, declare, getAllSupertypes, getDefaultValue, getId, getLocalClass2FinalVar, getUnits, isVisible, makeExplicit, transform

Methods inherited from class recoder.kit.TwoPassTransformation

execute

Methods inherited from class recoder.kit.Transformation

attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attach, attachAsArgument, attachAsArgument, attachAsArgument, attachAsArgument, attachAsArgument, attachAsArgument, attachAsArgument, attachAsArgument, attachAsBody, attachAsCondition, attachAsGuard, attachAsInitializer, attachAsLabel, attachAsMessage, attachAsPrefix, attachAsPrefix, attachAsPrefix, attachAsPrefix, attachAsUpdate, detach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttach, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsArgument, doAttachAsBody, doAttachAsCondition, doAttachAsGuard, doAttachAsInitializer, doAttachAsLabel, doAttachAsMessage, doAttachAsPrefix, doAttachAsPrefix, doAttachAsPrefix, doAttachAsPrefix, doAttachAsUpdate, doDetach, doReplace, getChangeHistory, getCrossReferenceSourceInfo, getNameInfo, getProblemReport, getProgramFactory, getServiceConfiguration, getSourceFileRepository, getSourceInfo, replace, rollback, setProblemReport, setServiceConfiguration, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

IMPLICIT_OBJECT_CREATE

public static final java.lang.String IMPLICIT_OBJECT_CREATE

See Also:

Constant Field Values

NEW_OBJECT_VAR_NAME

public static final java.lang.String NEW_OBJECT_VAR_NAME

See Also:

Constant Field Values

class2identifier

private java.util.HashMap<ClassDeclaration,Identifier> class2identifier

Constructor Detail

CreateObjectBuilder

public CreateObjectBuilder(CrossReferenceServiceConfiguration services,
                           RecoderModelTransformer.TransformerCache cache)

Method Detail

createBody

private StatementBlock createBody(ClassDeclaration recoderClass)

Creates the body of the static <createObject> method.

makeTyRef

private TypeReference makeTyRef(ClassDeclaration recoderClass)

createMethod

public MethodDeclaration createMethod(ClassDeclaration type)

creates the implicit static <createObject> method that takes the object to be created out of the pool

Parameters:

type - the TypeDeclaration for which the <prepare> is created

Returns:

the implicit <prepare> method

analyze

public ProblemReport analyze()

Overrides:

analyze in class TwoPassTransformation

makeExplicit

protected void makeExplicit(TypeDeclaration td)

entry method for the constructor normalform builder

Specified by:

makeExplicit in class RecoderModelTransformer

Parameters:

td - the TypeDeclaration