JML

org.jmlspecs.checker
Class JmlFlowControlContext

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.checker.JmlContext
          extended byorg.jmlspecs.checker.JmlFlowControlContext
All Implemented Interfaces:
CContextType, CFlowControlContextType, Cloneable, Constants, Constants, Constants

public class JmlFlowControlContext
extends JmlContext
implements CFlowControlContextType

This class is used during typechecking for control flow analysis that maintains local variable definite assignment (JLS2, 16), throwable, and reachability information (JLS2, 14.20).


Field Summary
private static int DEFAULT_VAR_ESTIMATE
          Default estimate of the number of local variable slots to reserve.
 
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) JmlFlowControlContext(CFlowControlContextType parent, int varEstimate, TokenReference where)
          Construct a nested flow control context.
protected JmlFlowControlContext(CFlowControlContextType parent, CFlowControlContextType clone)
          Used to clone this flow control context.
(package private) JmlFlowControlContext(CFlowControlContextType parent, TokenReference where)
          Construct a nested flow control context.
(package private) JmlFlowControlContext(CMethodContextType parent, int varEstimate, boolean isInExternalGF, TokenReference where)
          Construct an outer-most flow control context.
(package private) JmlFlowControlContext(CMethodContextType parent, int varEstimate, TokenReference where)
          Construct an outer-most flow control context.
 
Method Summary
 void addFANonNull(Object expr)
          Mark expr (or member) as NonNull in this context
 void addFANonNulls(Object[] exprs)
          adds exprs (or members) as NonNull in this context
 void addFANull(Object expr)
           
 void addFANulls(Object[] exprs)
           
 void addLocalClass(CClass clazz)
          Adds to this context a class declared via a type declaration statement.
 void addSyntheticThisParameter()
          Records that a variable slot must be reserved for a synthetic this parameter.
 void addThisVariable()
          Records that the Java keyword this is used in this block.
 void addThrowable(CThrowableInfo throwable)
          Registers that the given throwable can be thrown within this context.
 void addVariable(JLocalVariable var)
          Adds a local variable to this block
 void adopt(CFlowControlContextType context)
           
 void adoptNullityInfo(CContextType other)
           
 void adoptParallelContexts(CFlowControlContextType[] contexts)
          Adopts the information from the given contexts.
 void checkingComplete()
          Registers that this context is no longer needed.
 CFlowControlContextType cloneContext()
          Create a clone of this context to handle divergent paths in the control flow.
 CExpressionContextType createExpressionContext()
           
 CFlowControlContextType createFinallyContext(CFlowControlContextType tryContext, TokenReference where)
           
 CFlowControlContextType createFlowControlContext(int params, TokenReference where)
           
 CFlowControlContextType createFlowControlContext(TokenReference where)
           
 CLabeledContext createLabeledContext(JLabeledStatement self)
           
 CLoopContext createLoopContext(JLoopStatement self)
           
 CFlowControlContextType[] createParallelContexts(int count, TokenReference where)
          Creates a set of child contexts for typechecking parallel control flows.
 CSwitchBodyContext createSwitchBodyContext(JSwitchStatement stmt, CType switchType)
           
 CTryContext createTryContext(TokenReference where)
           
 boolean declaredOutsideOfLoop(JLocalVariable var)
          Indicates whether this context is enclosed in a loop and the given variable is declared outside the inner-most loop context.
 boolean declares(JLocalVariable var)
          Returns true if the given local variable is declared exactly in this context, i.e., it is not declared in an outer context.
 void dumpNonNulls(String msg)
           
 CVariableInfoTable fieldInfo()
          Returns the field info table
