org.jmlspecs.checker
Class JmlMemberAccess

java.lang.Object
  org.multijava.util.Utils
      org.multijava.mjc.MemberAccess
          org.jmlspecs.checker.JmlMemberAccess

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants

public class JmlMemberAccess

extends MemberAccess

implements Constants

This class represents and contains the information needed to determine whether a member of a class or compilation unit can be accessed from some other member. It has the interface checking code for ensuring that modifiers are valid for the member containing it, e.g., class, field, and method signature classes. The modifier checking code was factored out of JmlTypeDeclaration, JmlFieldDeclaration, and JmlMethodDeclaration rather than using callbacks so the modifier checking could all be done in one class.

See Also:

CMember

Field Summary
protected static long	invalidJmlClassModifiers           The invalid JML class modifiers are ghost, instance, monitored, uninitialized, non_null, and helper.
protected static long	invalidJmlFieldModifiers           The invalid JML field modifiers.
protected static long	invalidJmlMethodModifiers           The invalid JML method modifiers are ghost, instance, monitored, and uninitialized.

 

Fields inherited from class org.multijava.mjc.MemberAccess

host, hostCompilationUnit, interfaceFieldModifiers, interfaceMethodModifiers, invalidAbstractMethodModifiers, invalidClassModifiers, invalidFieldModifiers, invalidMethodModifiers, modifiers, owner

 

Fields inherited from class org.multijava.util.Utils

DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO

 

Fields inherited from interface org.jmlspecs.checker.Constants

ACC2_RAC_METHOD, ACC_CODE, ACC_CODE_BIGINT_MATH, ACC_CODE_JAVA_MATH, ACC_CODE_SAFE_MATH, ACC_GHOST, ACC_HELPER, ACC_INSTANCE, ACC_MODEL, ACC_MONITORED, ACC_QUERY, ACC_SECRET, ACC_SPEC_BIGINT_MATH, ACC_SPEC_JAVA_MATH, ACC_SPEC_PROTECTED, ACC_SPEC_PUBLIC, ACC_SPEC_SAFE_MATH, ACC_UNINITIALIZED, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_BIGINT_MATH, EVERYTHING, JML_JMLObjectSet, NOT_SPECIFIED, NOTHING, OPE_BACKWARD_IMPLIES, OPE_EQUIV, OPE_EXISTS, OPE_FORALL, OPE_IMPLIES, OPE_L_ARROW, OPE_MAX, OPE_MIN, OPE_NOT_EQUIV, OPE_NUM_OF, OPE_PRODUCT, OPE_R_ARROW, OPE_SUBTYPE, OPE_SUM, SAME, TID_BIGINT, TID_REAL, TID_TYPE, TN_JMLOBJECTSET, TN_JMLTYPE, TN_JMLVALUESET

 

Fields inherited from interface org.multijava.mjc.Constants

ACC_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, NULLITY_MODS, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP

 

Fields inherited from interface org.multijava.util.classfile.Constants

ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_SYNTHETIC, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID

 

Constructor Summary

JmlMemberAccess(CClass owner, long modifiers)           Constructs a member export

JmlMemberAccess(CClass owner, CMemberHost host, long modifiers)           Constructs a top-level member export

 

