JML

org.jmlspecs.checker
Class JmlCompilationUnitContext

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

public class JmlCompilationUnitContext
extends JmlContext
implements CCompilationUnitContextType, Constants

This class represents the context for a compilation unit during checking passes (checkInterface, checkInitializers, typecheck).

See Also:
CContextType

Field Summary
private  Main.PTMode mode
           
 
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) JmlCompilationUnitContext(Main compiler, CCompilationUnit cunit)
          Construct a compilation unit context.
 
Method Summary
 MJMathMode arithmeticMode()
          Indicates the integral arithmetic mode that should be used.
 void classToGenerate(CSourceClass clazz)
          Adds a class to generate
 CBinaryClassContext createBinaryClassContext(CBinaryClass clazz)
           
 boolean equals(Object o)
          Indicates whether this is equal to a given object.
 CVariableState fieldInfo(int pos)
          Fields cannot be declared in the context of a compilation unit (yet), consequently we do not expect to invoke this method on a compilation unit context.
 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()
          getClass
 CCompilationUnitContextType getCompilationUnit()
          Returns the compilation unit context for this context.
 Main getCompiler()
          Gets the compiler
 CFlowControlContextType getFlowControlContext()
          Returns the nearest control flow context (where control flow information is stored.)
 CMethodContextType getMethodContext()
          getMethod
 CContextType getParentContext()
          getParentContext
 int hashCode()
          Returns the hash code for this, equivalent to this.cunit.hashCode().
 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, CExpressionContextType context)
          searches for a field with the given identifier
 JLocalVariable lookupLocalVariable(String ident)
          Finds the variable with the given identifier in this context.
 CMethod lookupMethod(String name, CType[] params, CClassContextType context)
          Searches for the most specific method applicable to the given identifier and argument type tuple, in the current context.
 CMethodSet lookupMethodOrSet(String name, CType[] params, CClassContextType context)
          Searches for the most specific method(s) applicable to the given identifier and argument type tuple, in the current context.
 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.
 Main.PTMode mode()
           
 void registerVisibleMethod(CMethod method)
          Registers that a declaration of the given method occurs within the compilation unit.
 void registerVisibleType(CType type)
          Registers that a reference to the given type occurs within the compilation unit.
 void reportTrouble(Exception trouble)
          Adds a trouble into the list and eats it.
 void resolveMaybeExtMethodRef(String ident)
          Searches for any imported external generic functions.
 void setMode(Main.PTMode m)
           
 
Methods inherited from class org.jmlspecs.checker.JmlContext
addFANonNull, addFANonNulls, addFANull, addFANulls, adoptNullityInfo, catchUp, check, check, check, check, createClassContext, createDummyContext, createExtMethodContext, createInterfaceContext, declaredOutsideOfLoop, declares, dumpNonNulls, enterSpecScope, exitSpecScope, fail, fail, fail, getCMethod, getContextNullity, getFANonNulls, getFANulls, getHostClass, initializeField, inSpecScope, isBeforeSuperConstructorCall, isFANonNull, isFieldDefinitelyAssigned, isInConstructor, isInInitializer, isInLoop, isPure, isStatic, lookupField, lookupMethod, lookupMethodOrSet, lookupOuterField, lookupTypeVariable, mergeNullityInfo, modUtil, registerGFDecl, removeAllFANullity, removeFANonNull, replaceFieldInfoUpTo
 
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, finalize, getClass, notify, notifyAll, toString, wait, wait, wait
 
Methods inherited from interface org.multijava.mjc.CContextType
addFANonNull, addFANonNulls, addFANull, addFANulls, adoptNullityInfo, catchUp, check, check, check, check, createClassContext, createExtMethodContext, createInterfaceContext, declaredOutsideOfLoop, declares, dumpNonNulls, fail, fail, getCMethod, getFANonNulls, getFANulls, initializeField, isBeforeSuperConstructorCall, isFANonNull, isFieldDefinitelyAssigned, isInConstructor, isInInitializer, isInLoop, isPure, isStatic, lookupField, lookupMethod, lookupMethodOrSet, lookupOuterField, lookupTypeVariable, mergeNullityInfo, modUtil, registerGFDecl, removeAllFANullity, removeFANonNull, replaceFieldInfoUpTo
 

Field Detail

mode

private Main.PTMode mode
Constructor Detail

JmlCompilationUnitContext

JmlCompilationUnitContext(Main compiler,
                          CCompilationUnit cunit)
Construct a compilation unit context.

 requires compiler != null && cunit != null;
 ensures delegee != null && (delegee instanceof CCompilationUnitContext);
 

Method Detail

fieldInfo

public CVariableState fieldInfo(int pos)
Fields cannot be declared in the context of a compilation unit (yet), consequently we do not expect to invoke this method on a compilation unit context.

