Version:

$Revision: 1.19 $

Author:

Yoonsik Cheon

Nested Class Summary

 

Nested classes inherited from class org.jmlspecs.checker.JmlNode

JmlNode.DummyInitializerDeclaration

 

Field Summary
protected  JmlAssignableFieldSet	assignableFieldSet
protected  JmlAssignableFieldSet	minAssignableFieldSet
protected  JmlSpecBody	specBody
protected  JmlRequiresClause[]	specHeader
protected  JmlSpecVarDecl[]	specVarDecls

 

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
protected	JmlGeneralSpecCase(TokenReference where, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBody specBody)           Creates a new JmlGeneralSpecCase instance.

 

Method Summary
void	accept(MjcVisitor m)           Throws an UnsupportedOperationException since an MjcVisitor cannot be used to visit a JML AST.
void	addRequiresClause(JmlRequiresClause req)           Add the given requires clause to this specification case.
JmlAssignableFieldSet	getAssignableFieldSet(JmlSourceMethod method)           Returns the maximal set of fields that can be assigned to by the given method (takes the union of the assignable clauses from all specification cases).
JmlAssignableFieldSet	getMinAssignableFieldSet(JmlSourceMethod method, JmlDataGroupMemberMap dataGroupMap)           Returns the minimal set of fields that can be assigned to by the given method (takes the intersection of the assignable clauses of all specification cases).
boolean	hasNonRedundantAssignable()           Returns true if this general specification case has a non-redunant assignable clause.
boolean	hasNonRedundantEnsures()           Returns true if this general specification case has a non-redunant ensures clause.
boolean	hasNonRedundantRequiresClause()           Returns true if this general specification case has a non-redunant requires clause.
boolean	hasSpecBody()
boolean	hasSpecHeader()
boolean	hasSpecVarDecls()
protected  long	privacy(CFlowControlContextType context)           Returns the privacy of this specification case.
JmlSpecBody	specBody()
JmlRequiresClause[]	specHeader()
JmlSpecVarDecl[]	specVarDecls()
void	typecheck(CFlowControlContextType context)           Typechecks this specification case in the context in which it appears.
void	typecheck(CFlowControlContextType context, long privacy, boolean isNestedSpecCase)           Typechecks this specification case with the privacy, privacy, in the context in which it appears.

 

Methods inherited from class org.jmlspecs.checker.JmlSpecCase

isCodeSpec

 

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

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

specVarDecls

protected JmlSpecVarDecl[] specVarDecls

specHeader

protected JmlRequiresClause[] specHeader

specBody

protected JmlSpecBody specBody

assignableFieldSet

protected JmlAssignableFieldSet assignableFieldSet

minAssignableFieldSet

protected JmlAssignableFieldSet minAssignableFieldSet

JmlGeneralSpecCase

protected JmlGeneralSpecCase(TokenReference where,
                             JmlSpecVarDecl[] specVarDecls,
                             JmlRequiresClause[] specHeader,
                             JmlSpecBody specBody)

Creates a new JmlGeneralSpecCase instance.

Parameters:

where - a TokenReference value

specVarDecls - an array of spec variable declarations (JmlSpecVarDecl)

specHeader - an array of requires clauses (JmlRequiresClause)

specBody - a specification body (JmlSpecBody)

getAssignableFieldSet

public JmlAssignableFieldSet getAssignableFieldSet(JmlSourceMethod method)

Returns the maximal set of fields that can be assigned to by the given method (takes the union of the assignable clauses from all specification cases).

getMinAssignableFieldSet

public JmlAssignableFieldSet getMinAssignableFieldSet(JmlSourceMethod method,
                                                      JmlDataGroupMemberMap dataGroupMap)

Returns the minimal set of fields that can be assigned to by the given method (takes the intersection of the assignable clauses of all specification cases). This set is used in the checking of assignable fields when there are calls in the method body.

specVarDecls

public JmlSpecVarDecl[] specVarDecls()

specHeader

public JmlRequiresClause[] specHeader()

specBody

public JmlSpecBody specBody()

hasSpecVarDecls

public boolean hasSpecVarDecls()

hasSpecHeader

public boolean hasSpecHeader()

hasSpecBody

public boolean hasSpecBody()

hasNonRedundantAssignable

public boolean hasNonRedundantAssignable()

Returns true if this general specification case has a non-redunant assignable clause.

hasNonRedundantRequiresClause

public boolean hasNonRedundantRequiresClause()

Returns true if this general specification case has a non-redunant requires clause.

hasNonRedundantEnsures

public boolean hasNonRedundantEnsures()

Returns true if this general specification case has a non-redunant ensures clause.

addRequiresClause

public void addRequiresClause(JmlRequiresClause req)

Add the given requires clause to this specification case.

accept

public void accept(MjcVisitor m)

Description copied from class: JmlNode

Throws an UnsupportedOperationException since an MjcVisitor cannot be used to visit a JML AST.

Overrides:

accept in class JmlNode

typecheck

public void typecheck(CFlowControlContextType context,
                      long privacy,
                      boolean isNestedSpecCase)
               throws PositionedError

Typechecks this specification case with the privacy, privacy, in the context in which it appears. Mutates the context to record the information learned during checking.

 requires privacy == ACC_PUBLIC || privacy == ACC_PROTECTED ||
   privacy == ACC_PRIVATE || privacy == 0;
 

Parameters:

context - the context in which this appears

Throws:

PositionedError - if any checks fail

typecheck

public void typecheck(CFlowControlContextType context)
               throws PositionedError

Typechecks this specification case in the context in which it appears. Mutates the context to record the information learned during checking.

Parameters:

context - the context in which this appears

Throws:

PositionedError - if any checks fail

privacy

protected long privacy(CFlowControlContextType context)

Returns the privacy of this specification case. For a light-weight specification, the default privacy is that of the method; for a heavy-weight specification, it is package visibility.

 ensures \result == ACC_PUBLIC || \result == ACC_PROTECTED ||
   \result == ACC_PRIVATE || \result == 0;