public final class SLEnvInput extends AbstractEnvInput
bootClassPath, classPath, includes, initConfig, javaPath, name, profile
Constructor and Description |
---|
SLEnvInput(String javaPath,
List<File> classPath,
File bootClassPath,
Profile profile,
List<File> includes) |
SLEnvInput(String javaPath,
Profile profile) |
Modifier and Type | Method and Description |
---|---|
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(Set<KeYJavaType> allKJTs,
String path) |
private ImmutableSet<PositionedString> |
createSpecs(SpecExtractor specExtractor) |
File |
getInitialFile()
Returns the initial
File which is loaded if available. |
static 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(String javaPath, List<File> classPath, File bootClassPath, Profile profile, List<File> includes)
public static String getLanguage()
private KeYJavaType[] sortKJTs(KeYJavaType[] kjts)
private ImmutableSet<PositionedString> createDLLibrarySpecsHelper(Set<KeYJavaType> allKJTs, String path) throws ProofInputException
ProofInputException
private ImmutableSet<PositionedString> createDLLibrarySpecs() 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