Method Summary
void	checkAccessModifiers(CContextType context, JMemberDeclaration member)           Check illegal combinations of modifiers common to classes, interfaces, fields, and methods.
void	checkClassModifiers(CContextType context, JTypeDeclaration member)           Check for illegal combinations of modifiers specific to classes and interfaces.
void	checkFieldModifiers(CContextType context, JFieldDeclaration member)           Check for illegal combinations of modifiers specific to field declarations.
long	checkInterfaceFieldModifiers(CContextType context, JFieldDeclaration member)           Check for illegal combinations of modifiers disallowed in interface field declarations.
long	checkInterfaceMethodModifiers(CContextType context, JMethodDeclaration member)           Check for illegal combinations of modifiers disallowed in interface method declarations.
void	checkMethodModifiers(CContextType context, JMethodDeclaration member)           Check for illegal combinations of modifiers specific to method declarations.
JMLMathMode	codeArithmeticMode()           Returns the arithmetic mode of the code (or -1 if not specified)
boolean	inJavaFile()           Returns true if this member is declared in a '.java' file.
boolean	isExplicitlyPrivate()           Returns true if this member has a private modifier.
boolean	isExplicitlyProtected()           Returns true iff this member has a protected modifier.
boolean	isExplicitlyPublic()           Returns true iff this member has a public modifier.
boolean	isGhost()           Returns true if this member is a ghost variable.
boolean	isHelper()           Returns true if this member is a helper method.
boolean	isInstance()           Returns true if this member is a instance variable.
boolean	isMemberVisibleInX(CMember member, CMemberHost from)           Indicates whether this is accessible from the given host.
boolean	isModel()           Returns true if this member is a model.
boolean	isMonitored()           Returns true if this member is a monitored field.
boolean	isPrivate()           Returns true if this member is private.
boolean	isProtected()           Returns true if this member is protected, including spec_portected in a JML specification scope.
boolean	isPublic()           Returns true if this member is public, including spec_public in a JML specification scope.
boolean	isPure()           Returns true if this member is pure.
boolean	isQuery()           Returns true if this member is query.
boolean	isSecret()           Returns true if this member is secret.
boolean	isSpecProtected()           Returns true if this member is spec_protected.
boolean	isSpecPublic()           Returns true if this member is spec_public.
boolean	isUninitialized()           Returns true if this member is an uninitialized field.
protected  long	privacy()           Returns the privacy of this declaration.
JMLMathMode	specArithmeticMode()           Returns the arithmetic mode of the spec (or -1 if not specified)

 

Methods inherited from class org.multijava.mjc.MemberAccess

addModifiers, checkExternalMethodModifiers, getCCompilationUnit, getOwnerName, hasDefaultAccess, host, isAbstract, isExternalMethod, isFinal, isInterface, isMemberVisibleIn, isNative, isStatic, isStrictFP, isSynchronized, isTransient, isVolatile, modifiers, owner, removeAbstractModifier, removeFinalModifier, removePrivateModifier, removeStaticModifier, setModifiers, setOwner

 

Methods inherited from class org.multijava.util.Utils

assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray

 

Methods inherited from class java.lang.Object

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

 

Field Detail

invalidJmlClassModifiers

protected static final long invalidJmlClassModifiers

The invalid JML class modifiers are ghost, instance, monitored, uninitialized, non_null, and helper.

invalidJmlFieldModifiers

protected static final long invalidJmlFieldModifiers

The invalid JML field modifiers.

invalidJmlMethodModifiers

protected static final long invalidJmlMethodModifiers

The invalid JML method modifiers are ghost, instance, monitored, and uninitialized.

JmlMemberAccess

public JmlMemberAccess(CClass owner,
                       long modifiers)

Constructs a member export

Parameters:

owner - the owner of this field

modifiers - the modifiers on this field

JmlMemberAccess

public JmlMemberAccess(CClass owner,
                       CMemberHost host,
                       long modifiers)

Constructs a top-level member export

Parameters:

owner - the owner of this member

host - the host of this member's declaration

modifiers - the modifiers on this member

isMemberVisibleInX

public boolean isMemberVisibleInX(CMember member,
                                  CMemberHost from)

Indicates whether this is accessible from the given host.

Parameters:

member - the member that needs to be accessed

from - the host that wants to access member

Returns:

true iff the given host is allowed access to this member

inJavaFile

public boolean inJavaFile()

Returns true if this member is declared in a '.java' file.

isPublic

public boolean isPublic()

Returns true if this member is public, including spec_public in a JML specification scope.

Overrides:

isPublic in class MemberAccess

isProtected

public boolean isProtected()

Returns true if this member is protected, including spec_portected in a JML specification scope.

Overrides:

isProtected in class MemberAccess

isPrivate

public boolean isPrivate()

Returns true if this member is private. In a JML specification scope, it also means not being spec_public nor spec_protected.

Overrides:

isPrivate in class MemberAccess

isExplicitlyPublic

public boolean isExplicitlyPublic()

Returns true iff this member has a public modifier.

isExplicitlyProtected

public boolean isExplicitlyProtected()

