public final class JMLSpecExtractor extends java.lang.Object implements SpecExtractor
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.
|
static ImmutableSet<LabeledParserRuleContext> |
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.
|
ImmutableList<PositionedString> |
getWarnings()
Returns all warnings generated so far in the translation process.
|
public JMLSpecExtractor(Services services)
public static ImmutableSet<LabeledParserRuleContext> 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
public LoopSpecification extractLoopInvariant(IProgramMethod pm, LoopStatement loop) throws SLTranslationException
SpecExtractor
extractLoopInvariant
in interface SpecExtractor
SLTranslationException
public ImmutableList<PositionedString> getWarnings()
SpecExtractor
getWarnings
in interface SpecExtractor
Copyright © 2003-2019 The KeY-Project.