public class SchemaRecoder2KeY extends Recoder2KeY implements SchemaJavaReader
Modifier and Type | Field and Description |
---|---|
protected Namespace<SchemaVariable> |
svns
the namespace containing the program schema variables allowed here
|
Constructor and Description |
---|
SchemaRecoder2KeY(Services services,
NamespaceSet nss) |
Modifier and Type | Method and Description |
---|---|
de.uka.ilkd.key.java.Context |
createEmptyContext()
creates an empty RECODER compilation unit
|
protected CompilationUnit |
embedClass(ClassDeclaration classDecl,
de.uka.ilkd.key.java.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,
de.uka.ilkd.key.java.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) |
createContext, createContext, embedBlock, embedMethod, getConverter, getDynamicallyCreatedClasses, getServiceConfiguration, getTypeConverter, isParsingLibs, parseSpecialClasses, readBlock, readBlockWithEmptyContext, readBlockWithProgramVariables, readCompilationUnit, readCompilationUnitsAsFiles, rec2key, reportError, setClassPath, transformModel
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
readBlockWithEmptyContext, readBlockWithProgramVariables
protected Namespace<SchemaVariable> svns
public SchemaRecoder2KeY(Services services, NamespaceSet nss)
protected Recoder2KeYConverter makeConverter(Services services, NamespaceSet nss)
Recoder2KeY
makeConverter
in class Recoder2KeY
nss
- the namespaces provided to the constructorprotected java.util.HashMap<?,?> getKeYClassConstructorCache()
protected java.util.HashMap<?,?> getMethodCache()
public void setSVNamespace(Namespace<SchemaVariable> svns)
setSVNamespace
in interface SchemaJavaReader
public de.uka.ilkd.key.java.Context createEmptyContext()
createEmptyContext
in class Recoder2KeY
protected CompilationUnit embedClass(ClassDeclaration classDecl, de.uka.ilkd.key.java.Context context)
classDecl
- the recoder.java.ClassDeclaration to wrapcontext
- the Context containing the recoder.java.CompilationUnit where the class is wrappedprotected StatementBlock recoderBlock(java.lang.String block, de.uka.ilkd.key.java.Context context)
block
- a String describing a java blockcontext
- recoder.java.CompilationUnit in which the block has to be
interpretedpublic void parseSpecialClasses()
parseSpecialClasses
in class Recoder2KeY
Recoder2KeY.parseSpecialClasses()
Copyright © 2003-2019 The KeY-Project.