public class KeYFile extends Object implements EnvInput
Modifier and Type | Field and Description |
---|---|
private String |
bootClassPath |
private String |
chooseContract |
private ImmutableList<String> |
classPaths |
protected RuleSource |
file
the RuleSource delivering the input stream for the file.
|
private Includes |
includes |
protected InitConfig |
initConfig |
private InputStream |
input |
private String |
javaPath |
private boolean |
javaPathAlreadyParsed |
protected ProgressMonitor |
monitor
the graphical entity to notify on the state of reading.
|
private String |
name |
private Profile |
profile |
private String |
proofObligation |
Constructor and Description |
---|
KeYFile(String name,
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(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 |
---|---|
String |
chooseContract() |
void |
close() |
private KeYParserF |
createDeclParser(InputStream is) |
boolean |
equals(Object o) |
File |
getInitialFile()
Returns the initial
File which is loaded if available. |
protected 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. |
String |
getProofObligation() |
int |
hashCode() |
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.
|
File |
readBootClassPath()
gets the boot classpath element, null if none set.
|
List<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.
|
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.
|
String |
toString() |
private final String name
protected final RuleSource file
protected final ProgressMonitor monitor
private String javaPath
private boolean javaPathAlreadyParsed
private InputStream input
protected InitConfig initConfig
private String chooseContract
private String proofObligation
private final Profile profile
private ImmutableList<String> classPaths
private String bootClassPath
private Includes includes
public KeYFile(String name, RuleSource file, ProgressMonitor monitor, Profile profile)
public KeYFile(String name, File file, ProgressMonitor monitor, Profile profile)
private KeYParserF createDeclParser(InputStream is) throws IOException
IOException
protected InputStream getNewStream() throws FileNotFoundException
FileNotFoundException
protected ProofSettings getPreferences() throws ProofInputException
ProofInputException
public ProofSettings readPreferences() throws ProofInputException
ProofInputException
public 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 File readBootClassPath() throws IOException
EnvInput
readBootClassPath
in interface EnvInput
IOException
public List<File> readClassPath()
EnvInput
readClassPath
in interface EnvInput
public 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 String chooseContract()
public String getProofObligation()
public Profile getProfile()
EnvInput
Profile
to use.getProfile
in interface EnvInput
Profile
to use.