org.jmlspecs.checker
Class JmlSourceField

java.lang.Object
  org.multijava.util.Utils
      org.multijava.mjc.CMember
          org.multijava.mjc.CField
              org.multijava.mjc.CSourceField
                  org.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_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, 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_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, 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, 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_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, deprecated, getCClass, getCCompilationUnit, getIdent, getJavaName, getMethod, getOwnerName, getQualNameWithSeparator, hasDefaultAccess, hasProtectedVisibilityIn, host, ident, isAccessibleFrom, 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

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

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.