public class Recoder2KeY extends java.lang.Object implements JavaReader
readCompilationUnit(String)
,
#readCompilationUnitsAsFiles(String[])
or the
readBlock(String, Context)
-methods.
Results are often stored in caches.
It used to be monolithic but now uses separate classes for doing the actual
conversion and type conversion.Recoder2KeYConverter
,
Recoder2KeYTypeConverter
Constructor and Description |
---|
Recoder2KeY(Services services,
KeYCrossReferenceServiceConfiguration servConf,
KeYRecoderMapping rec2key,
NamespaceSet nss,
TypeConverter tc)
create a new Recoder2KeY transformation object.
|
Recoder2KeY(Services services,
NamespaceSet nss)
create a new Recoder2KeY transformation object.
|
Modifier and Type | Method and Description |
---|---|
protected de.uka.ilkd.key.java.Context |
createContext(ImmutableList<ProgramVariable> pvs)
create a new context with a temporary name and make a list of variables
visible from within.
|
protected de.uka.ilkd.key.java.Context |
createContext(ImmutableList<ProgramVariable> vars,
CrossReferenceSourceInfo csi)
create a new Context with a temporary name and make a list of variables
visible from within.
|
de.uka.ilkd.key.java.Context |
createEmptyContext()
creates an empty RECODER compilation unit with a temporary name.
|
protected MethodDeclaration |
embedBlock(StatementBlock block)
wraps a RECODER StatementBlock in a method
it is wrapped in a method called
<virtual_method_for_parsing> . |
protected ClassDeclaration |
embedMethod(MethodDeclaration mdecl,
de.uka.ilkd.key.java.Context context)
wraps a RECODER MethodDeclaration in a class
|
Recoder2KeYConverter |
getConverter()
return the associated converter object
|
java.util.List<java.lang.String> |
getDynamicallyCreatedClasses()
get the list of names of classes that have been created dynamically due
to lacking definitions.
|
KeYCrossReferenceServiceConfiguration |
getServiceConfiguration() |
Recoder2KeYTypeConverter |
getTypeConverter()
return the associated type converter object
|
boolean |
isParsingLibs()
are we currently parsing library code (special classes)?
|
protected Recoder2KeYConverter |
makeConverter(Services services,
NamespaceSet nss)
create the ast converter.
|
void |
parseSpecialClasses()
makes sure that the special classes (library classes) have been parsed
in.
|
void |
parseSpecialClasses(FileRepo fileRepo)
makes sure that the special classes (library classes) have been parsed
in.
|
JavaBlock |
readBlock(java.lang.String block,
de.uka.ilkd.key.java.Context context)
parses a given JavaBlock using the context to determine the right
references
|
JavaBlock |
readBlockWithEmptyContext(java.lang.String block)
parses a given JavaBlock using the context to determine the right
references using an empty context
|
JavaBlock |
readBlockWithProgramVariables(Namespace<IProgramVariable> varns,
java.lang.String s)
parses a given JavaBlock using a namespace to determine the right
references using an empty context.
|
CompilationUnit |
readCompilationUnit(java.lang.String cUnitString)
read a compilation unit, given as a string.
|
CompilationUnit[] |
readCompilationUnitsAsFiles(java.lang.String[] cUnitStrings,
FileRepo fileRepo)
parse a list of java files and transform it to the corresponding KeY
entities.
|
KeYRecoderMapping |
rec2key() |
static void |
reportError(java.lang.String message,
java.lang.Throwable t)
report an error in form of a ConvertException.
|
void |
setClassPath(java.io.File bootClassPath,
java.util.List<java.io.File> classPath) |
protected void |
transformModel(java.util.List<CompilationUnit> cUnits)
Transform a list of compilation units.
|
public Recoder2KeY(Services services, KeYCrossReferenceServiceConfiguration servConf, KeYRecoderMapping rec2key, NamespaceSet nss, TypeConverter tc)
servConf
- the service configuration to be used, not nullrec2key
- the mapping to store mapped types and mapped ASTs to, not nullnss
- the namespaces to work upon, not nulltc
- the type converter, not nullpublic Recoder2KeY(Services services, NamespaceSet nss)
services
- services to retrieve objects from, not nullnss
- the namespaces to work upon, not nullprotected Recoder2KeYConverter makeConverter(Services services, NamespaceSet nss)
services
- nss
- the namespaces provided to the constructorpublic Recoder2KeYConverter getConverter()
public Recoder2KeYTypeConverter getTypeConverter()
public boolean isParsingLibs()
public KeYCrossReferenceServiceConfiguration getServiceConfiguration()
public KeYRecoderMapping rec2key()
public CompilationUnit[] readCompilationUnitsAsFiles(java.lang.String[] cUnitStrings, FileRepo fileRepo) throws ParseExceptionInFile
cUnitStrings
- a list of strings, each element is interpreted as a file to be
read. not null.fileRepo
- the fileRepo which will store the filesParseExceptionInFile
- any exception occurring while treating the file is wrapped
into a parse exception that contains the filename.public CompilationUnit readCompilationUnit(java.lang.String cUnitString)
cUnitString
- a string represents a compilation unitpublic void setClassPath(java.io.File bootClassPath, java.util.List<java.io.File> classPath)
public java.util.List<java.lang.String> getDynamicallyCreatedClasses()
public void parseSpecialClasses()
public void parseSpecialClasses(FileRepo fileRepo)
fileRepo
- the fileRepo which will store the filesprotected void transformModel(java.util.List<CompilationUnit> cUnits)
cUnits
- a list of compilation units, not null.protected MethodDeclaration embedBlock(StatementBlock block)
<virtual_method_for_parsing>
.block
- the recoder.java.StatementBlock to wrapprotected ClassDeclaration embedMethod(MethodDeclaration mdecl, de.uka.ilkd.key.java.Context context)
mdecl
- the recoder.java.declaration.MethodDeclaration to wrapcontext
- the recoder.java.declaration.ClassDeclaration where the method
has to be embeddedpublic de.uka.ilkd.key.java.Context createEmptyContext()
protected de.uka.ilkd.key.java.Context createContext(ImmutableList<ProgramVariable> pvs)
pvs
- a list of variablesprotected de.uka.ilkd.key.java.Context createContext(ImmutableList<ProgramVariable> vars, CrossReferenceSourceInfo csi)
vars
- a list of variablescsi
- a special source infopublic JavaBlock readBlock(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
interprestedpublic JavaBlock readBlockWithEmptyContext(java.lang.String block)
readBlockWithEmptyContext
in interface JavaReader
block
- a String describing a java blockpublic JavaBlock readBlockWithProgramVariables(Namespace<IProgramVariable> varns, java.lang.String s)
readBlockWithProgramVariables
in interface JavaReader
s
- a String describing a java blockpublic static void reportError(java.lang.String message, java.lang.Throwable t)
message
- message to be used.t
- the cause of the exceptional caseConvertException
- alwaysCopyright © 2003-2019 The KeY-Project.