org.jmlspecs.jml4.ast
Class JmlModifier

java.lang.Object
  org.jmlspecs.jml4.ast.JmlModifier

public class JmlModifier
extends java.lang.Object

This class offers services for processing JML modifiers. Note that non_null, nullable and the *_by_default modifiers are not handled here (yet).

Field Summary

static long	CODE_BIGINT_MATH
static long	CODE_JAVA_MATH
static long	CODE_SAFE_MATH
static long	GHOST
static long	HELPER
static long	INSTANCE
static long	MODEL
static long	NON_NULL
static long	NON_NULL_BY_DEFAULT
static long	NULLABLE
static long	NULLABLE_BY_DEFAULT
static long	PEER
static long	PURE
static long	READONLY
static long	REP
static long	SPEC_BIGINT_MATH
static long	SPEC_JAVA_MATH
static long	SPEC_PROTECTED
static long	SPEC_PUBLIC
static long	SPEC_SAFE_MATH
static long	UNINITIALIZED

Method Summary

static long	getFromAnnotations(Annotation[] annotations)
static long	getFromAnnotations(AnnotationBinding[] annotations)
static TypeReference	identToTypeRef(char[] origIdentifier, long pos) If origIdentifier is the name of a JML modifier, then return a type reference to the Java 5 annotation class representing the modifier; otherwise return null;
static boolean	isGhost(long jmlModifiers)
static boolean	isHelper(long jmlModifiers)
static boolean	isInstance(long jmlModifiers)
static boolean	isModel(long jmlModifiers)
static boolean	isNonNull(long jmlModifiers)
static boolean	isNonNullByDefault(long jmlModifiers)
static boolean	isNullable(long jmlModifiers)
static boolean	isPeer(long jmlModifiers)
static boolean	isPure(long jmlModifiers)
static boolean	isReadonly(long jmlModifiers)
static boolean	isRep(long jmlModifiers)
static boolean	isSpecProtected(long jmlModifiers)
static boolean	isSpecPublic(long jmlModifiers)
void	traverse(ASTVisitor visitor, BlockScope scope)

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

CODE_BIGINT_MATH

public static final long CODE_BIGINT_MATH

See Also:

Constant Field Values

CODE_JAVA_MATH

public static final long CODE_JAVA_MATH

See Also:

Constant Field Values

CODE_SAFE_MATH

public static final long CODE_SAFE_MATH

See Also:

Constant Field Values

GHOST

public static final long GHOST

See Also:

Constant Field Values

HELPER

public static final long HELPER

See Also:

Constant Field Values

INSTANCE

public static final long INSTANCE

See Also:

Constant Field Values

NON_NULL

public static final long NON_NULL

See Also:

Constant Field Values

NON_NULL_BY_DEFAULT

public static final long NON_NULL_BY_DEFAULT

See Also:

Constant Field Values

NULLABLE

public static final long NULLABLE

See Also:

Constant Field Values

NULLABLE_BY_DEFAULT

public static final long NULLABLE_BY_DEFAULT

See Also:

Constant Field Values

MODEL

public static final long MODEL

See Also:

Constant Field Values

PEER

public static final long PEER

See Also:

Constant Field Values

PURE

public static final long PURE

See Also:

Constant Field Values

READONLY

public static final long READONLY

See Also:

Constant Field Values

REP

public static final long REP

See Also:

Constant Field Values

SPEC_BIGINT_MATH

public static final long SPEC_BIGINT_MATH

See Also:

Constant Field Values

SPEC_JAVA_MATH

public static final long SPEC_JAVA_MATH

See Also:

Constant Field Values

SPEC_PROTECTED

public static final long SPEC_PROTECTED

See Also:

Constant Field Values

SPEC_PUBLIC

public static final long SPEC_PUBLIC

See Also:

Constant Field Values

SPEC_SAFE_MATH

public static final long SPEC_SAFE_MATH

See Also:

Constant Field Values

UNINITIALIZED

public static final long UNINITIALIZED

See Also:

Constant Field Values

Method Detail

getFromAnnotations

public static long getFromAnnotations(Annotation[] annotations)

getFromAnnotations

public static long getFromAnnotations(AnnotationBinding[] annotations)

isPure

public static boolean isPure(long jmlModifiers)

isHelper

public static boolean isHelper(long jmlModifiers)

isNonNull

public static boolean isNonNull(long jmlModifiers)

isNonNullByDefault

public static boolean isNonNullByDefault(long jmlModifiers)

isNullable

public static boolean isNullable(long jmlModifiers)

isPeer

public static boolean isPeer(long jmlModifiers)

isReadonly

public static boolean isReadonly(long jmlModifiers)

isRep

public static boolean isRep(long jmlModifiers)

isInstance

public static boolean isInstance(long jmlModifiers)

isGhost

public static boolean isGhost(long jmlModifiers)

isModel

public static boolean isModel(long jmlModifiers)

isSpecPublic

public static boolean isSpecPublic(long jmlModifiers)

isSpecProtected

public static boolean isSpecProtected(long jmlModifiers)

identToTypeRef

public static TypeReference identToTypeRef(char[] origIdentifier,
                                           long pos)

If origIdentifier is the name of a JML modifier, then return a type reference to the Java 5 annotation class representing the modifier; otherwise return null;

Parameters:

origIdentifier -

pos -

traverse

public void traverse(ASTVisitor visitor,
                     BlockScope scope)