JML

org.jmlspecs.checker
Class JmlContext

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.checker.JmlContext
All Implemented Interfaces:
CContextType, Cloneable, Constants, Constants, Constants
Direct Known Subclasses:
JmlClassContext, JmlCompilationUnitContext, JmlExpressionContext, JmlFlowControlContext, JmlMethodContext

public abstract class JmlContext
extends Utils
implements CContextType, Constants

Descendents of this class represent local contexts during checking passes (checkInterface, checkInitializers, typecheck). The context classes follow the control flow and maintain information about variables (initialized, used, allocated) and exceptions (thrown, caught). They also verify that a context is still reachable. The contexts are used for name resolution (JLS2, 6 and 14.4), checking for unreachable statements (JLS2 14.20), checking for definite assignment (JLS2, 16), and for checking for proper subclassing and overriding (JLS2, 8).

The contexts are hierarchical. To wit, a compilation unit context is created and passed to the method that checks a class. This method creates a class context by passing the compilation unit context to the CClassContext constructor. When checking methods of the class the CClassContext instance is passed to the CMethodContext constructor. These context classes are stored in fields of the AST nodes.

During typechecking the context hierarchy is mutated in a way that mimics the actual run-time control flow. For example, variable declarations cause the context to be mutated to record the variable's name and type. Assignment to a variable causes the context to be mutated to record that the variable is definitely assigned. Reference a variable's value triggers a check that the variable has been definitely assigned.


Field Summary
private  CContextNullity contextNullity
           
protected  CCompilationUnitContextType cunit
           
protected  CContext delegee
           
protected  CContextType parent
          The parent context.
private static int specScopeCounter
          number of nested spec scopes
 
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) JmlContext()
          Constructs a new context.
protected JmlContext(CContextType parent)
          Construct a block context, it supports local variable allocation throw statement and return statement
 
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 adoptNullityInfo(CContextType other)
           
 MJMathMode arithmeticMode()
          Indicates the integral arithmetic mode that should be used.
 void catchUp(JTypeDeclarationType decl)
          Calls back to the compiler for this context and requests that the compiler catch-up decl to the same pass as the currently active task.
 boolean check(boolean expr, MessageDescription mess)
          Verifies an expression and if false signals an error.
 boolean check(boolean expr, MessageDescription mess, Object param1)
          Verifies an expression and if false signals an error.
 boolean check(boolean expr, MessageDescription mess, Object param1, Object param2)
          Verifies an expression and if false signals an error.
 boolean check(boolean expr, MessageDescription mess, Object[] params)
           
 void classToGenerate(CSourceClass clazz)
          Adds a source class to be generated
 CClassContextType createClassContext(CClass self)
          Creates a class context with this context as its parent.
static CFlowControlContextType createDummyContext(JmlSourceClass self)
           
 CExtMethodContext createExtMethodContext(CSourceClass host, CClass owner)
          Create a new child of this context representing the context in which an external method declaration is typechecked.
 CInterfaceContextType createInterfaceContext(CClass self)
          Creates an interface context with this context as its parent.
 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)
           
static void enterSpecScope()
          Enters a new JML specification scope.
static void exitSpecScope()
          Exits the current JML specification scope.
 void fail(MessageDescription mess, Object params)
           
 void fail(MessageDescription mess, Object param1, Object param2)
          Generates an UnpositionedError with a given message.
 void fail(MessageDescription mess, Object[] params)
          Generates an UnpositionedError with a given message.
 CMemberHost findNearestHost()
          Returns the signature of the nearest lexically enclosing context that can host member declarations (i.e., a CClass or a CCompilationUnit).
 CClassContextType getClassContext()
          Returns the class context for this context.
 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.
 CCompilationUnitContextType getCompilationUnit()
          Returns the compilation unit context for this context.
 Main getCompiler()
          Gets the compiler for this context
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.)
 CClass getHostClass()
          Returns the signature of the class declaration in which this context is enclosed, or null if this context is not enclosed in a class declaration.
 CMethodContextType getMethodContext()
          Returns the method context for this context.
 CContextType getParentContext()
          Returns the parent context for this context
 void initializeField(VariableDescriptor varDesc)
          Marks the field with the given descriptor as definitely assigned to in this context.