Returns true iff this member has a protected modifier.

isExplicitlyPrivate

public boolean isExplicitlyPrivate()

Returns true if this member has a private modifier.

isSpecPublic

public boolean isSpecPublic()

Returns true if this member is spec_public.

isSpecProtected

public boolean isSpecProtected()

Returns true if this member is spec_protected.

isPure

public boolean isPure()

Returns true if this member is pure. A member is pure if it is annotated with the JML pure modifier.

Overrides:

isPure in class MemberAccess

isQuery

public boolean isQuery()

Returns true if this member is query. A member is query if it is annotated with the JML query modifier.

isSecret

public boolean isSecret()

Returns true if this member is secret. A member is secret if it is annotated with the JML secret modifier.

isModel

public boolean isModel()

Returns true if this member is a model. It is a model member if it is annotated with the JML model modifier.

isGhost

public boolean isGhost()

Returns true if this member is a ghost variable. A member is a ghost variable if it is annotated with the JML ghost modifier.

isInstance

public boolean isInstance()

Returns true if this member is a instance variable. It is an instance variable if it is annotated with the JML instance modifier.

isHelper

public boolean isHelper()

Returns true if this member is a helper method. A member is a helper if it is annotated with the JML helper modifier.

isMonitored

public boolean isMonitored()

Returns true if this member is a monitored field. A member is monitored if it is annotated with the JML monitored modifier.

isUninitialized

public boolean isUninitialized()

Returns true if this member is an uninitialized field. A member is uninitialized if it is annotated with the JML uninitialized modifier.

privacy

protected long privacy()

Returns the privacy of this declaration. If the modifiers has either SPEC_PUBLIC or SPEC_PROTECTED, then that access modifier takes a precedence over the JAVA access modifiers.

codeArithmeticMode

public JMLMathMode codeArithmeticMode()

Returns the arithmetic mode of the code (or -1 if not specified)

specArithmeticMode

public JMLMathMode specArithmeticMode()

Returns the arithmetic mode of the spec (or -1 if not specified)

checkAccessModifiers

public void checkAccessModifiers(CContextType context,
                                 JMemberDeclaration member)
                          throws PositionedError

Check illegal combinations of modifiers common to classes, interfaces, fields, and methods.

Overrides:

checkAccessModifiers in class MemberAccess

Throws:

PositionedError

checkClassModifiers

public void checkClassModifiers(CContextType context,
                                JTypeDeclaration member)
                         throws PositionedError

Check for illegal combinations of modifiers specific to classes and interfaces.

Overrides:

checkClassModifiers in class MemberAccess

Throws:

PositionedError

checkFieldModifiers

public void checkFieldModifiers(CContextType context,
                                JFieldDeclaration member)
                         throws PositionedError

Check for illegal combinations of modifiers specific to field declarations.

Overrides:

checkFieldModifiers in class MemberAccess

Throws:

PositionedError

checkInterfaceFieldModifiers

public long checkInterfaceFieldModifiers(CContextType context,
                                         JFieldDeclaration member)
                                  throws PositionedError

Check for illegal combinations of modifiers disallowed in interface field declarations. Adds the default public, static, and final modifiers (not done for model/ghost fields); these default modifiers are the only ones allowed for fields declared in interfaces.

Overrides:

checkInterfaceFieldModifiers in class MemberAccess

Returns:

the new set of modifiers

Throws:

PositionedError

checkMethodModifiers

public void checkMethodModifiers(CContextType context,
                                 JMethodDeclaration member)
                          throws PositionedError

Check for illegal combinations of modifiers specific to method declarations.

Overrides:

checkMethodModifiers in class MemberAccess

Throws:

PositionedError

checkInterfaceMethodModifiers

public long checkInterfaceMethodModifiers(CContextType context,
                                          JMethodDeclaration member)
                                   throws PositionedError

Check for illegal combinations of modifiers disallowed in interface method declarations. Adds the default public and abstract modifiers (not done for model methods); these default modifiers are the only ones allowed for methods declared in interfaces.

Overrides:

checkInterfaceMethodModifiers in class MemberAccess

Returns:

the new set of modifiers

Throws:

PositionedError