JML

org.jmlspecs.checker
Class JmlInterfaceContext

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.checker.JmlContext
          extended byorg.jmlspecs.checker.JmlClassContext
              extended byorg.jmlspecs.checker.JmlInterfaceContext
All Implemented Interfaces:
CClassContextType, CContextType, CInterfaceContextType, Cloneable, Constants, Constants, Constants

public class JmlInterfaceContext
extends JmlClassContext
implements CInterfaceContextType

This class represents the context for an interface declaration during checking passes (checkInterface, checkInitializers, typecheck).

See Also:
CContextType

Field Summary
 
Fields inherited from class org.jmlspecs.checker.JmlContext
cunit, delegee, parent
 
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
(package private) JmlInterfaceContext(CContextType parent, CClass clazz)
          Instantiates a context for checking interface declarations.
 
Method Summary
 void checkingComplete(JTypeDeclarationType decl, CVariableInfoTable staticC, CVariableInfoTable instanceC, CVariableInfoTable[] constructorsC)
          Verifies all final fields are initialized. !
 
Methods inherited from class org.jmlspecs.checker.JmlClassContext
addInitializer, createConstructorContext, createInitializerContext, createMethodContext, fieldInfo, fieldInfoTable, findNearestHost, getClassContext, getHostClass, getOwnerClass, hasInitializer, initializeField, isFieldDefinitelyAssigned, lookupClass, lookupField, lookupLocalVariable, lookupMethod, lookupMethodOrSet, lookupOuterField, lookupOuterLocalVariable, lookupTypeVariable, markAllFieldsAsInitialized, registerVisibleType, replaceFieldInfoUpTo, resolveMaybeExtMethodRef, setFieldInfoTable
 
Methods inherited from class org.jmlspecs.checker.JmlContext
addFANonNull, addFANonNulls, addFANull, addFANulls, adoptNullityInfo, arithmeticMode, catchUp, check, check, check, check, classToGenerate, createClassContext, createDummyContext, createExtMethodContext, createInterfaceContext, declaredOutsideOfLoop, declares, dumpNonNulls, enterSpecScope, exitSpecScope, fail, fail, fail, getCMethod, getCompilationUnit, getCompiler, getContextNullity, getFANonNulls, getFANulls, getFlowControlContext, getMethodContext, getParentContext, inSpecScope, isBeforeSuperConstructorCall, isFANonNull, isInConstructor, isInInitializer, isInLoop, isPure, isStatic, lookupField, lookupMethod, lookupMethodOrSet, lookupOuterField, mergeNullityInfo, modUtil, registerGFDecl, registerVisibleMethod, removeAllFANullity, removeFANonNull, reportTrouble
 
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
 
Methods inherited from interface org.multijava.mjc.CClassContextType
addInitializer, createConstructorContext, createInitializerContext, createMethodContext, fieldInfo, fieldInfoTable, findNearestHost, getClassContext, getHostClass, getOwnerClass, hasInitializer, initializeField, isFieldDefinitelyAssigned, lookupClass, lookupField, lookupMethod, lookupMethodOrSet, lookupOuterField, lookupOuterLocalVariable, lookupTypeVariable, markAllFieldsAsInitialized, registerVisibleType, replaceFieldInfoUpTo, resolveMaybeExtMethodRef, setFieldInfoTable
 
Methods inherited from interface org.multijava.mjc.CContextType
addFANonNull, addFANonNulls, addFANull, addFANulls, adoptNullityInfo, arithmeticMode, catchUp, check, check, check, check, classToGenerate, createClassContext, createExtMethodContext, createInterfaceContext, declaredOutsideOfLoop, declares, dumpNonNulls, fail, fail, getCMethod, getCompilationUnit, getCompiler, getFANonNulls, getFANulls, getFlowControlContext, getMethodContext, getParentContext, isBeforeSuperConstructorCall, isFANonNull, isInConstructor, isInInitializer, isInLoop, isPure, isStatic, lookupField, lookupLocalVariable, lookupMethod, lookupMethodOrSet, lookupOuterField, mergeNullityInfo, modUtil, registerGFDecl, registerVisibleMethod, removeAllFANullity, removeFANonNull, reportTrouble
 

Constructor Detail

JmlInterfaceContext

JmlInterfaceContext(CContextType parent,
                    CClass clazz)
Instantiates a context for checking interface declarations. Clients should not call this but should instead call CContextType.createInterfaceContext.

 requires (* \caller instanceof CContextType *);
 

Parameters:
parent - the parent context or null at top level
clazz - the corresponding clazz
See Also:
CContextType.createInterfaceContext(CClass)
Method Detail

checkingComplete

public void checkingComplete(JTypeDeclarationType decl,
                             CVariableInfoTable staticC,
                             CVariableInfoTable instanceC,
                             CVariableInfoTable[] constructorsC)
                      throws UnpositionedError
Verifies all final fields are initialized. !FIXME! Currently checks nothing. Probably needs to check that fields are initialized since interfaces can have fields (or does this initialization then fall to implementors?).

Specified by:
checkingComplete in interface CInterfaceContextType
Overrides:
checkingComplete in class JmlClassContext
Throws:
UnpositionedError - if any checks fail

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.