JML

org.jmlspecs.checker
Class JmlMemberAccess

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.mjc.MemberAccess
          extended byorg.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.

Constructor Detail

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
Method Detail

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

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.