EnvInput (KeY API Documentation)

All Known Implementing Classes:

AbstractEnvInput, EmptyEnvInput, KeYFile, KeYUserProblemFile, LDTInput, SLEnvInput
```
public interface EnvInput
```
Represents an entity read to produce an environment to read a proof obligation. Environment means the initial configuration of a prover containing namespaces and Java model.

Method Summary

All Methods Instance Methods Abstract Methods
Modifier and Type	Method and Description
`java.io.File`	`getInitialFile()` Returns the initial `File` which is loaded if available.
`int`	`getNumberOfChars()` Returns the total numbers of chars that can be read in this input.
`Profile`	`getProfile()` Returns the `Profile` to use.
`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.
`Includes`	`readIncludes()` Reads the include section and returns an Includes object.
`java.lang.String`	`readJavaPath()` Reads the Java path.
`void`	`setInitConfig(InitConfig initConfig)` Sets the initial configuration the read environment input should be added to.

- Method Detail
  - name
```
java.lang.String name()
```
    Returns the name of this input.
  - getNumberOfChars
```
int getNumberOfChars()
```
    Returns the total numbers of chars that can be read in this input.
  - setInitConfig
```
void setInitConfig(InitConfig initConfig)
```
    Sets the initial configuration the read environment input should be added to. Must be called before calling any of the read* methods.
  - readIncludes
```
Includes readIncludes()
               throws ProofInputException
```
    Reads the include section and returns an Includes object.
    
    Throws:
    
    ProofInputException
  - readJavaPath
```
java.lang.String readJavaPath()
                       throws ProofInputException
```
    Reads the Java path.
    
    Throws:
    
    ProofInputException
  - readClassPath
```
java.util.List<java.io.File> readClassPath()
                                    throws ProofInputException
```
    gets the classpath elements to be considered here.
    
    Throws:
    
    ProofInputException
  - readBootClassPath
```
java.io.File readBootClassPath()
                        throws java.io.IOException
```
    gets the boot classpath element, null if none set.
    
    Throws:
    
    java.io.IOException
  - read
```
ImmutableSet<PositionedString> read()
                             throws ProofInputException
```
    Reads the input using the given modification strategy, i.e., parts of the input do not modify the initial configuration while others do.
    
    Returns:
    
    The found warnings or an empty ImmutableSet if no warnings occurred.
    
    Throws:
    
    ProofInputException
  - getProfile
```
Profile getProfile()
```
    Returns the Profile to use.
    
    Returns:
    
    The Profile to use.
  - getInitialFile
```
java.io.File getInitialFile()
```
    Returns the initial File which is loaded if available.
    
    Returns:
    
    The initial File which is loaded or null otherwise.

Interface EnvInput

Method Summary

Method Detail

name

getNumberOfChars

setInitConfig

readIncludes

readJavaPath

readClassPath

readBootClassPath

read

getProfile

getInitialFile