de.uka.ilkd.key.java

Class SchemaRecoder2KeY

java.lang.Object

de.uka.ilkd.key.java.Recoder2KeY

de.uka.ilkd.key.java.SchemaRecoder2KeY

All Implemented Interfaces:

JavaReader, SchemaJavaReader

public class SchemaRecoder2KeY
extends Recoder2KeY
implements SchemaJavaReader

Field Summary

Fields

Modifier and Type	Field and Description
private static java.util.HashMap<?,?>	recClass2schemakeyClassCons caches constructor access for reflection
private static java.util.HashMap<?,?>	schemaCt2meth caches access to methods for reflection
private static SchemaCrossReferenceServiceConfiguration	schemaServConf
protected Namespace<SchemaVariable>	svns the namespace containing the program schema variables allowed here

Constructor Summary

Constructors

Constructor and Description
SchemaRecoder2KeY(Services services, NamespaceSet nss)

Method Summary

Modifier and Type	Method and Description
Context	createEmptyContext() creates an empty RECODER compilation unit
protected CompilationUnit	embedClass(ClassDeclaration classDecl, Context context) wraps a RECODER ClassDeclaration in a compilation unit
protected java.util.HashMap<?,?>	getKeYClassConstructorCache() returns the hashmap of a concrete RecodeR class to the constructor of its corresponding KeY class.
protected java.util.HashMap<?,?>	getMethodCache()
protected Recoder2KeYConverter	makeConverter(Services services, NamespaceSet nss) create the ast converter.
void	parseSpecialClasses() there is no need to parse special classes in this case, so this is empty
protected StatementBlock	recoderBlock(java.lang.String block, Context context) parses a given JavaBlock using the context to determine the right references and returns a statement block of recoder.
void	setSVNamespace(Namespace<SchemaVariable> svns)

Methods inherited from class de.uka.ilkd.key.java.Recoder2KeY

createContext, createContext, embedBlock, embedMethod, getConverter, getDynamicallyCreatedClasses, getServiceConfiguration, getTypeConverter, isParsingLibs, readBlock, readBlockWithEmptyContext, readBlockWithProgramVariables, readCompilationUnit, readCompilationUnitsAsFiles, rec2key, reportError, setClassPath, transformModel

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.java.JavaReader

readBlockWithEmptyContext, readBlockWithProgramVariables

Field Detail

svns

protected Namespace<SchemaVariable> svns

the namespace containing the program schema variables allowed here

schemaCt2meth

private static final java.util.HashMap<?,?> schemaCt2meth

caches access to methods for reflection

recClass2schemakeyClassCons

private static final java.util.HashMap<?,?> recClass2schemakeyClassCons

caches constructor access for reflection

schemaServConf

private static SchemaCrossReferenceServiceConfiguration schemaServConf

Constructor Detail

SchemaRecoder2KeY

public SchemaRecoder2KeY(Services services,
                         NamespaceSet nss)

Method Detail

makeConverter

protected Recoder2KeYConverter makeConverter(Services services,
                                             NamespaceSet nss)

Description copied from class: Recoder2KeY

create the ast converter. This is overwritten in SchemaRecoder2KeY to use schema-aware converters.

Overrides:

makeConverter in class Recoder2KeY

nss - the namespaces provided to the constructor

Returns:

a newley created converter

getKeYClassConstructorCache

protected java.util.HashMap<?,?> getKeYClassConstructorCache()

returns the hashmap of a concrete RecodeR class to the constructor of its corresponding KeY class. Speeds up reflection. Attention must be overwritten by subclasses!

getMethodCache

protected java.util.HashMap<?,?> getMethodCache()

setSVNamespace

public void setSVNamespace(Namespace<SchemaVariable> svns)

Specified by:

setSVNamespace in interface SchemaJavaReader

createEmptyContext

public Context createEmptyContext()

creates an empty RECODER compilation unit

Overrides:

createEmptyContext in class Recoder2KeY

Returns:

the recoder.java.CompilationUnit

embedClass

protected CompilationUnit embedClass(ClassDeclaration classDecl,
                                     Context context)

wraps a RECODER ClassDeclaration in a compilation unit

Parameters:

classDecl - the recoder.java.ClassDeclaration to wrap

context - the Context containing the recoder.java.CompilationUnit where the class is wrapped

Returns:

the enclosing recoder.java.CompilationUnit

recoderBlock

protected StatementBlock recoderBlock(java.lang.String block,
                                      Context context)

parses a given JavaBlock using the context to determine the right references and returns a statement block of recoder.

Overrides:

recoderBlock in class Recoder2KeY

Parameters:

block - a String describing a java block

context - recoder.java.CompilationUnit in which the block has to be interpreted

Returns:

the parsed and resolved recoder statement block

parseSpecialClasses

public void parseSpecialClasses()

there is no need to parse special classes in this case, so this is empty

Overrides:

parseSpecialClasses in class Recoder2KeY

See Also:

Recoder2KeY.parseSpecialClasses()