public abstract class AbstractProblemLoader
extends java.lang.Object
This class provides the basic functionality to load something in KeY.
The loading process is done in the current Thread
and
no user interaction is required.
The basic usage of this class is to instantiate a new
SingleThreadProblemLoader
or ProblemLoader
instance which should load the file configured by the constructor's arguments.
The next step is to call load()
which does the loading process and
tries to instantiate a proof and to apply rules again if possible. The result
of the loading process is available via the getter methods.
Modifier and Type | Class and Description |
---|---|
static class |
AbstractProblemLoader.ReplayResult |
Constructor and Description |
---|
AbstractProblemLoader(java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
Profile profileOfNewProofs,
boolean forceNewProfileOfNewProofs,
ProblemLoaderControl control,
boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile,
java.util.Properties poPropertiesToForce)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected EnvInput |
createEnvInput(FileRepo fileRepo)
Instantiates the
EnvInput which represents the file to load. |
protected FileRepo |
createFileRepo()
Creates a new FileRepo (with or without consistency) based on the settings.
|
protected InitConfig |
createInitConfig()
Creates the
InitConfig . |
protected ProblemInitializer |
createProblemInitializer(FileRepo fileRepo)
Instantiates the
ProblemInitializer to use. |
protected ProofAggregate |
createProof(IPersistablePO.LoadedPOContainer poContainer)
Creates a
Proof for the given IPersistablePO.LoadedPOContainer and
tries to apply rules again. |
protected IPersistablePO.LoadedPOContainer |
createProofObligationContainer()
Creates a
IPersistablePO.LoadedPOContainer if available which contains
the ProofOblInput for which a Proof should be instantiated. |
java.io.File |
getBootClassPath()
Returns the optional boot class path.
|
java.util.List<java.io.File> |
getClassPath()
Returns the optional class path entries to use.
|
EnvInput |
getEnvInput()
Returns the instantiated
EnvInput which describes the file to load. |
java.io.File |
getFile()
Returns the file or folder to load.
|
InitConfig |
getInitConfig()
Returns the instantiated
InitConfig which provides access to the loaded source elements and specifications. |
ProblemInitializer |
getProblemInitializer()
Returns the instantiated
ProblemInitializer used during the loading process. |
Proof |
getProof()
Returns the instantiate proof or
null if no proof was instantiated during loading process. |
Pair<java.lang.String,Location> |
getProofScript() |
AbstractProblemLoader.ReplayResult |
getResult()
Returns the
AbstractProblemLoader.ReplayResult if available. |
boolean |
hasProofScript()
Run proof script if it is present in the input data.
|
boolean |
isLoadSingleJavaFile() |
void |
load()
Executes the loading process and tries to instantiate a proof
and to re-apply rules on it if possible.
|
protected void |
loadEnvironment()
Loads and initialized the proof environment.
|
protected void |
loadSelectedProof(IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList)
Loads a proof from the proof list.
|
Pair<java.lang.String,Location> |
readProofScript() |
protected ProblemLoaderException |
recoverParserErrorMessage(java.lang.Exception e)
Tries to recover parser errors and make them human-readable,
rewrap them into ProblemLoaderExceptions.
|
protected void |
selectAndLoadProof(ProblemLoaderControl control,
InitConfig initConfig)
Asks the user to select a proof obligation and loads it.
|
void |
setLoadSingleJavaFile(boolean loadSingleJavaFile) |
protected void |
setProof(Proof proof) |
void |
setProofPath(java.io.File proofFilename) |
public AbstractProblemLoader(java.io.File file, java.util.List<java.io.File> classPath, java.io.File bootClassPath, java.util.List<java.io.File> includes, Profile profileOfNewProofs, boolean forceNewProfileOfNewProofs, ProblemLoaderControl control, boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile, java.util.Properties poPropertiesToForce)
file
- The file or folder to load.classPath
- The optional class path entries to use.bootClassPath
- An optional boot class path.includes
- Optional includes to consider.profileOfNewProofs
- The Profile
to use for new Proof
s.forceNewProfileOfNewProofs
- true profileOfNewProofs
will be used as Profile
of new proofs, false
Profile
specified by problem file will be used for new proofs.control
- The ProblemLoaderControl
to use.askUiToSelectAProofObligationIfNotDefinedByLoadedFile
- true
to call UserInterfaceControl#selectProofObligation(InitConfig)
if no Proof
is defined by the loaded proof or false
otherwise which still allows to work with the loaded InitConfig
.protected void setProof(Proof proof)
public final void load() throws ProofInputException, java.io.IOException, ProblemLoaderException
ProofInputException
- Occurred Exception.java.io.IOException
- Occurred Exception.ProblemLoaderException
- Occurred Exception.protected void loadEnvironment() throws ProofInputException, java.io.IOException
ProofInputException
- Occurred Exception.java.io.IOException
- Occurred Exception.load()
protected void selectAndLoadProof(ProblemLoaderControl control, InitConfig initConfig)
control
- the ui controller.initConfig
- the proof configuration.load()
protected void loadSelectedProof(IPersistablePO.LoadedPOContainer poContainer, ProofAggregate proofList) throws ProofInputException, ProblemLoaderException
poContainer
- the container created by createProofObligationContainer()
.proofList
- the proof list containing the proof to load.ProofInputException
- Occurred Exception.ProblemLoaderException
- Occurred Exception.load()
protected ProblemLoaderException recoverParserErrorMessage(java.lang.Exception e)
protected FileRepo createFileRepo() throws java.io.IOException
java.io.IOException
- if for some reason the FileRepo can not be created
(e.g. temporary directory can not be created).protected EnvInput createEnvInput(FileRepo fileRepo) throws java.io.IOException
EnvInput
which represents the file to load.fileRepo
- the FileRepo used to ensure consistency between proof and source codeEnvInput
.java.io.IOException
- Occurred Exception.protected ProblemInitializer createProblemInitializer(FileRepo fileRepo)
ProblemInitializer
to use.fileRepo
- the FileRepo used to ensure consistency between proof and source coderegisterProof
- Register loaded Proof
ProblemInitializer
to use.protected InitConfig createInitConfig() throws ProofInputException
InitConfig
.InitConfig
.ProofInputException
- Occurred Exception.protected IPersistablePO.LoadedPOContainer createProofObligationContainer() throws java.io.IOException
IPersistablePO.LoadedPOContainer
if available which contains
the ProofOblInput
for which a Proof
should be instantiated.IPersistablePO.LoadedPOContainer
or null
if not available.java.io.IOException
- Occurred Exception.protected ProofAggregate createProof(IPersistablePO.LoadedPOContainer poContainer) throws ProofInputException
Proof
for the given IPersistablePO.LoadedPOContainer
and
tries to apply rules again.poContainer
- The IPersistablePO.LoadedPOContainer
to instantiate a Proof
for.Proof
.ProofInputException
- Occurred Exception.public boolean hasProofScript()
true
iff there is a proof script to runpublic Pair<java.lang.String,Location> readProofScript() throws ProofInputException
ProofInputException
public Pair<java.lang.String,Location> getProofScript() throws ProblemLoaderException
ProblemLoaderException
public java.io.File getFile()
public java.util.List<java.io.File> getClassPath()
public java.io.File getBootClassPath()
public EnvInput getEnvInput()
EnvInput
which describes the file to load.EnvInput
which describes the file to load.public ProblemInitializer getProblemInitializer()
ProblemInitializer
used during the loading process.ProblemInitializer
used during the loading process.public InitConfig getInitConfig()
InitConfig
which provides access to the loaded source elements and specifications.InitConfig
which provides access to the loaded source elements and specifications.public Proof getProof()
null
if no proof was instantiated during loading process.null
if no proof was instantiated during loading process.public AbstractProblemLoader.ReplayResult getResult()
AbstractProblemLoader.ReplayResult
if available.AbstractProblemLoader.ReplayResult
or null
if not available.public void setProofPath(java.io.File proofFilename)
public boolean isLoadSingleJavaFile()
public void setLoadSingleJavaFile(boolean loadSingleJavaFile)
Copyright © 2003-2019 The KeY-Project.