de.uka.ilkd.key.java.recoderext

Class KeYCrossReferenceNameInfo

java.lang.Object

recoder.AbstractService

recoder.service.DefaultNameInfo

de.uka.ilkd.key.java.recoderext.KeYCrossReferenceNameInfo

All Implemented Interfaces:

java.beans.PropertyChangeListener, java.util.EventListener, Service, NameInfo

public class KeYCrossReferenceNameInfo
extends DefaultNameInfo

This is a specialisation of the NameInfo interface which allows KeY to detect multiple declaration of types. It stores all defined type (w/o possible some array types which do not matter) in a hash table to look up. If it records an attempt to register a declaration type twice, a verbose conversion exception is thrown. It also reports a missing "java.lang.Object" definition in a ConvertException. Recoder itself usually fails at a random point with a NullPointerException. An instance of this class is created in KeYCrossReferenceServiceConfiguration.

Author:

MU

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.HashMap<java.lang.String,ClassType>	classtypes

Fields inherited from class recoder.AbstractService

serviceConfiguration

Constructor Summary

Constructors

Constructor and Description
KeYCrossReferenceNameInfo(ServiceConfiguration config)

Method Summary

Modifier and Type	Method and Description
ClassType	getJavaLangObject() This implementation checks whether an implementation is available and fails if not.
Type	getType(java.lang.String name)
void	register(ClassType ct) register a class type.
void	unregisterClassType(java.lang.String fullname) unregister a class type.

Methods inherited from class recoder.service.DefaultNameInfo

createArrayType, createArrayType, createPackage, getArrayType, getBooleanType, getByteType, getCharType, getClassType, getClassTypes, getDoubleType, getField, getFields, getFloatType, getIntType, getJavaIoSerializable, getJavaLangAnnotationAnnotation, getJavaLangBoolean, getJavaLangByte, getJavaLangCharacter, getJavaLangClass, getJavaLangCloneable, getJavaLangDouble, getJavaLangEnum, getJavaLangFloat, getJavaLangInteger, getJavaLangLong, getJavaLangRunnable, getJavaLangShort, getJavaLangString, getLongType, getNullType, getPackage, getPackages, getShortType, getTypes, getTypes, getUnknownAnnotationProperty, getUnknownClassType, getUnknownConstructor, getUnknownElement, getUnknownField, getUnknownMethod, getUnknownPackage, getUnknownType, getUnknownVariable, information, initialize, isPackage, propertyChange, register, unregisterField, unregisterPackages

Methods inherited from class recoder.AbstractService

getServiceConfiguration

Methods inherited from class java.lang.Object

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

Methods inherited from interface recoder.Service

getServiceConfiguration

Field Detail

classtypes

private java.util.HashMap<java.lang.String,ClassType> classtypes

Constructor Detail

KeYCrossReferenceNameInfo

public KeYCrossReferenceNameInfo(ServiceConfiguration config)

Method Detail

register

public void register(ClassType ct)

register a class type.

Specified by:

register in interface NameInfo

Overrides:

register in class DefaultNameInfo

Parameters:

ct - class type to register

Throws:

ConvertException - if there was already a different type registered for the same name

unregisterClassType

public void unregisterClassType(java.lang.String fullname)

unregister a class type. This happens for instance when removing an EnumDeclaration and inserting an EnumClassDeclaration instead

Specified by:

unregisterClassType in interface NameInfo

Overrides:

unregisterClassType in class DefaultNameInfo

Parameters:

fullname - name of the type to be unregistered

getType

public Type getType(java.lang.String name)

Specified by:

getType in interface NameInfo

Overrides:

getType in class DefaultNameInfo

getJavaLangObject

public ClassType getJavaLangObject()
                            throws ConvertException

This implementation checks whether an implementation is available and fails if not.

Specified by:

getJavaLangObject in interface NameInfo

Overrides:

getJavaLangObject in class DefaultNameInfo

Throws:

ConvertException - if no implementation of java.lang.Object is available presently.