org.jmlspecs.checker
Class JmlContext

java.lang.Object
  org.multijava.util.Utils
      org.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
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_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, 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_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, 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, 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_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
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.
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
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	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
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	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

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

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

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()