JML

org.jmlspecs.checker
Class JmlSourceField

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.mjc.CMember
          extended byorg.multijava.mjc.CField
              extended byorg.multijava.mjc.CSourceField
                  extended byorg.jmlspecs.checker.JmlSourceField
All Implemented Interfaces:
CFieldAccessor, Cloneable, Constants, Constants, Constants, org.jmlspecs.util.classfile.JmlModifiable, VariableDescriptor

public class JmlSourceField
extends CSourceField
implements org.jmlspecs.util.classfile.JmlModifiable, Constants

A class for representing an exported field of a class. This class provides JML-specific handling of fields by overriding several inherited methods. For example, the visibility observer methods such as isPublic, isProtected, and isPrivate now consider spec_public-ness and spec_protected-ness too.

Version:
$Revision: 1.15 $
Author:
Yoonsik Cheon

Field Summary
private  JmlMemberDeclaration fieldAST
           
 
Fields inherited from class org.multijava.mjc.CSourceField
initialized
 
Fields inherited from class org.multijava.mjc.CField
 
Fields inherited from class org.multijava.mjc.CMember
 
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
JmlSourceField(JmlMemberAccess access, String ident, CType type, boolean deprecated)
          Constructs a field export
 
Method Summary
protected  FieldInfo createFieldInfo(int modifiers, String name, String type, Object value, boolean deprecated, boolean synthetic)
          Creates a new field info object.
 JmlMemberDeclaration getAST()
          Returns the AST for this field.
 JmlSourceField getMostRefined()
          Returns the most refined declaration AST for this field.
 boolean inJavaFile()
          Returns true if this member is declared in a '.java' file.
 boolean isDataGroup()
          Returns true if this member has an associated data group.
 boolean isDefinitelyAssigned()
           
 boolean isEffectivelyModel()
          Returns true iff this field should be treated as a model field; the field itself is defined as model (or ghost) or it is defined in a model class or interface.
 boolean isGhost()
          Returns true iff this field is explicitly declared as ghost.
 boolean isLocalTo(CMemberHost from)
          Indicates whether the declaration of this member is local to the given host.
 boolean isModel()
          Returns true iff this field is explicitly declared as model.
 JmlMemberAccess jmlAccess()
           
 void setAST(JmlMemberDeclaration fieldAST)
          Sets the AST for this field.
 
Methods inherited from class org.multijava.mjc.CSourceField
index, initializedUnlessFinalInstance, isUsed, setIndex, setUsed, toString
 
Methods inherited from class org.multijava.mjc.CField
createFieldInfo, genFieldInfo, genLoad, genStore, getField, getType, getValue, isFieldStatic, setType, setValue
 
Methods inherited from class org.multijava.mjc.CMember
access, addModifiers, deprecated, getCClass, getCCompilationUnit, getIdent, getJavaName, getMethod, getOwnerName, getQualNameWithSeparator, hasDefaultAccess, hasProtectedVisibilityIn, host, ident, isAccessibleFrom, isDeclaredNonNull, isDeprecated, isFinal, isPrivate, isProtected, isPublic, isStatic, modifiers, owner, qualifiedName, setModifiers
 
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, wait, wait, wait
 
Methods inherited from interface org.multijava.mjc.VariableDescriptor
ident, isFinal
 
Methods inherited from interface org.multijava.mjc.CFieldAccessor
ident, isFinal, isStatic, owner
 

Field Detail

fieldAST

private JmlMemberDeclaration fieldAST
Constructor Detail

JmlSourceField

public JmlSourceField(JmlMemberAccess access,
                      String ident,
                      CType type,
                      boolean deprecated)
Constructs a field export

Parameters:
access - contains the info used to determine visibility of this field
ident - the name of this field
type - the type of this field
deprecated - is this field deprecated
Method Detail

isDataGroup

public boolean isDataGroup()
Returns true if this member has an associated data group. That is, model fields and spec_public and spec_protected have associated data groups.


isDefinitelyAssigned

public boolean isDefinitelyAssigned()
Overrides:
isDefinitelyAssigned in class CSourceField

inJavaFile

public boolean inJavaFile()
Returns true if this member is declared in a '.java' file.


isEffectivelyModel

public boolean isEffectivelyModel()
Returns true iff this field should be treated as a model field; the field itself is defined as model (or ghost) or it is defined in a model class or interface.

Specified by:
isEffectivelyModel in interface org.jmlspecs.util.classfile.JmlModifiable

isModel

public boolean isModel()
Returns true iff this field is explicitly declared as model.

Specified by:
isModel in interface org.jmlspecs.util.classfile.JmlModifiable

isGhost

public boolean isGhost()
Returns true iff this field is explicitly declared as ghost.

Specified by:
isGhost in interface org.jmlspecs.util.classfile.JmlModifiable

isLocalTo

public boolean isLocalTo(CMemberHost from)
Description copied from class: CMember
Indicates whether the declaration of this member is local to the given host. There are two cases:
  1. If the given host is not a compilation unit, then this is local to the given host if the declaration of this appears in the same compilation unit in which the declaration of the given host appears.
  2. If the given host is a compilation unit, then this is local to the given host if the declaration of this appears within the given host.

Overrides:
isLocalTo in class CMember

setAST

public void setAST(JmlMemberDeclaration fieldAST)
Sets the AST for this field.


getAST

public JmlMemberDeclaration getAST()
Returns the AST for this field.


getMostRefined

public JmlSourceField getMostRefined()
Returns the most refined declaration AST for this field.


jmlAccess

public JmlMemberAccess jmlAccess()
Returns:
the member access information object for this member.

createFieldInfo

protected FieldInfo createFieldInfo(int modifiers,
                                    String name,
                                    String type,
                                    Object value,
                                    boolean deprecated,
                                    boolean synthetic)
Creates a new field info object. This method is overridden here to return a JML-specific field info object.


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.