protected  CContextNullity getContextNullity()
           
 Object[] getFANonNulls()
          returns the JPhyla that are known to be non-null in this context.
 Object[] getFANulls()
           
 CFlowControlContextType getFlowControlContext()
          Returns the nearest control flow context (where control flow information is stored.)
 JLabeledStatement getLabeledStatement(String label)
          Returns the statement with the specified label.
 JStatement getNearestBreakableStatement()
          Returns the nearest breakable statement.
 JStatement getNearestContinuableStatement()
          Returns the nearest continuable statement.
 TokenReference getTokenReference()
           
 void initializeField(VariableDescriptor varDesc)
          Marks the field with the given descriptor as definitely assigned to in this context.
 void initializeVariable(VariableDescriptor varDesc)
          Marks the variable with the given descriptor as definitely assigned to in this context.
 boolean isFANonNull(Object expr)
          Indicates whether expr (or member) is conditionally NonNull is this context.
 boolean isFieldDefinitelyAssigned(int pos)
          Indicates whether the field in the given position is definitely assigned to in this context.
 boolean isFreshVariableName(JLocalVariable var)
          Checks whether a local variable has a name that is fresh (i.e., no other local variable in scope has the same name).
 boolean isReachable()
          Indicates whether the statements in this context are reachable up to most recent statement that was typechecked.
 boolean isVarDefinitelyAssigned(int pos)
          Indicates whether the variable in the given position is definitely assigned to in this context.
 boolean isVarDefinitelyUnassigned(int pos)
          Indicates whether the variable in the given position is definitely unassigned to in this context.
 int localsIndex()
           
 int localsPosition()
          Returns the number of stack positions required to store the local variables encountered thus far in this context.
 ArrayList localVars()
          Returns the local variables list
 CClass lookupClass(String name)
          Searches for a class with the given simple name according the procedure in JLS2 6.5.5.
 JLocalVariable lookupLocalVariable(String ident)
          Returns the variable referred to by the given name in this context, recursing to surrounding contexts as appropriate.
 void merge(CFlowControlContextType context)
           
 void mergeNullityInfo(CContextType other)
          Merge the list of guarded nulls in this context with that of the given context.
 int numberOfLocalVars()
           
 int parentIndex()
           
 void removeAllFANullity()
           
 void removeFANonNull(Object expr)
           
 void replaceFieldInfoUpTo(int pos, CVariableInfoTable replacement)
          Replaces the local field info for fields in positions 0 up to pos with the info in replacement.
 void replaceVariableInfoUpTo(int pos, CVariableInfoTable replacement)
          Replaces the local variable info in positions 0 up to pos with the info in replacement.
 void setReachable(boolean reachable)
          Mutates the reachability status of this context.
 CVariableInfoTable variableInfo()
          Returns the variable info table
 
Methods inherited from class org.jmlspecs.checker.JmlContext
arithmeticMode, catchUp, check, check, check, check, classToGenerate, createClassContext, createDummyContext, createExtMethodContext, createInterfaceContext, enterSpecScope, exitSpecScope, fail, fail, fail, findNearestHost, getClassContext, getCMethod, getCompilationUnit, getCompiler, getHostClass, getMethodContext, getParentContext, inSpecScope, isBeforeSuperConstructorCall, isInConstructor, isInInitializer, isInLoop, isPure, isStatic, lookupField, lookupField, lookupMethod, lookupMethod, lookupMethodOrSet, lookupMethodOrSet, lookupOuterField, lookupOuterField, lookupOuterLocalVariable, lookupTypeVariable, modUtil, registerGFDecl, registerVisibleMethod, registerVisibleType, 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
arithmeticMode, catchUp, check, check, check, check, classToGenerate, createClassContext, createExtMethodContext, createInterfaceContext, fail, fail, findNearestHost, getClassContext, getCMethod, getCompilationUnit, getCompiler, getMethodContext, getParentContext, isBeforeSuperConstructorCall, isInConstructor, isInInitializer, isInLoop, isPure, isStatic, lookupField, lookupField, lookupMethod, lookupMethod, lookupMethodOrSet, lookupMethodOrSet, lookupOuterField, lookupOuterField, lookupOuterLocalVariable, lookupTypeVariable, modUtil, registerGFDecl, registerVisibleMethod, registerVisibleType, reportTrouble, resolveMaybeExtMethodRef
 

