org.jmlspecs.checker
Class JmlStoreRefExpression

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Phylum
          org.multijava.mjc.JPhylum
              org.jmlspecs.checker.JmlNode
                  org.jmlspecs.checker.JmlStoreRef
                      org.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

JmlStoreRefExpression

public JmlStoreRefExpression(TokenReference where,
                             JmlName[] names)

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