JML

org.jmlspecs.checker
Class JmlStoreRefExpression

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.util.compiler.Phylum
          extended byorg.multijava.mjc.JPhylum
              extended byorg.jmlspecs.checker.JmlNode
                  extended byorg.jmlspecs.checker.JmlStoreRef
                      extended byorg.jmlspecs.checker.JmlStoreRefExpression
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, PhylumType

public class JmlStoreRefExpression
extends JmlStoreRef

An AST node class for JML store reference expressions. The production rule for the store reference expressions, store-ref-expression is defined as follows.

  store-ref-expression ::= store-ref-name [ store-ref-name-suffix ] ...
  store-ref-name ::= ident | "super" | "this"
  store-ref-name-suffix ::= "." ident | "this" | "[" spec-array-ref-expr "]"
  spec-array-ref-expr ::= spec-expression
    | spec-expression ".." spec-expression
    | "*"
 

Version:
$Revision: 1.20 $
Author:
Yoonsik Cheon

Nested Class Summary
 
Nested classes inherited from class org.jmlspecs.checker.JmlNode
JmlNode.DummyInitializerDeclaration
 
Field Summary
private  JExpression expression
           
private  boolean isFieldsOf
           
private  String name
           
private  JmlName[] names
          The initial name and name suffixes of this store-ref-expression.
 
Fields inherited from class org.jmlspecs.checker.JmlNode
MJCVISIT_MESSAGE
 
Fields inherited from class org.multijava.mjc.JPhylum
EMPTY
 
Fields inherited from class org.multijava.util.compiler.Phylum
 
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
JmlStoreRefExpression(TokenReference where, JmlName[] names)
           
 
Method Summary
 void accept(MjcVisitor p)
          Accepts the specified visitor.
 JExpression expression()
          Returns an expression object corresponding to this store ref expression.
 CFieldAccessor getField()
          Returns CFieldAccessor of this store ref expression if it denotes denotes a class field.
 String getName()
           
 CType getType()
          Returns the type of this store ref expression.
 boolean isFieldOfReceiver()
          Returns true if the store-ref expression refers to a field of the current receiver (this).
 boolean isInvalidModelFieldRef()
          Returns true iff the store ref expression accesses a field of a model field.
 boolean isLocalVarReference()
           
 boolean isModelField()
          Returns true if the given argument refers to a model field.
 boolean isStoreRefExpression()
           
 boolean isSuperExpression()
          Returns true iff the store ref expression is the pseudo variable 'super'.
 boolean isThisExpression()
          Returns true iff the store ref expression is the receiver 'this'.
 JmlName[] names()
           
 String toString()
           
 JmlStoreRef typecheck(CExpressionContextType context, long privacy)
          Typechecks this store reference in the given visibility, privacy, and mutates the context, context, to record information gathered during typechecking.
 JmlStoreRef typecheck(CExpressionContextType context, long privacy, CType type)
          Typechecks this store reference in the given visibility, privacy, and mutates the context, context, to record information gathered during typechecking.
 
Methods inherited from class org.jmlspecs.checker.JmlStoreRef
clone, isEverything, isInformalStoreRef, isNothing, isNothingOrNotSpecified, isNotSpecified, isPrivateData
 
Methods inherited from class org.jmlspecs.checker.JmlNode
enterSpecScope, enterSpecScope, exitSpecScope, exitSpecScope, privacy, privacyString
 
Methods inherited from class org.multijava.mjc.JPhylum
check, check, check, check, fail, fail, fail, warn, warn, warn, warn
 
Methods inherited from class org.multijava.util.compiler.Phylum
getTokenReference, setTokenReference
 
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
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

names

private final JmlName[] names
The initial name and name suffixes of this store-ref-expression.


expression

private JExpression expression

isFieldsOf

private boolean isFieldsOf

name

private final String name
Constructor Detail

JmlStoreRefExpression

public JmlStoreRefExpression(TokenReference where,
                             JmlName[] names)
Method Detail

isStoreRefExpression

public boolean isStoreRefExpression()
Overrides:
isStoreRefExpression in class JmlStoreRef

getName

public String getName()

names

public JmlName[] names()

getType

public CType getType()
Returns the type of this store ref expression. If this store ref expression denotes a spec array ref expression, e.g., a[*], its element type is returned. This method must be called after type checking.


expression

public JExpression expression()
Returns an expression object corresponding to this store ref expression. This method must be called after type checking.


isSuperExpression

public boolean isSuperExpression()
Returns true iff the store ref expression is the pseudo variable 'super'. This method must be called after type checking.

Overrides:
isSuperExpression in class JmlStoreRef

isThisExpression

public boolean isThisExpression()
Returns true iff the store ref expression is the receiver 'this'. This method must be called after type checking.

Overrides:
isThisExpression in class JmlStoreRef

isInvalidModelFieldRef

public boolean isInvalidModelFieldRef()
Returns true iff the store ref expression accesses a field of a model field. This method must be called after type checking.

Overrides:
isInvalidModelFieldRef in class JmlStoreRef

toString

public String toString()
Overrides:
toString in class Object

isModelField

public boolean isModelField()
Returns true if the given argument refers to a model field. This method must be called after typechecking.

  requires (* called after typechecking *);
 


isFieldOfReceiver

public boolean isFieldOfReceiver()
Returns true if the store-ref expression refers to a field of the current receiver (this).

Overrides:
isFieldOfReceiver in class JmlStoreRef

getField

public CFieldAccessor getField()
Returns CFieldAccessor of this store ref expression if it denotes denotes a class field. Otherwise, return null. This method must be called after typechecking.

  requires (* called after typechecking *);
 


isLocalVarReference

public boolean isLocalVarReference()
Overrides:
isLocalVarReference in class JmlStoreRef

typecheck

public JmlStoreRef typecheck(CExpressionContextType context,
                             long privacy)
                      throws PositionedError
Typechecks this store reference in the given visibility, privacy, and mutates the context, context, to record information gathered during typechecking.

Parameters:
context - the context in which this store reference appears
privacy - the visibility in which to typecheck
Returns:
a desugared store reference
Throws:
PositionedError - if the check fails

typecheck

public JmlStoreRef typecheck(CExpressionContextType context,
                             long privacy,
                             CType type)
                      throws PositionedError
Typechecks this store reference in the given visibility, privacy, and mutates the context, context, to record information gathered during typechecking.

Parameters:
context - the context in which this store reference appears
privacy - the visibility in which to typecheck
type - the type whose fields this store reference is supposed to denote
Returns:
a desugared store reference
Throws:
PositionedError - if the check fails

accept

public void accept(MjcVisitor p)
Accepts the specified visitor.

Overrides:
accept in class JmlStoreRef
Parameters:
p - the visitor

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.