public final class JMLInfoExtractor
extends java.lang.Object
Constructor and Description |
---|
JMLInfoExtractor() |
Modifier and Type | Method and Description |
---|---|
static boolean |
hasJMLModifier(FieldDeclaration fd,
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.
|
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.
|
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.
|
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) |
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)
Copyright © 2003-2019 The KeY-Project.