public final class JMLInfoExtractor
extends java.lang.Object
Constructor and Description |
---|
JMLInfoExtractor() |
Modifier and Type | Method and Description |
---|---|
private static boolean |
checkFor(java.lang.String key,
ImmutableList<Comment> coms)
Checks whether one of the passed comments is a JML comment
containing "key".
|
private static boolean |
checkFor(java.lang.String key,
java.lang.String comment)
Checks whether "comment" is a JML comment containing "key".
|
private static ImmutableList<Comment> |
extractFieldModifiers(java.lang.String fieldName,
KeYJavaType containingClass)
Extracts the list of comments for a given field.
|
static boolean |
hasJMLModifier(FieldDeclaration fd,
java.lang.String mod) |
private static boolean |
hasJMLModifier(IProgramMethod pm,
java.lang.String mod) |
private static boolean |
hasJMLModifier(TypeDeclaration td,
java.lang.String mod) |
static boolean |
isHelper(IProgramMethod pm)
Returns true iff the given method is specified "helper".
|
static boolean |
isNullable(java.lang.String fieldName,
KeYJavaType containingClass)
Returns true, if containingClass is a reference Type and has a
field declaration with name fieldName, which is explicitly or
implicitly declared "nullable"
|
static boolean |
isNullableByDefault(KeYJavaType t)
Returns true if the given type is specified as nullable, i.e. all fields
and method parameters are by default specified "nullable"
If t is not a reference type, false is returned.
|
static boolean |
isPure(IProgramMethod pm)
Returns true iff the given method is specified "pure".
|
static boolean |
isPureByDefault(KeYJavaType t)
Returns true iff the given type is specified as pure, i.e. all
methods and constructors are by default specified "pure"
If t is not a reference type, false is returned.
|
static boolean |
isStrictlyPure(IProgramMethod pm)
Returns true iff the given method is specified "strictly_pure"
or the containing type is specified so.
|
static boolean |
isStrictlyPureByDefault(KeYJavaType t)
Returns true iff the given type is specified as pure, i.e. all
methods and constructors are by default specified "strictly_pure"
If t is not a reference type, false is returned.
|
static boolean |
parameterIsNullable(IProgramMethod pm,
int pos)
Returns true iff the
pos -th parameter of the given method
is declared "nullable" (implicitly or explicitly). |
static boolean |
parameterIsNullable(IProgramMethod pm,
ParameterDeclaration pd)
Returns true iff the parameter of the given method
is declared "nullable" (implicitly or explicitly).
|
static boolean |
resultIsNullable(IProgramMethod pm) |
private static boolean checkFor(java.lang.String key, java.lang.String comment)
private static boolean checkFor(java.lang.String key, ImmutableList<Comment> coms)
private static boolean hasJMLModifier(TypeDeclaration td, java.lang.String mod)
private static boolean hasJMLModifier(IProgramMethod pm, java.lang.String mod)
private static ImmutableList<Comment> extractFieldModifiers(java.lang.String fieldName, KeYJavaType containingClass)
fieldName
- containingClass
- public static boolean hasJMLModifier(FieldDeclaration fd, java.lang.String mod)
public static boolean isPureByDefault(KeYJavaType t)
public static boolean isStrictlyPureByDefault(KeYJavaType t)
public static boolean isNullableByDefault(KeYJavaType t)
public static boolean isNullable(java.lang.String fieldName, KeYJavaType containingClass)
public static boolean parameterIsNullable(IProgramMethod pm, int pos)
pos
-th parameter of the given method
is declared "nullable" (implicitly or explicitly).public static boolean parameterIsNullable(IProgramMethod pm, ParameterDeclaration pd)
public static boolean resultIsNullable(IProgramMethod pm)
public static boolean isPure(IProgramMethod pm)
public static boolean isHelper(IProgramMethod pm)
public static boolean isStrictlyPure(IProgramMethod pm)