Field Detail

DEFAULT_VAR_ESTIMATE

private static final int DEFAULT_VAR_ESTIMATE
Default estimate of the number of local variable slots to reserve.

Constructor Detail

JmlFlowControlContext

JmlFlowControlContext(CFlowControlContextType parent,
                      TokenReference where)
Construct a nested flow control context. Clients should not call this but should instead call CCompilationUnitContextType.createFlowControlContext.

 requires (* \caller instanceof CContextType *);
 ensures ((CFlowControlContext)delegee).nestedFlowControlContext;
 

Parameters:
parent - the parent context, it must be different than null except if called by the top level
See Also:
#createFlowControlContext()

JmlFlowControlContext

JmlFlowControlContext(CFlowControlContextType parent,
                      int varEstimate,
                      TokenReference where)
Construct a nested flow control context. Clients should not call this but should instead call createFlowControlContext(int).

 requires (* \caller instanceof CContextType *);
 ensures ((CFlowControlContext)delegee).nestedFlowControlContext;
 

Parameters:
parent - the parent context, it must be different than null
varEstimate - an estimate of the number of variable slots to reserve
See Also:
#createFlowControlContext(int)

JmlFlowControlContext

JmlFlowControlContext(CMethodContextType parent,
                      int varEstimate,
                      TokenReference where)
Construct an outer-most flow control context. Clients should not call this but should instead call CMethodContextType.createFlowControlContext(int).

 requires (* \caller instanceof CContextType *);
 ensures !((CFlowControlContext)delegee).nestedFlowControlContext;
 

Parameters:
parent - the parent context, it must be different than null
varEstimate - an estimate of the number of variable slots to reserve
See Also:
CMethodContextType#createFlowControlContext(int)

JmlFlowControlContext

JmlFlowControlContext(CMethodContextType parent,
                      int varEstimate,
                      boolean isInExternalGF,
                      TokenReference where)
Construct an outer-most flow control context. Clients should not call this but should instead call CMethodContextType.createFlowControlContext(int, boolean).

 requires (* \caller instanceof CContextType *);
 ensures !((CFlowControlContext)delegee).nestedFlowControlContext;
 

Parameters:
parent - the parent context, it must be different than null
varEstimate - an estimate of the number of variable slots to reserve
isInExternalGF - true if we are currently in a method of an external generic function
See Also:
CMethodContextType#createFlowControlContext(int)

JmlFlowControlContext

protected JmlFlowControlContext(CFlowControlContextType parent,
                                CFlowControlContextType clone)
Used to clone this flow control context.

Parameters:
parent - the parent context, it must be different than null
clone - the context whose state is to be adopted
Method Detail

checkingComplete

public void checkingComplete()

Registers that this context is no longer needed. Passes information collected by this context to the parent context.

Passes this context's field information to the surrounding context; passes local variable information to the surrounding context if that context is one which maintains local variable information.

Checks that local variables are used and issues warnings if not.

This should only be called on a linearly nested context! !FIXME!10/26 If we refactor the context creation code as planned (to lock the parent context) then this method is called to unlock the parent context when we exit a linearly nested context.

Specified by:
checkingComplete in interface CFlowControlContextType

getTokenReference

public TokenReference getTokenReference()
Specified by:
getTokenReference in interface CFlowControlContextType

createFlowControlContext

public CFlowControlContextType createFlowControlContext(TokenReference where)
Specified by:
createFlowControlContext in interface CFlowControlContextType

createFlowControlContext

public CFlowControlContextType createFlowControlContext(int params,
                                                        TokenReference where)
Specified by:
createFlowControlContext in interface CFlowControlContextType

createLabeledContext

public CLabeledContext createLabeledContext(JLabeledStatement self)
Specified by:
createLabeledContext in interface CFlowControlContextType