Specified by:
fieldInfo in interface CCompilationUnitContextType
Throws:
UnsupportedOperationException

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 CCompilationUnitContextType
Overrides:
lookupClass in class JmlContext
Parameters:
name - the class name, without qualifiers
Returns:
the class if found, null otherwise
Throws:
UnpositionedError - if search fails

lookupMethod

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

Specified by:
lookupMethod in interface CCompilationUnitContextType
Overrides:
lookupMethod in class JmlContext
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,
                                    CClassContextType context)
                             throws UnpositionedError
Searches for the most specific method(s) applicable to the given identifier and argument type tuple, in the current context.

Specified by:
lookupMethodOrSet in interface CCompilationUnitContextType
Overrides:
lookupMethodOrSet in class JmlContext
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,
                                  CExpressionContextType context)
                           throws UnpositionedError
searches for a field with the given identifier

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

lookupLocalVariable

public JLocalVariable lookupLocalVariable(String ident)
Finds the variable with the given identifier in this context.

Specified by:
lookupLocalVariable in interface CContextType
Overrides:
lookupLocalVariable in class JmlContext
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 CCompilationUnitContextType
Overrides:
lookupOuterLocalVariable in class JmlContext
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,
                                       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 CCompilationUnitContextType
Overrides:
lookupOuterField in class JmlContext
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

resolveMaybeExtMethodRef

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

Specified by:
resolveMaybeExtMethodRef in interface CCompilationUnitContextType
Overrides:
resolveMaybeExtMethodRef in class JmlContext
Parameters:
ident - the name of the generic function to search for

registerVisibleMethod

public void registerVisibleMethod(CMethod method)
Registers that a declaration of the given method occurs within the compilation unit.

Specified by:
registerVisibleMethod in interface CCompilationUnitContextType
Overrides:
registerVisibleMethod in class JmlContext

registerVisibleType

public void registerVisibleType(CType type)
Registers that a reference to the given type occurs within the compilation unit.

Specified by:
registerVisibleType in interface CCompilationUnitContextType
Overrides:
registerVisibleType in class JmlContext

getParentContext

public CContextType getParentContext()
getParentContext

Specified by:
getParentContext in interface CCompilationUnitContextType
Overrides:
getParentContext in class JmlContext
Returns:
the parent

getClassContext

public CClassContextType getClassContext()
getClass

Specified by:
getClassContext in interface CCompilationUnitContextType
Overrides:
getClassContext in class JmlContext
Returns:
the near parent of type CClassContextType

getMethodContext

public CMethodContextType getMethodContext()
getMethod

Specified by:
getMethodContext in interface CCompilationUnitContextType
Overrides:
getMethodContext in class JmlContext
Returns:
the near parent of type CMethodContextType

getCompilationUnit

public CCompilationUnitContextType getCompilationUnit()
Description copied from interface: CContextType
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 CCompilationUnitContextType
Overrides:
getCompilationUnit in class JmlContext
Returns:
the compilation unit

getFlowControlContext

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

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

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 CCompilationUnitContextType
Overrides:
findNearestHost in class JmlContext
Returns:
the nearest parent that can be coerced to a CMemberHost, i.e., this.cunit

createBinaryClassContext

public CBinaryClassContext createBinaryClassContext(CBinaryClass clazz)
Specified by:
createBinaryClassContext in interface CCompilationUnitContextType

reportTrouble

public void reportTrouble(Exception trouble)
Adds a trouble into the list and eats it. This method should be called after a try catch block after catching exception or directly without exception thrown.o

Specified by:
reportTrouble in interface CCompilationUnitContextType
Overrides:
reportTrouble in class JmlContext
Parameters:
trouble - the trouble

getCompiler

public Main getCompiler()
Gets the compiler

Specified by:
getCompiler in interface CCompilationUnitContextType
Overrides:
getCompiler in class JmlContext

classToGenerate

public void classToGenerate(CSourceClass clazz)
Adds a class to generate

Specified by:
classToGenerate in interface CCompilationUnitContextType
Overrides:
classToGenerate in class JmlContext

equals

public boolean equals(Object o)
Indicates whether this is equal to a given object.

Specified by:
equals in interface CCompilationUnitContextType
Overrides:
equals in class Object
Parameters:
o - the object to compare against
Returns:
true iff o is another CCompilationUnitContextType formed around an identical (i.e., ==) CCompilationUnit

hashCode

public int hashCode()
Returns the hash code for this, equivalent to this.cunit.hashCode().

Specified by:
hashCode in interface CCompilationUnitContextType
Overrides:
hashCode in class Object
Returns:
the hash code for this

mode

public Main.PTMode mode()

setMode

public void setMode(Main.PTMode m)

arithmeticMode

public MJMathMode arithmeticMode()
Description copied from interface: CContextType
Indicates the integral arithmetic mode that should be used.

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

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.