static boolean inSpecScope()
          Returns true if currently in JML specification scope.
 boolean isBeforeSuperConstructorCall()
          Indicates whether this context is enclosed in a constructor and occurs before the constructor has invoked the superclass constructor.
 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 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 isInLoop()
          Indicates whether this context is enclosed in a loop.
 boolean isPure()
          Indicates whether this context is "pure".
 boolean isStatic()
          Indicates whether this context is "static".
 CClass lookupClass(String name)
          Searches for a class with the given simple name according the procedure in JLS2 6.5.5.
 CFieldAccessor lookupField(String ident)
          searches for a field with the given identifier
 CFieldAccessor lookupField(String ident, CExpressionContextType context)
          searches for a field with the given identifier
 JLocalVariable lookupLocalVariable(String ident)
          searches for a local variable with the given identifier
 CMethod lookupMethod(String name, CType[] params)
          Searches for the most specific method in the current context that is applicable to the given identifier and argument type tuple.
 CMethod lookupMethod(String name, CType[] params, CClassContextType context)
          Searches for the most specific method in the current context that is applicable to the given identifier and argument type tuple.
 CMethodSet lookupMethodOrSet(String name, CType[] params)
          Searches for the most specific method(s) in the current context that is applicable to the given identifier and argument type tuple.
 CMethodSet lookupMethodOrSet(String name, CType[] params, CClassContextType context)
          Searches for the most specific method(s) in the current context that is applicable to the given identifier and argument type tuple.
 CFieldAccessor lookupOuterField(String ident)
          Searches for a field of the given name in the context surrounding the current lexical contour.
 CFieldAccessor lookupOuterField(String ident, CExpressionContextType context)
          Searches for a field of the given name in the context surrounding the current lexical contour.
 JExpression lookupOuterLocalVariable(TokenReference ref, String ident)
          Finds a local variable with the given name that appears outside the current lexical contour.
 CTypeVariable lookupTypeVariable(String ident)
          search for type variable that are accessible
 void mergeNullityInfo(CContextType other)
          Merge the list of guarded nulls in this context with that of the given context.
 ModifierUtility modUtil()
          Returns the modifier utility for this.
 void registerGFDecl(String methodIdent, CGenericFunctionCollection coll)
          Registers the declaration of an external generic function in this context.
 void registerVisibleMethod(CMethod method)
          Registers with the surrounding context that a declaration of the given method occurs in this context.
 void registerVisibleType(CType type)
          Registers with the surrounding context that a reference to the given type occurs in this context.
 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 reportTrouble(Exception trouble)
          Reports the given error and the "swallows" it, allowing compilation to continue.
 void resolveMaybeExtMethodRef(String ident)
          Searches for any imported external generic functions.
 
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

specScopeCounter

private static int specScopeCounter
number of nested spec scopes


parent

protected CContextType parent
The parent context.

 invariant parent != null ==> parent instanceof JmlContext;
 


cunit

protected CCompilationUnitContextType cunit

delegee

protected CContext delegee

contextNullity

private final CContextNullity contextNullity
Constructor Detail

JmlContext

JmlContext()
Constructs a new context.


JmlContext

protected JmlContext(CContextType parent)
Construct a block context, it supports local variable allocation throw statement and return statement

Parameters:
parent - the parent context, it must be different than null except if called by the top level
Method Detail

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.

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

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
Throws:
UnpositionedError

lookupMethod

public CMethod lookupMethod(String name,
                            CType[] params)
                     throws UnpositionedError
Searches for the most specific method in the current context that is applicable to the given identifier and argument type tuple.

Specified by:
lookupMethod in interface CContextType
Parameters:
name - method name
params - method parameter types
Throws:
UnpositionedError - if the result is ambiguous

lookupMethod

public CMethod lookupMethod(String name,
                            CType[] params,
                            CClassContextType context)
                     throws UnpositionedError