createLoopContext

public CLoopContext createLoopContext(JLoopStatement self)
Specified by:
createLoopContext in interface CFlowControlContextType

createSwitchBodyContext

public CSwitchBodyContext createSwitchBodyContext(JSwitchStatement stmt,
                                                  CType switchType)
Specified by:
createSwitchBodyContext in interface CFlowControlContextType

createTryContext

public CTryContext createTryContext(TokenReference where)
Specified by:
createTryContext in interface CFlowControlContextType

createFinallyContext

public CFlowControlContextType createFinallyContext(CFlowControlContextType tryContext,
                                                    TokenReference where)
Specified by:
createFinallyContext in interface CFlowControlContextType

createExpressionContext

public CExpressionContextType createExpressionContext()
Specified by:
createExpressionContext in interface CFlowControlContextType

cloneContext

public CFlowControlContextType cloneContext()
Create a clone of this context to handle divergent paths in the control flow.

Specified by:
cloneContext in interface CFlowControlContextType

createParallelContexts

public CFlowControlContextType[] createParallelContexts(int count,
                                                        TokenReference where)
Creates a set of child contexts for typechecking parallel control flows. After using the contexts they should be passed to the adoptParallelContexts method of this.

 also
   requires count > 0;
 

Specified by:
createParallelContexts in interface CFlowControlContextType
See Also:
adoptParallelContexts(CFlowControlContextType[])

adoptParallelContexts

public void adoptParallelContexts(CFlowControlContextType[] contexts)
Adopts the information from the given contexts.

 also
   requires contexts != null && contexts.length > 0;
 

Specified by:
adoptParallelContexts in interface CFlowControlContextType

merge

public void merge(CFlowControlContextType context)
Specified by:
merge in interface CFlowControlContextType

adopt

public void adopt(CFlowControlContextType context)
Specified by:
adopt in interface CFlowControlContextType

isFreshVariableName

public boolean isFreshVariableName(JLocalVariable var)
Checks whether a local variable has a name that is fresh (i.e., no other local variable in scope has the same name).

Specified by:
isFreshVariableName in interface CFlowControlContextType
Parameters:
var - the variable

addVariable

public void addVariable(JLocalVariable var)
                 throws UnpositionedError
Adds a local variable to this block

Specified by:
addVariable in interface CFlowControlContextType
Parameters:
var - the name of the variable
Throws:
UnpositionedError - if the variable is a redeclaration

addThisVariable

public void addThisVariable()
Records that the Java keyword this is used in this block.

Specified by:
addThisVariable in interface CFlowControlContextType

addSyntheticThisParameter

public void addSyntheticThisParameter()
Records that a variable slot must be reserved for a synthetic this parameter. Recall that this is passed as a parameter for external methods.

Specified by:
addSyntheticThisParameter in interface CFlowControlContextType

localsPosition

public int localsPosition()
Returns the number of stack positions required to store the local variables encountered thus far in this context.

Specified by:
localsPosition in interface CFlowControlContextType

numberOfLocalVars

public int numberOfLocalVars()
Specified by:
numberOfLocalVars in interface CFlowControlContextType

variableInfo

public CVariableInfoTable variableInfo()
Description copied from interface: CFlowControlContextType
Returns the variable info table

Specified by:
variableInfo in interface CFlowControlContextType

fieldInfo

public CVariableInfoTable fieldInfo()
Description copied from interface: CFlowControlContextType
Returns the field info table

Specified by:
fieldInfo in interface CFlowControlContextType

localVars

public ArrayList localVars()
Description copied from interface: CFlowControlContextType
Returns the local variables list

Specified by:
localVars in interface CFlowControlContextType

parentIndex

public int parentIndex()
Specified by:
parentIndex in interface CFlowControlContextType

localsIndex

public int localsIndex()
Specified by:
localsIndex in interface CFlowControlContextType

