Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.proof.io.consistency | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
void |
Recoder2KeY.parseSpecialClasses(FileRepo fileRepo)
makes sure that the special classes (library classes) have been parsed
in.
|
CompilationUnit[] |
Recoder2KeY.readCompilationUnitsAsFiles(java.lang.String[] cUnitStrings,
FileRepo fileRepo)
parse a list of java files and transform it to the corresponding KeY
entities.
|
Modifier and Type | Method and Description |
---|---|
FileRepo |
InitConfig.getFileRepo() |
Modifier and Type | Method and Description |
---|---|
void |
InitConfig.setFileRepo(FileRepo fileRepo) |
void |
ProblemInitializer.setFileRepo(FileRepo fileRepo)
Sets the FileRepo responsible for consistency between source code and proof.
|
Constructor and Description |
---|
KeYUserProblemFile(java.lang.String name,
java.io.File file,
FileRepo fileRepo,
ProgressMonitor monitor,
Profile profile,
boolean compressed)
Instantiates a new user problem file.
|
Modifier and Type | Method and Description |
---|---|
protected FileRepo |
AbstractProblemLoader.createFileRepo()
Creates a new FileRepo (with or without consistency) based on the settings.
|
Modifier and Type | Method and Description |
---|---|
protected EnvInput |
AbstractProblemLoader.createEnvInput(FileRepo fileRepo)
Instantiates the
EnvInput which represents the file to load. |
protected ProblemInitializer |
AbstractProblemLoader.createProblemInitializer(FileRepo fileRepo)
Instantiates the
ProblemInitializer to use. |
Constructor and Description |
---|
KeYFile(java.lang.String name,
java.io.File file,
FileRepo fileRepo,
ProgressMonitor monitor,
Profile profile,
boolean compressed)
Creates a new representation for a given file by indicating a name and a
file representing the physical source of the .key file.
|
KeYFile(java.lang.String name,
RuleSource file,
ProgressMonitor monitor,
Profile profile,
FileRepo fileRepo)
creates a new representation for a given file by indicating a name
and a RuleSource representing the physical source of the .key file.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractFileRepo
Abstract repo implementation to perform tasks independent from the concrete way the files are
cached.
|
class |
DiskFileRepo
This class uses a temporary directory as a store for the proof-relevant files.
|
class |
MemoryFileRepo
This class uses the memory as a store for the proof-relevant files.
|
class |
SimpleFileRepo
This FileRepo is able to build a proof bundle but is not able to guarantee consistency
between the saved proof and the source code because it does not cache the source code.
|
class |
TrivialFileRepo
This FileRepo does not cache any files but writes to / reads from the original files on disk.
|
Modifier and Type | Method and Description |
---|---|
java.io.InputStream |
FileCollection.Walker.openCurrent(FileRepo repo)
Create a new InputStream for the current element of the iteration.
|
Copyright © 2003-2019 The KeY-Project.