public final class JMLSpecExtractor extends Object implements SpecExtractor
Modifier and Type | Field and Description |
---|---|
private static String |
DEFAULT_SIGNALS_ONLY |
private static String |
ERROR |
private JMLSpecFactory |
jsf |
private static String |
RUNTIME_EXCEPTION |
private Services |
services |
private static 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 String |
concatenate(Comment[] comments)
Concatenates the passed comments in a position-preserving way.
|
private ImmutableSet<BlockContract> |
createBlockContracts(IProgramMethod method,
List<Label> labels,
StatementBlock block,
Comment[] comments) |
static ImmutableSet<PositionedString> |
createNonNullPositionedString(String varName,
KeYJavaType kjt,
boolean isImplicitVar,
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.
|
LoopInvariant |
extractLoopInvariant(IProgramMethod pm,
LoopStatement loop)
Returns the loop invariant for the passed loop (if any).
|
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 String |
getDefaultSignalsOnly(IProgramMethod pm) |
private 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,
String fileName) |
private Comment[] |
removeDuplicates(Comment[] comments) |
private static final String THROWABLE
private static final String ERROR
private static final String RUNTIME_EXCEPTION
private static final String DEFAULT_SIGNALS_ONLY
private final Services services
private final JMLSpecFactory jsf
private ImmutableSet<PositionedString> warnings
public JMLSpecExtractor(Services services)
private String concatenate(Comment[] comments)
private int getIndexOfMethodDecl(IProgramMethod pm, TextualJMLConstruct[] constructsArray)
private String getDefaultSignalsOnly(IProgramMethod pm)
public static ImmutableSet<PositionedString> createNonNullPositionedString(String varName, KeYJavaType kjt, boolean isImplicitVar, 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
SLTranslationException
public ImmutableSet<BlockContract> extractBlockContracts(IProgramMethod method, LabeledStatement labeled) throws SLTranslationException
SpecExtractor
extractBlockContracts
in interface SpecExtractor
SLTranslationException
private ImmutableSet<BlockContract> createBlockContracts(IProgramMethod method, List<Label> labels, StatementBlock block, Comment[] comments) throws SLTranslationException
SLTranslationException
private String getFileName(IProgramMethod method)
private TextualJMLConstruct[] parseMethodLevelComments(Comment[] comments, String fileName) throws SLTranslationException
SLTranslationException
public LoopInvariant extractLoopInvariant(IProgramMethod pm, LoopStatement loop) throws SLTranslationException
SpecExtractor
extractLoopInvariant
in interface SpecExtractor
SLTranslationException
public ImmutableSet<PositionedString> getWarnings()
SpecExtractor
getWarnings
in interface SpecExtractor