setReachable

public final void setReachable(boolean reachable)
Mutates the reachability status of this context.

Specified by:
setReachable in interface CFlowControlContextType
Parameters:
reachable - indicates whether the statements in this context are reachable after the current statement being checked.

isReachable

public final boolean isReachable()
Indicates whether the statements in this context are reachable up to most recent statement that was typechecked. (Assuming that statement's typechecking code calls setReachable appropriately.)

Specified by:
isReachable in interface CFlowControlContextType
Returns:
if this context is still reachable

getLabeledStatement

public JLabeledStatement getLabeledStatement(String label)
Returns the statement with the specified label.

Specified by:
getLabeledStatement in interface CFlowControlContextType

getNearestBreakableStatement

public JStatement getNearestBreakableStatement()
Returns the nearest breakable statement.

Specified by:
getNearestBreakableStatement in interface CFlowControlContextType

getNearestContinuableStatement

public JStatement getNearestContinuableStatement()
Returns the nearest continuable statement.

Specified by:
getNearestContinuableStatement in interface CFlowControlContextType

getFlowControlContext

public CFlowControlContextType getFlowControlContext()
Returns the nearest control flow context (where control flow information is stored.)

Specified by:
getFlowControlContext in interface CFlowControlContextType
Overrides:
getFlowControlContext in class JmlContext
Returns:
the nearest parent of type CFlowControlContextType

initializeVariable

public void initializeVariable(VariableDescriptor varDesc)
Marks the variable with the given descriptor as definitely assigned to in this context.

Specified by:
initializeVariable in interface CFlowControlContextType

isVarDefinitelyAssigned

public boolean isVarDefinitelyAssigned(int pos)
Indicates whether the variable in the given position is definitely assigned to in this context.

Specified by:
isVarDefinitelyAssigned in interface CFlowControlContextType

isVarDefinitelyUnassigned

public boolean isVarDefinitelyUnassigned(int pos)
Indicates whether the variable in the given position is definitely unassigned to in this context.

Specified by:
isVarDefinitelyUnassigned in interface CFlowControlContextType
Parameters:
pos - stack position
Returns:
true iff the variable is definitely unassigned

replaceFieldInfoUpTo

public void replaceFieldInfoUpTo(int pos,
                                 CVariableInfoTable replacement)
Replaces the local field info for fields in positions 0 up to pos with the info in replacement.

Specified by:
replaceFieldInfoUpTo in interface CFlowControlContextType
Overrides:
replaceFieldInfoUpTo in class JmlContext

replaceVariableInfoUpTo

public void replaceVariableInfoUpTo(int pos,
                                    CVariableInfoTable replacement)
Replaces the local variable info in positions 0 up to pos with the info in replacement.

Specified by:
replaceVariableInfoUpTo in interface CFlowControlContextType

initializeField

public void initializeField(VariableDescriptor varDesc)
Marks the field with the given descriptor as definitely assigned to in this context.

Specified by:
initializeField in interface CFlowControlContextType
Overrides:
initializeField in class JmlContext

isFieldDefinitelyAssigned

public boolean isFieldDefinitelyAssigned(int pos)
Indicates whether the field in the given position is definitely assigned to in this context.

Specified by:
isFieldDefinitelyAssigned in interface CFlowControlContextType
Overrides:
isFieldDefinitelyAssigned in class JmlContext

addLocalClass

public void addLocalClass(CClass clazz)
                   throws UnpositionedError
Adds to this context a class declared via a type declaration statement.

Specified by:
addLocalClass in interface CFlowControlContextType
Parameters:
clazz - the clazz to add
Throws:
UnpositionedError - if duplicate class exists in this lexical context

getContextNullity

protected CContextNullity getContextNullity()
Overrides:
getContextNullity in class JmlContext

isFANonNull

public boolean isFANonNull(Object expr)
Indicates whether expr (or member) is conditionally NonNull is this context.

Specified by:
isFANonNull in interface CContextType
Overrides:
isFANonNull in class JmlContext

getFANonNulls

public Object[] getFANonNulls()
returns the JPhyla that are known to be non-null in this context.

Specified by:
getFANonNulls in interface CContextType
Overrides:
getFANonNulls in class JmlContext

getFANulls

public Object[] getFANulls()
Specified by:
getFANulls in interface CContextType
Overrides:
getFANulls in class JmlContext

addFANonNull

public void addFANonNull(Object expr)
Mark expr (or member) as NonNull in this context

Specified by:
addFANonNull in interface CContextType
Overrides:
addFANonNull in class JmlContext

addFANull

public void addFANull(Object expr)
Specified by:
addFANull in interface CContextType
Overrides:
addFANull in class JmlContext

removeFANonNull

public void removeFANonNull(Object expr)
Specified by:
removeFANonNull in interface CContextType
Overrides:
removeFANonNull in class JmlContext

removeAllFANullity

public void removeAllFANullity()
Specified by:
removeAllFANullity in interface CContextType
Overrides:
removeAllFANullity in class JmlContext

addFANonNulls

public void addFANonNulls(Object[] exprs)
adds exprs (or members) as NonNull in this context

Specified by:
addFANonNulls in interface CContextType
Overrides:
addFANonNulls in class JmlContext

addFANulls

public void addFANulls(Object[] exprs)
Specified by:
addFANulls in interface CContextType
Overrides:
addFANulls in class JmlContext

mergeNullityInfo

public void mergeNullityInfo(CContextType other)
Merge the list of guarded nulls in this context with that of the given context. This is done by taking a union of the two sets.

Specified by:
mergeNullityInfo in interface CContextType
Overrides:
mergeNullityInfo in class JmlContext

adoptNullityInfo

public void adoptNullityInfo(CContextType other)
Specified by:
adoptNullityInfo in interface CContextType
Overrides:
adoptNullityInfo in class JmlContext

dumpNonNulls

public void dumpNonNulls(String msg)
Specified by:
dumpNonNulls in interface CContextType
Overrides:
dumpNonNulls in class JmlContext

lookupClass

public CClass lookupClass(String name)
                   throws UnpositionedError
Searches for a class with the given simple name according the procedure in JLS2 6.5.5. This method checks the first bullet point of that section: "If the simple type name occurs within the scope of a visible local class declaration with that name, then the simple type name denotes that local class type." If no match is found, then this method calls to the surrounding context to check the remaining bullet points.

Specified by:
lookupClass in interface CFlowControlContextType
Overrides:
lookupClass in class JmlContext
Parameters:
name - the class name, without qualifiers
Returns:
the class if found, null otherwise
Throws:
UnpositionedError - if search fails

lookupLocalVariable

public JLocalVariable lookupLocalVariable(String ident)
Returns the variable referred to by the given name in this context, recursing to surrounding contexts as appropriate. If no variable of the given name is found then null is returned.

Specified by:
lookupLocalVariable in interface CContextType
Overrides:
lookupLocalVariable in class JmlContext
Parameters:
ident - the name of the variable
Returns:
a variable from an ident in current context

declaredOutsideOfLoop

public boolean declaredOutsideOfLoop(JLocalVariable var)
Indicates whether this context is enclosed in a loop and the given variable is declared outside the inner-most loop context.

Specified by:
declaredOutsideOfLoop in interface CContextType
Overrides:
declaredOutsideOfLoop in class JmlContext

declares

public boolean declares(JLocalVariable var)
Returns true if the given local variable is declared exactly in this context, i.e., it is not declared in an outer context.

Specified by:
declares in interface CContextType
Overrides:
declares in class JmlContext

addThrowable

public void addThrowable(CThrowableInfo throwable)
Description copied from interface: CFlowControlContextType
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 CFlowControlContextType
Parameters:
throwable - the type of the new throwable

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.