public class KeYFile extends java.lang.Object implements EnvInput
Modifier and Type | Field and Description |
---|---|
private java.lang.String |
bootClassPath |
private java.lang.String |
chooseContract |
private ImmutableList<java.lang.String> |
classPaths |
protected RuleSource |
file
the RuleSource delivering the input stream for the file.
|
private Includes |
includes |
protected InitConfig |
initConfig |
private java.io.InputStream |
input |
private java.lang.String |
javaPath |
private boolean |
javaPathAlreadyParsed |
protected ProgressMonitor |
monitor
the graphical entity to notify on the state of reading.
|
private java.lang.String |
name |
private Profile |
profile |
private java.lang.String |
proofObligation |
Constructor and Description |
---|
KeYFile(java.lang.String name,
java.io.File file,
ProgressMonitor monitor,
Profile profile)
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,
java.io.File file,
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)
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 | Method and Description |
---|---|
java.lang.String |
chooseContract() |
void |
close() |
private KeYParserF |
createDeclParser(java.io.InputStream is) |
boolean |
equals(java.lang.Object o) |
java.io.File |
getInitialFile()
Returns the initial
File which is loaded if available. |
protected java.io.InputStream |
getNewStream() |
int |
getNumberOfChars()
Returns the total numbers of chars that can be read in this input.
|
protected ProofSettings |
getPreferences() |
Profile |
getProfile()
Returns the
Profile to use. |
java.lang.String |
getProofObligation() |
int |
hashCode() |
java.lang.String |
name()
Returns the name of this input.
|
ImmutableSet<PositionedString> |
read()
Reads the input using the given modification strategy, i.e.,
parts of the input do not modify the initial configuration while
others do.
|
java.io.File |
readBootClassPath()
gets the boot classpath element, null if none set.
|
java.util.List<java.io.File> |
readClassPath()
gets the classpath elements to be considered here.
|
void |
readFuncAndPred()
reads the functions and predicates declared in the .key file only,
modifying the function namespaces of the respective taclet options.
|
Includes |
readIncludes()
Reads the include section and returns an Includes object.
|
java.lang.String |
readJavaPath()
Reads the Java path.
|
ProofSettings |
readPreferences() |
void |
readRulesAndProblem()
reads the rules and problems declared in the .key file only,
modifying the set of rules
of the initial configuration
|
void |
readSorts()
reads the sorts declaration of the .key file only,
modifying the sort namespace
of the initial configuration
|
void |
setInitConfig(InitConfig conf)
Sets the initial configuration the read environment input should be
added to.
|
java.lang.String |
toString() |
private final java.lang.String name
protected final RuleSource file
protected final ProgressMonitor monitor
private java.lang.String javaPath
private boolean javaPathAlreadyParsed
private java.io.InputStream input
protected InitConfig initConfig
private java.lang.String chooseContract
private java.lang.String proofObligation
private final Profile profile
private ImmutableList<java.lang.String> classPaths
private java.lang.String bootClassPath
private Includes includes
public KeYFile(java.lang.String name, RuleSource file, ProgressMonitor monitor, Profile profile)
public KeYFile(java.lang.String name, java.io.File file, ProgressMonitor monitor, Profile profile)
public KeYFile(java.lang.String name, java.io.File file, ProgressMonitor monitor, Profile profile, boolean compressed)
name
- the name of the resourcefile
- the file to find itmonitor
- a possibly null reference to a monitor for the loading
progressprofile
- the KeY profile under which the file is to be loadcompressed
- true
iff the file has compressed contentprivate KeYParserF createDeclParser(java.io.InputStream is) throws java.io.IOException
java.io.IOException
protected java.io.InputStream getNewStream() throws java.io.FileNotFoundException
java.io.FileNotFoundException
protected ProofSettings getPreferences() throws ProofInputException
ProofInputException
public ProofSettings readPreferences() throws ProofInputException
ProofInputException
public java.lang.String name()
EnvInput
public int getNumberOfChars()
EnvInput
getNumberOfChars
in interface EnvInput
public void setInitConfig(InitConfig conf)
EnvInput
setInitConfig
in interface EnvInput
public Includes readIncludes() throws ProofInputException
EnvInput
readIncludes
in interface EnvInput
ProofInputException
public java.io.File readBootClassPath() throws java.io.IOException
EnvInput
readBootClassPath
in interface EnvInput
java.io.IOException
public java.util.List<java.io.File> readClassPath()
EnvInput
readClassPath
in interface EnvInput
public java.lang.String readJavaPath() throws ProofInputException
EnvInput
readJavaPath
in interface EnvInput
ProofInputException
public ImmutableSet<PositionedString> read() throws ProofInputException
EnvInput
read
in interface EnvInput
ImmutableSet
if no warnings occurred.ProofInputException
public void readSorts() throws ProofInputException
ProofInputException
public void readFuncAndPred() throws ProofInputException
ProofInputException
public void readRulesAndProblem() throws ProofInputException
ProofInputException
public void close()
public java.lang.String chooseContract()
public java.lang.String getProofObligation()
public java.lang.String toString()
toString
in class java.lang.Object
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public Profile getProfile()
EnvInput
Profile
to use.getProfile
in interface EnvInput
Profile
to use.public java.io.File getInitialFile()
EnvInput
File
which is loaded if available.getInitialFile
in interface EnvInput
File
which is loaded or null
otherwise.