org.jmlspecs.checker
Class JmlMethodContext

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.checker.JmlContext
          org.jmlspecs.checker.JmlMethodContext

All Implemented Interfaces:

CContextType, Cloneable, CMethodContextType, Constants, Constants, Constants

Direct Known Subclasses:

JmlConstructorContext, JmlInitializerContext

public class JmlMethodContext

extends JmlContext

implements CMethodContextType

This class represents the context for a method 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
protected	JmlMethodContext(CContextType parent)
(package private)	JmlMethodContext(CContextType parent, CMethod self)           Create a context in which to check a method.

 

Method Summary
void	addThrowable(CThrowableInfo throwable)           Registers that the given throwable can be thrown within this context.
CFlowControlContextType	createFlowControlContext(int localVars, boolean isInExternalGF, TokenReference where)
CFlowControlContextType	createFlowControlContext(int localVars, TokenReference where)
CMethod	getCMethod()           Returns the signature of the method declaration in which this context is enclosed, or null if this context is not enclosed in a method declaration.
CMethodContextType	getMethodContext()           Returns the nearest surrounding context of type CMethodContext.
boolean	isInConstructor()           Indicates whether this context is enclosed in a constructor.
boolean	isInInitializer()           Indicates whether this context is enclosed in an instance or static initializer.
boolean	isPure()           Indicates whether this context is "pure".
boolean	isStatic()           Indicates whether this context is "static".
CTypeVariable	lookupTypeVariable(String ident)           search for type variable that are accessible
Set	throwables()
void	verifyExceptions(TokenReference ref)           Verifies that all checked exceptions are defined in the throw list.

 

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, findNearestHost, getClassContext, getCompilationUnit, getCompiler, getContextNullity, getFANonNulls, getFANulls, getFlowControlContext, getHostClass, getParentContext, initializeField, inSpecScope, isBeforeSuperConstructorCall, isFANonNull, isFieldDefinitelyAssigned, isInLoop, lookupClass, lookupField, lookupField, lookupLocalVariable, lookupMethod, lookupMethod, lookupMethodOrSet, lookupMethodOrSet, lookupOuterField, lookupOuterField, lookupOuterLocalVariable, mergeNullityInfo, modUtil, registerGFDecl, registerVisibleMethod, registerVisibleType, removeAllFANullity, removeFANonNull, replaceFieldInfoUpTo, reportTrouble, resolveMaybeExtMethodRef

 

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.CContextType

addFANonNull, addFANonNulls, addFANull, addFANulls, adoptNullityInfo, arithmeticMode, catchUp, check, check, check, check, classToGenerate, createClassContext, createExtMethodContext, createInterfaceContext, declaredOutsideOfLoop, declares, dumpNonNulls, fail, fail, findNearestHost, getClassContext, getCompilationUnit, getCompiler, getFANonNulls, getFANulls, getFlowControlContext, getParentContext, initializeField, isBeforeSuperConstructorCall, isFANonNull, isFieldDefinitelyAssigned, isInLoop, lookupClass, lookupField, lookupField, lookupLocalVariable, lookupMethod, lookupMethod, lookupMethodOrSet, lookupMethodOrSet, lookupOuterField, lookupOuterField, lookupOuterLocalVariable, mergeNullityInfo, modUtil, registerGFDecl, registerVisibleMethod, registerVisibleType, removeAllFANullity, removeFANonNull, replaceFieldInfoUpTo, reportTrouble, resolveMaybeExtMethodRef

 

Constructor Detail

JmlMethodContext

JmlMethodContext(CContextType parent,
                 CMethod self)

Create a context in which to check a method. Clients should not call this but should instead call CClassContextType.createMethodContext.

 requires (* \caller instanceof CContextType *);
 

Parameters:

parent - the parent context

self - the corresponding method interface

See Also:

CClassContextType.createMethodContext(CMethod)

JmlMethodContext

protected JmlMethodContext(CContextType parent)

verifyExceptions

public void verifyExceptions(TokenReference ref)
                      throws PositionedError

Verifies that all checked exceptions are defined in the throw list.

Specified by:

verifyExceptions in interface CMethodContextType

Throws:

PositionedError - if checks fail

createFlowControlContext

public CFlowControlContextType createFlowControlContext(int localVars,
                                                        TokenReference where)

Specified by:

createFlowControlContext in interface CMethodContextType

createFlowControlContext

public CFlowControlContextType createFlowControlContext(int localVars,
                                                        boolean isInExternalGF,
                                                        TokenReference where)

Specified by:

createFlowControlContext in interface CMethodContextType

getCMethod

public CMethod getCMethod()

Returns the signature of the method declaration in which this context is enclosed, or null if this context is not enclosed in a method declaration.

Specified by:

getCMethod in interface CMethodContextType

Overrides:

getCMethod in class JmlContext

getMethodContext

public CMethodContextType getMethodContext()

Returns the nearest surrounding context of type CMethodContext.

Specified by:

getMethodContext in interface CMethodContextType

Overrides:

getMethodContext in class JmlContext

lookupTypeVariable

public CTypeVariable lookupTypeVariable(String ident)
                                 throws UnpositionedError

Description copied from interface: CContextType

search for type variable that are accessible

Specified by:

lookupTypeVariable in interface CContextType

Overrides:

lookupTypeVariable in class JmlContext

Throws:

UnpositionedError

isInInitializer

public boolean isInInitializer()

Indicates whether this context is enclosed in an instance or static initializer.

Specified by:

isInInitializer in interface CMethodContextType

Overrides:

isInInitializer in class JmlContext

isInConstructor

public boolean isInConstructor()

Indicates whether this context is enclosed in a constructor.

Specified by:

isInConstructor in interface CMethodContextType

Overrides:

isInConstructor in class JmlContext

isStatic

public boolean isStatic()

Indicates whether this context is "static".

Specified by:

isStatic in interface CMethodContextType

Overrides:

isStatic in class JmlContext

Returns:

true iff this context is enclosed in a context for a static initializer or static method.

isPure

public boolean isPure()

Indicates whether this context is "pure". By WMD.

Specified by:

isPure in interface CMethodContextType

Overrides:

isPure in class JmlContext

Returns:

true iff this context is enclosed in a pure method.

addThrowable

public void addThrowable(CThrowableInfo throwable)

Description copied from interface: CMethodContextType

Registers that the given throwable can be thrown within this context. The implementation passes the throwable up through the nested contexts until a surrounding context is found that can handle throwables. For example, a CMethodContextType instance collects the throwables that are uncaught within a method body, while a CTryContext collects the throwables that are thrown within a try-block and are therefore subject to handling by associated catch-blocks.

Specified by:

addThrowable in interface CMethodContextType

Parameters:

throwable - the type of the new throwable

throwables

public Set throwables()

Specified by:

throwables in interface CMethodContextType

Returns:

the list of exception that may be thrown