public final class JMLSpecExtractor extends java.lang.Object implements SpecExtractor
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
DEFAULT_SIGNALS_ONLY |
private static java.lang.String |
ERROR |
private JMLSpecFactory |
jsf |
private static java.lang.String |
RUNTIME_EXCEPTION |
private Services |
services |
private static java.lang.String |
THROWABLE |
private ImmutableSet<PositionedString> |
warnings |
Constructor and Description |
---|
JMLSpecExtractor(Services services) |
Modifier and Type | Method and Description |
---|---|
static int |
arrayDepth(Type type,
Services services)
Get the depth for the nonNull predicate.
|
private java.lang.String |
concatenate(Comment[] comments)
Concatenates the passed comments in a position-preserving way.
|
private ImmutableSet<BlockContract> |
createBlockContracts(IProgramMethod method,
java.util.List<Label> labels,
StatementBlock block,
Comment[] comments) |
private ImmutableSet<LoopContract> |
createLoopContracts(IProgramMethod method,
java.util.List<Label> labels,
LoopStatement loop,
Comment[] comments) |
private ImmutableSet<LoopContract> |
createLoopContracts(IProgramMethod method,
java.util.List<Label> labels,
StatementBlock block,
Comment[] comments) |
static ImmutableSet<PositionedString> |
createNonNullPositionedString(java.lang.String varName,
KeYJavaType kjt,
boolean isImplicitVar,
java.lang.String fileName,
Position pos,
Services services)
creates a JML specification expressing that the given variable/field is
not null and in case of a reference array type that also its elements are
non-null In case of implicit fields or primitive typed fields/variables
the empty set is returned
|
ImmutableSet<BlockContract> |
extractBlockContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the block contracts for the passed labeled statement if it labels
a block.
|
ImmutableSet<BlockContract> |
extractBlockContracts(IProgramMethod method,
StatementBlock block)
Returns the block contracts for the passed block.
|
ImmutableSet<SpecificationElement> |
extractClassSpecs(KeYJavaType kjt)
Returns the class invariants for the passed type.
|
ImmutableSet<LoopContract> |
extractLoopContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the loop contracts for the passed labeled statement if it labels
a block.
|
ImmutableSet<LoopContract> |
extractLoopContracts(IProgramMethod method,
LoopStatement loop)
Returns the loop contracts for the passed loop.
|
ImmutableSet<LoopContract> |
extractLoopContracts(IProgramMethod method,
StatementBlock block)
Returns the loop contracts for the passed block.
|
LoopSpecification |
extractLoopInvariant(IProgramMethod pm,
LoopStatement loop)
Returns the loop invariant for the passed loop (if any).
|
ImmutableSet<MergeContract> |
extractMergeContracts(IProgramMethod method,
MergePointStatement mps,
ImmutableList<ProgramVariable> methodParams)
Returns the
MergeContract s for the given
MergePointStatement . |
ImmutableSet<SpecificationElement> |
extractMethodSpecs(IProgramMethod pm)
Returns the operation contracts for the passed operation.
|
ImmutableSet<SpecificationElement> |
extractMethodSpecs(IProgramMethod pm,
boolean addInvariant)
Extracts method specifications (i.e., contracts) from Java+JML input.
|
private java.lang.String |
getDefaultSignalsOnly(IProgramMethod pm) |
private java.lang.String |
getFileName(IProgramMethod method) |
private int |
getIndexOfMethodDecl(IProgramMethod pm,
TextualJMLConstruct[] constructsArray) |
ImmutableSet<PositionedString> |
getWarnings()
Returns all warnings generated so far in the translation process.
|
private TextualJMLConstruct[] |
parseMethodLevelComments(Comment[] comments,
java.lang.String fileName) |
private Comment[] |
removeDuplicates(Comment[] comments) |
private static final java.lang.String THROWABLE
private static final java.lang.String ERROR
private static final java.lang.String RUNTIME_EXCEPTION
private static final java.lang.String DEFAULT_SIGNALS_ONLY
private final Services services
private final JMLSpecFactory jsf
private ImmutableSet<PositionedString> warnings
public JMLSpecExtractor(Services services)
private java.lang.String concatenate(Comment[] comments)
private int getIndexOfMethodDecl(IProgramMethod pm, TextualJMLConstruct[] constructsArray)
private java.lang.String getDefaultSignalsOnly(IProgramMethod pm)
public static ImmutableSet<PositionedString> createNonNullPositionedString(java.lang.String varName, KeYJavaType kjt, boolean isImplicitVar, java.lang.String fileName, Position pos, Services services)
varName
- the String specifying the variable/field namekjt
- the KeYJavaType representing the variables/field declared typeisImplicitVar
- a boolean indicating if the the field is an implicit one (in
which case nofileName
- the String containing the filename where the field/variable
has been declaredpos
- the Position where to place this implicit specificationpublic static int arrayDepth(Type type, Services services)
public ImmutableSet<SpecificationElement> extractClassSpecs(KeYJavaType kjt) throws SLTranslationException
SpecExtractor
extractClassSpecs
in interface SpecExtractor
SLTranslationException
public ImmutableSet<SpecificationElement> extractMethodSpecs(IProgramMethod pm) throws SLTranslationException
SpecExtractor
extractMethodSpecs
in interface SpecExtractor
SLTranslationException
public ImmutableSet<SpecificationElement> extractMethodSpecs(IProgramMethod pm, boolean addInvariant) throws SLTranslationException
extractMethodSpecs
in interface SpecExtractor
pm
- method to extract foraddInvariant
- whether to add static invariants to pre- and
post-conditionsSLTranslationException
public ImmutableSet<BlockContract> extractBlockContracts(IProgramMethod method, StatementBlock block) throws SLTranslationException
SpecExtractor
extractBlockContracts
in interface SpecExtractor
method
- the program methodblock
- the statement blockSLTranslationException
public ImmutableSet<BlockContract> extractBlockContracts(IProgramMethod method, LabeledStatement labeled) throws SLTranslationException
SpecExtractor
extractBlockContracts
in interface SpecExtractor
method
- the program methodlabeled
- the labeled statementSLTranslationException
- a translation exceptionpublic ImmutableSet<LoopContract> extractLoopContracts(IProgramMethod method, LoopStatement loop) throws SLTranslationException
SpecExtractor
extractLoopContracts
in interface SpecExtractor
method
- the program method containing the loop.loop
- the loop.SLTranslationException
- a translation exceptionpublic ImmutableSet<LoopContract> extractLoopContracts(IProgramMethod method, StatementBlock block) throws SLTranslationException
SpecExtractor
extractLoopContracts
in interface SpecExtractor
method
- the program method containing the block.block
- the block.SLTranslationException
- a translation exceptionpublic ImmutableSet<LoopContract> extractLoopContracts(IProgramMethod method, LabeledStatement labeled) throws SLTranslationException
SpecExtractor
extractLoopContracts
in interface SpecExtractor
method
- the program methodlabeled
- the labeled statementSLTranslationException
- a translation exceptionpublic ImmutableSet<MergeContract> extractMergeContracts(IProgramMethod method, MergePointStatement mps, ImmutableList<ProgramVariable> methodParams) throws SLTranslationException
SpecExtractor
MergeContract
s for the given
MergePointStatement
.extractMergeContracts
in interface SpecExtractor
methodParams
- TODOSLTranslationException
private ImmutableSet<BlockContract> createBlockContracts(IProgramMethod method, java.util.List<Label> labels, StatementBlock block, Comment[] comments) throws SLTranslationException
SLTranslationException
private ImmutableSet<LoopContract> createLoopContracts(IProgramMethod method, java.util.List<Label> labels, LoopStatement loop, Comment[] comments) throws SLTranslationException
SLTranslationException
private ImmutableSet<LoopContract> createLoopContracts(IProgramMethod method, java.util.List<Label> labels, StatementBlock block, Comment[] comments) throws SLTranslationException
SLTranslationException
private java.lang.String getFileName(IProgramMethod method)
private TextualJMLConstruct[] parseMethodLevelComments(Comment[] comments, java.lang.String fileName) throws SLTranslationException
SLTranslationException
public LoopSpecification extractLoopInvariant(IProgramMethod pm, LoopStatement loop) throws SLTranslationException
SpecExtractor
extractLoopInvariant
in interface SpecExtractor
SLTranslationException
public ImmutableSet<PositionedString> getWarnings()
SpecExtractor
getWarnings
in interface SpecExtractor