Searches for the most specific method in the current context that is applicable to the given identifier and argument type tuple.

Specified by:
lookupMethod in interface CContextType
Parameters:
name - method name
params - method parameter types
context - the context of the class containing the method call
Throws:
UnpositionedError - if the result is ambiguous

lookupMethodOrSet

public CMethodSet lookupMethodOrSet(String name,
                                    CType[] params)
                             throws UnpositionedError
Searches for the most specific method(s) in the current context that is applicable to the given identifier and argument type tuple.

Specified by:
lookupMethodOrSet in interface CContextType
Parameters:
name - method name
params - method parameter types
Throws:
UnpositionedError - if the result is ambiguous

lookupMethodOrSet

public CMethodSet lookupMethodOrSet(String name,
                                    CType[] params,
                                    CClassContextType context)
                             throws UnpositionedError
Searches for the most specific method(s) in the current context that is applicable to the given identifier and argument type tuple.

Specified by:
lookupMethodOrSet in interface CContextType
Parameters:
name - method name
params - method parameter types
context - the context of the class containing the method call
Throws:
UnpositionedError - if the result is ambiguous

lookupField

public CFieldAccessor lookupField(String ident)
                           throws UnpositionedError
searches for a field with the given identifier

Specified by:
lookupField in interface CContextType
Returns:
a field from an ident in current context
Throws:
UnpositionedError - this error will be positioned soon

lookupField

public CFieldAccessor lookupField(String ident,
                                  CExpressionContextType context)
                           throws UnpositionedError
searches for a field with the given identifier

Specified by:
lookupField in interface CContextType
Returns:
a field from an ident in current context
Throws:
UnpositionedError - this error will be positioned soon

lookupLocalVariable

public JLocalVariable lookupLocalVariable(String ident)
searches for a local variable with the given identifier

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

lookupOuterLocalVariable

public JExpression lookupOuterLocalVariable(TokenReference ref,
                                            String ident)
Finds a local variable with the given name that appears outside the current lexical contour.

Specified by:
lookupOuterLocalVariable in interface CContextType
Parameters:
ref - a token reference used to build a new JOuterLocalVariableExpression
ident - the name of the outer variable
Returns:
a variable from an ident in the surrounding context, or null if not found

lookupOuterField

public CFieldAccessor lookupOuterField(String ident)
                                throws UnpositionedError
Searches for a field of the given name in the context surrounding the current lexical contour.

Specified by:
lookupOuterField in interface CContextType
Parameters:
ident - the name of the field
Returns:
a variable from a field in the surrounding context, or null if none is found
Throws:
UnpositionedError - this error will be positioned soon

lookupOuterField

public CFieldAccessor lookupOuterField(String ident,
                                       CExpressionContextType context)
                                throws UnpositionedError
Searches for a field of the given name in the context surrounding the current lexical contour.

Specified by:
lookupOuterField in interface CContextType
Parameters:
ident - the name of the field
context - the context of the field access
Returns:
a variable from a field in the surrounding context, or null if none is found
Throws:
UnpositionedError - this error will be positioned soon

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 CContextType

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 CContextType

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 CContextType

getParentContext

public CContextType getParentContext()
Returns the parent context for this context

Specified by:
getParentContext in interface CContextType
Returns:
the parent

getCompilationUnit

public CCompilationUnitContextType getCompilationUnit()
Returns the compilation unit context for this context. This only makes sense for contexts that do not themselves represent compilation units. I.e., in classes that represent compilation unit context this should be overridden.

Specified by:
getCompilationUnit in interface CContextType
Returns:
the compilation unit

getClassContext

public CClassContextType getClassContext()
Returns the class context for this context. This only makes sense for contexts that can appear inside classes. I.e., This should be overridden in classes representing other sorts of contexts.

Specified by:
getClassContext in interface CContextType
Returns:
the nearest parent of type CClassContextType.

getMethodContext

public CMethodContextType getMethodContext()
Returns the method context for this context. This only makes sense for contexts that can appear inside methods. I.e., This should be overridden in classes representing other sorts of contexts.

