JML

org.jmlspecs.checker
Class JmlGeneralSpecCase

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.JmlSpecCase
                      extended byorg.jmlspecs.checker.JmlGeneralSpecCase
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, PhylumType
Direct Known Subclasses:
JmlAbruptSpecCase, JmlExceptionalSpecCase, JmlGenericSpecCase, JmlNormalSpecCase

public abstract class JmlGeneralSpecCase
extends JmlSpecCase

An abstraction of JML specification cases. JML supports several kinds of specification cases, and this abstract class is the common superclass of different kinds of specification cases such as normal, exceptional, and generic (i.e., JmlExceptionalSpecCase, JmlNormalSpecCase, and JmlGenericSpecCase). A particular kind of specification case has the following form of production rule:

  X-spec-case :: = [ spec-var-decls ] spec-header [ X-spec-body ]
    | [ spec-var-decls ] X-spec-body
 
where X can be generic, normal, and exceptional.

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
Constructor Detail

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)
Method Detail

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;
 


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.