de.uka.ilkd.key.speclang

Class SLEnvInput

java.lang.Object

de.uka.ilkd.key.proof.io.AbstractEnvInput

de.uka.ilkd.key.speclang.SLEnvInput

All Implemented Interfaces:

EnvInput

public final class SLEnvInput
extends AbstractEnvInput

EnvInput for standalone specification language front ends.

Field Summary

Fields inherited from class de.uka.ilkd.key.proof.io.AbstractEnvInput

bootClassPath, classPath, includes, initConfig, javaPath, name, profile

Constructor Summary

Constructors

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)

Method Summary

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)

Methods inherited from class de.uka.ilkd.key.proof.io.AbstractEnvInput

getNumberOfChars, getProfile, name, readBootClassPath, readClassPath, readIncludes, readJavaPath, setInitConfig

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

SLEnvInput

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)

SLEnvInput

public SLEnvInput(java.lang.String javaPath,
                  Profile profile)

Method Detail

getLanguage

public static java.lang.String getLanguage()

sortKJTs

private KeYJavaType[] sortKJTs(KeYJavaType[] kjts)

createDLLibrarySpecsHelper

private ImmutableSet<PositionedString> createDLLibrarySpecsHelper(java.util.Set<KeYJavaType> allKJTs,
                                                                  java.lang.String path)
                                                           throws ProofInputException

Throws:

ProofInputException

createDLLibrarySpecs

private ImmutableSet<PositionedString> createDLLibrarySpecs()
                                                     throws ProofInputException

For all library classes C, look for file C.key in same directory; if found, read specifications from this file.

Throws:

ProofInputException

addLoopInvariants

private void addLoopInvariants(SpecExtractor specExtractor,
                               SpecificationRepository specRepos,
                               KeYJavaType kjt,
                               IProgramMethod pm)
                        throws ProofInputException

Throws:

ProofInputException

addLoopContracts

private void addLoopContracts(SpecExtractor specExtractor,
                              SpecificationRepository specRepos,
                              KeYJavaType kjt,
                              IProgramMethod pm)
                       throws ProofInputException

Throws:

ProofInputException

addBlockAndLoopContracts

private void addBlockAndLoopContracts(SpecExtractor specExtractor,
                                      SpecificationRepository specRepos,
                                      IProgramMethod pm)
                               throws ProofInputException

Throws:

ProofInputException

addMergePointStatements

private void addMergePointStatements(SpecExtractor specExtractor,
                                     SpecificationRepository specRepos,
                                     IProgramMethod pm,
                                     ImmutableSet<SpecificationElement> methodSpecs)
                              throws ProofInputException

Throws:

ProofInputException

addLabeledBlockContracts

private void addLabeledBlockContracts(SpecExtractor specExtractor,
                                      SpecificationRepository specRepos,
                                      IProgramMethod pm)
                               throws ProofInputException

Throws:

ProofInputException

addLabeledLoopContracts

private void addLabeledLoopContracts(SpecExtractor specExtractor,
                                     SpecificationRepository specRepos,
                                     IProgramMethod pm)
                              throws ProofInputException

Throws:

ProofInputException

createSpecs

private ImmutableSet<PositionedString> createSpecs(SpecExtractor specExtractor)
                                            throws ProofInputException

Throws:

ProofInputException

read

public ImmutableSet<PositionedString> read()
                                    throws ProofInputException

Description copied from interface: EnvInput

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

getInitialFile

public java.io.File getInitialFile()

Description copied from interface: EnvInput

Returns the initial File which is loaded if available.

Returns:

The initial File which is loaded or null otherwise.