Specified by:
getMethodContext in interface CContextType
Returns:
the nearest parent of type CMethodContextType.

getFlowControlContext

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

Specified by:
getFlowControlContext in interface CContextType
Returns:
the nearest parent of type CFlowControlContextType

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 CContextType

getHostClass

public CClass getHostClass()
Returns the signature of the class declaration in which this context is enclosed, or null if this context is not enclosed in a class declaration.


findNearestHost

public CMemberHost findNearestHost()
Returns the signature of the nearest lexically enclosing context that can host member declarations (i.e., a CClass or a CCompilationUnit). Used for access checks, this is slightly different than getHostClass(). The later method returns an anchor class signature for external methods, which is useful in code generation and in typechecking external method bodies. On the other hand, this method returns a CCompilationUnit for external methods, which is useful in checking access between two differently named generic functions declared in the same compilation unit. !FIXME! It may be possible to eliminate this method and just use getHostClass now that private external methods are duplciated in every anchor.

Specified by:
findNearestHost in interface CContextType
Returns:
the nearest parent that can be coerced to a CMemberHost

createClassContext

public CClassContextType createClassContext(CClass self)
Creates a class context with this context as its parent.

Specified by:
createClassContext in interface CContextType
Parameters:
self - the corresponding class

createInterfaceContext

public CInterfaceContextType createInterfaceContext(CClass self)
Creates an interface context with this context as its parent.

Specified by:
createInterfaceContext in interface CContextType
Parameters:
self - the corresponding interface signature

createExtMethodContext

public CExtMethodContext createExtMethodContext(CSourceClass host,
                                                CClass owner)
Create a new child of this context representing the context in which an external method declaration is typechecked.

Specified by:
createExtMethodContext in interface CContextType
Parameters:
host - the host class
owner - the receiver class

getContextNullity

protected CContextNullity getContextNullity()

isFANonNull

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

Specified by:
isFANonNull in interface CContextType

getFANonNulls

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

Specified by:
getFANonNulls in interface CContextType

getFANulls

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

addFANonNull

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

Specified by:
addFANonNull in interface CContextType

addFANull

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

removeFANonNull

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

removeAllFANullity

public void removeAllFANullity()
Specified by:
removeAllFANullity in interface CContextType

addFANonNulls

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

Specified by:
addFANonNulls in interface CContextType

addFANulls

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

mergeNullityInfo

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

Specified by:
mergeNullityInfo in interface CContextType

adoptNullityInfo

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

dumpNonNulls

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

classToGenerate

public void classToGenerate(CSourceClass clazz)
Adds a source class to be generated

Specified by:
classToGenerate in interface CContextType
Parameters:
clazz - the class to be generated

resolveMaybeExtMethodRef

public void resolveMaybeExtMethodRef(String ident)
Searches for any imported external generic functions.

Specified by:
resolveMaybeExtMethodRef in interface CContextType
Parameters:
ident - the name of the generic function to search for

registerGFDecl

public void registerGFDecl(String methodIdent,
                           CGenericFunctionCollection coll)
Registers the declaration of an external generic function in this context.

Specified by:
registerGFDecl in interface CContextType

registerVisibleMethod

public void registerVisibleMethod(CMethod method)
Registers with the surrounding context that a declaration of the given method occurs in this context.

Specified by:
registerVisibleMethod in interface CContextType

registerVisibleType

public void registerVisibleType(CType type)
Registers with the surrounding context that a reference to the given type occurs in this context.

Specified by:
registerVisibleType in interface CContextType

reportTrouble

public void reportTrouble(Exception trouble)
Reports the given error and the "swallows" it, allowing compilation to continue. This method is used to report non-fatal errors; for fatal errors the exception is just thrown.

Specified by:
reportTrouble in interface CContextType
Parameters:
trouble - the error

fail

public void fail(MessageDescription mess,
                 Object param1,
                 Object param2)
          throws UnpositionedError
Generates an UnpositionedError with a given message.

