public final class SLEnvInput extends AbstractEnvInput
bootClassPath, classPath, includes, initConfig, javaPath, name, profile
Constructor and Description |
---|
SLEnvInput(java.lang.String javaPath,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
Profile profile,
java.util.List<java.io.File> includes) |
SLEnvInput(java.lang.String javaPath,
Profile profile) |
Modifier and Type | Method and Description |
---|---|
private void |
addBlockAndLoopContracts(SpecExtractor specExtractor,
SpecificationRepository specRepos,
IProgramMethod pm) |
private void |
addLabeledBlockContracts(SpecExtractor specExtractor,
SpecificationRepository specRepos,
IProgramMethod pm) |
private void |
addLabeledLoopContracts(SpecExtractor specExtractor,
SpecificationRepository specRepos,
IProgramMethod pm) |
private void |
addLoopContracts(SpecExtractor specExtractor,
SpecificationRepository specRepos,
KeYJavaType kjt,
IProgramMethod pm) |
private void |
addLoopInvariants(SpecExtractor specExtractor,
SpecificationRepository specRepos,
KeYJavaType kjt,
IProgramMethod pm) |
private void |
addMergePointStatements(SpecExtractor specExtractor,
SpecificationRepository specRepos,
IProgramMethod pm,
ImmutableSet<SpecificationElement> methodSpecs) |
private ImmutableSet<PositionedString> |
createDLLibrarySpecs()
For all library classes C, look for file C.key in same
directory; if found, read specifications from this file.
|
private ImmutableSet<PositionedString> |
createDLLibrarySpecsHelper(java.util.Set<KeYJavaType> allKJTs,
java.lang.String path) |
private ImmutableSet<PositionedString> |
createSpecs(SpecExtractor specExtractor) |
java.io.File |
getInitialFile()
Returns the initial
File which is loaded if available. |
static java.lang.String |
getLanguage() |
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.
|
private KeYJavaType[] |
sortKJTs(KeYJavaType[] kjts) |
getNumberOfChars, getProfile, name, readBootClassPath, readClassPath, readIncludes, readJavaPath, setInitConfig
public SLEnvInput(java.lang.String javaPath, java.util.List<java.io.File> classPath, java.io.File bootClassPath, Profile profile, java.util.List<java.io.File> includes)
public SLEnvInput(java.lang.String javaPath, Profile profile)
public static java.lang.String getLanguage()
private KeYJavaType[] sortKJTs(KeYJavaType[] kjts)
private ImmutableSet<PositionedString> createDLLibrarySpecsHelper(java.util.Set<KeYJavaType> allKJTs, java.lang.String path) throws ProofInputException
ProofInputException
private ImmutableSet<PositionedString> createDLLibrarySpecs() throws ProofInputException
ProofInputException
private void addLoopInvariants(SpecExtractor specExtractor, SpecificationRepository specRepos, KeYJavaType kjt, IProgramMethod pm) throws ProofInputException
ProofInputException
private void addLoopContracts(SpecExtractor specExtractor, SpecificationRepository specRepos, KeYJavaType kjt, IProgramMethod pm) throws ProofInputException
ProofInputException
private void addBlockAndLoopContracts(SpecExtractor specExtractor, SpecificationRepository specRepos, IProgramMethod pm) throws ProofInputException
ProofInputException
private void addMergePointStatements(SpecExtractor specExtractor, SpecificationRepository specRepos, IProgramMethod pm, ImmutableSet<SpecificationElement> methodSpecs) throws ProofInputException
ProofInputException
private void addLabeledBlockContracts(SpecExtractor specExtractor, SpecificationRepository specRepos, IProgramMethod pm) throws ProofInputException
ProofInputException
private void addLabeledLoopContracts(SpecExtractor specExtractor, SpecificationRepository specRepos, IProgramMethod pm) throws ProofInputException
ProofInputException
private ImmutableSet<PositionedString> createSpecs(SpecExtractor specExtractor) throws ProofInputException
ProofInputException
public ImmutableSet<PositionedString> read() throws ProofInputException
EnvInput
ImmutableSet
if no warnings occurred.ProofInputException
public java.io.File getInitialFile()
EnvInput
File
which is loaded if available.File
which is loaded or null
otherwise.