Specified by:
fail in interface CContextType
Parameters:
mess - the error message
param1 - the first message parameter
param2 - the second message parameter
Returns:
never, i.e., this method always throws an exception
Throws:
UnpositionedError - the error exception

fail

public void fail(MessageDescription mess,
                 Object params)
          throws UnpositionedError
Throws:
UnpositionedError

fail

public void fail(MessageDescription mess,
                 Object[] params)
          throws UnpositionedError
Generates an UnpositionedError with a given message.

Specified by:
fail in interface CContextType
Parameters:
mess - the error message
params - the message parameters
Returns:
never, i.e., this method always throws an exception
Throws:
UnpositionedError - the error exception

check

public boolean check(boolean expr,
                     MessageDescription mess)
              throws UnpositionedError
Verifies an expression and if false signals an error.

Specified by:
check in interface CContextType
Parameters:
expr - condition to verify
mess - the message to be displayed
Returns:
true iff expr is true
Throws:
UnpositionedError - this error will be positioned soon

check

public boolean check(boolean expr,
                     MessageDescription mess,
                     Object[] params)
              throws UnpositionedError
Specified by:
check in interface CContextType
Throws:
UnpositionedError

check

public boolean check(boolean expr,
                     MessageDescription mess,
                     Object param1)
              throws UnpositionedError
Verifies an expression and if false signals an error.

Specified by:
check in interface CContextType
Parameters:
expr - condition to verify
mess - the message to be displayed
param1 - the first parameter
Returns:
true iff expr is true
Throws:
UnpositionedError - this error will be positioned soon

check

public boolean check(boolean expr,
                     MessageDescription mess,
                     Object param1,
                     Object param2)
              throws UnpositionedError
Verifies an expression and if false signals an error.

Specified by:
check in interface CContextType
Parameters:
expr - condition to verify
mess - the message to be displayed
param1 - the first parameter
param2 - the second parameter
Returns:
true iff expr is true
Throws:
UnpositionedError - this error will be positioned soon

getCompiler

public Main getCompiler()
Gets the compiler for this context

Specified by:
getCompiler in interface CContextType

modUtil

public final ModifierUtility modUtil()
Returns the modifier utility for this.

Specified by:
modUtil in interface CContextType

isInLoop

public boolean isInLoop()
Indicates whether this context is enclosed in a loop.

Specified by:
isInLoop in interface CContextType

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

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

isInInitializer

public boolean isInInitializer()
Indicates whether this context is enclosed in an instance or static initializer.

Specified by:
isInInitializer in interface CContextType

isInConstructor

public boolean isInConstructor()
Indicates whether this context is enclosed in a constructor.

Specified by:
isInConstructor in interface CContextType

isBeforeSuperConstructorCall

public boolean isBeforeSuperConstructorCall()
Indicates whether this context is enclosed in a constructor and occurs before the constructor has invoked the superclass constructor.

Specified by:
isBeforeSuperConstructorCall in interface CContextType

isStatic

public boolean isStatic()
Indicates whether this context is "static".

Specified by:
isStatic in interface CContextType
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 CContextType
Returns:
true iff this context is enclosed in a pure method.

catchUp

public void catchUp(JTypeDeclarationType decl)
Calls back to the compiler for this context and requests that the compiler catch-up decl to the same pass as the currently active task.

Specified by:
catchUp in interface CContextType

arithmeticMode

public MJMathMode arithmeticMode()
Indicates the integral arithmetic mode that should be used.

Specified by:
arithmeticMode in interface CContextType

createDummyContext

public static CFlowControlContextType createDummyContext(JmlSourceClass self)

enterSpecScope

public static void enterSpecScope()
Enters a new JML specification scope.

See Also:
exitSpecScope(), inSpecScope()

exitSpecScope

public static void exitSpecScope()
Exits the current JML specification scope.

See Also:
enterSpecScope(), inSpecScope()

inSpecScope

public static boolean inSpecScope()
Returns true if currently in JML specification scope.

See Also:
enterSpecScope(), exitSpecScope()

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.