JML

org.jmlspecs.checker
Class JmlBinarySourceClass

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.mjc.CMember
          extended byorg.multijava.mjc.CClass
              extended byorg.multijava.mjc.CSourceClass
                  extended byorg.jmlspecs.checker.JmlSourceClass
                      extended byorg.jmlspecs.checker.JmlBinarySourceClass
All Implemented Interfaces:
Cloneable, CMemberHost, Comparable, Constants, Constants, Constants, org.jmlspecs.util.classfile.JmlModifiable

public class JmlBinarySourceClass
extends JmlSourceClass

This class represents a class read from a *.class file. It is primarily just a data structure, apart from methods for generating the qualified name and for determining whether the member is accessible from some class.


Nested Class Summary
 
Nested classes inherited from class org.multijava.mjc.CClass
CClass.NoDupStrategy, CClass.Observer
 
Field Summary
private  boolean isAnonymous
          Indicates whether the class represented by this is anonymous.
private  boolean isMember
          Indicates whether the class represented by this is a member type.
 
Fields inherited from class org.jmlspecs.checker.JmlSourceClass
levelNumber, refinedSourceClass, refiningSourceClass
 
Fields inherited from class org.multijava.mjc.CSourceClass
 
Fields inherited from class org.multijava.mjc.CClass
CLS_UNDEFINED, dispClassTypes, methods
 
Fields inherited from class org.multijava.mjc.CMember
 
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
JmlBinarySourceClass(Main compiler, ClassInfo classInfo, File file)
          Constructs a class export from file.
 
Method Summary
private static CClassType[] buildExceptionTypes(MethodInfo methodInfo)
           
protected static CClass buildReceiverClass(CClass host, MethodInfo methodInfo)
           
private static CMemberHost getHostFrom(String clazz)
          Returns the host for the class named by the argument.
private static CClass getOuterClassFrom(String clazz)
          Returns the surrounding class for the inner class named by the argument.
 boolean isAnonymous()
           
 boolean isMember()
          Indicates whether the class represented by this is a member type.
protected  CClassType[] loadInterfaces(String[] interfaces)
          Loads the interfaces specified by the Strings in the argument array (whether from other declarations in this compilation pass or from *.class files.)
protected  void processInnerClassesAttr(InnerClassInfo[] inners)
          Loads the inner classes specified by the info in the argument array (whether from other declarations in this compilation pass or from *.class files.)
 
Methods inherited from class org.jmlspecs.checker.JmlSourceClass
accumLocalInternalMethods, accumMostSpecificMethods, checkFileNameAndSuffix, classesRefined, compareLevelsTo, compareTo, computeSuffixNumber, createClassInfo, descendsFrom, finishSymbolTable, finishSymbolTableForInterfaces, genFields, genMethods, getAbstractMethods, getAST, getDeclaredField, getDeclaredInnerType, getInterfaceMethods, getLevelNumber, getMostRefined, getRefinedType, getRefiningType, getSuperClass, inJavaFile, innerClassesForAttribute, inSpecFile, isAccessibleFrom, isEffectivelyModel, isFieldRedefined, isFinishedPreProcessing, isGhost, isLocalTo, isModel, isMoreRefinedThan, isRefined, isRefiningType, jmlAccess, lookupFieldHelper, lookupJMLMethodName, lookupJMLMethodsWithSameSig, lookupRefinedField, lookupRefinedInnerType, lookupRefinedMethod, refines, setAST, setFinishedPreProcessing, setRefinedType
 
Methods inherited from class org.multijava.mjc.CSourceClass
addRMJMethodAnnotation, appendCustomAttributes, genCode, genConstructorArray, genInit, genSyntheticParams, genSyntheticParamsForExplicitThis, getOuterLocalAccess, getSyntheticParamsForExplicitSuper, getUniverseVersion, hasUniverseRuntimeSupport, initializerChecked, lookupClass, lookupMethodOrSet, nextDispatcherNumber, rmjAnnotate, setCheckedMembers, setInitializerChecked
 
Methods inherited from class org.multijava.mjc.CClass
accumLocalExtAndInheritedMethods, addBridgeMethod, addField, addRedirector, augmentWithMethod, checkBridgeMethod, checkTypeVariables, close, collectAbstractMethods, collectInterfaceMethods, descendsFrom, directlyVisibleTypes, equals, fields, fieldsForCodeGen, findGetterMethod, findOrCreateGetterMethod, findOrCreateSetterMethod, genClassFile, genCustomAttributes, genGenericFunctions, genInnerInfo, genInners, genInterfaces, getAllInheritableMethods, getAllInheritedMethods, getAllMethods, getCClass, getCompiler, getFieldCount, getGenericSignature, getIdentFrom, getInnerClasses, getInterfaces, getNextAccessName, getNextSyntheticIndex, getSubstitution, getSubstitution, getSuperSubstitution, getSuperType, getterOrSetterMethodFor, getType, getTypeVariables, hashCode, hasProtectedVisibilityIn, hasSyntheticOuterThis, initSession, isAbstract, isClass, isCompilationUnit, isDefinedInside, isGenericClass, isInnerClass, isInterface, isNestedType, lookupAllMethods, lookupField, lookupMethod, lookupMethodsSpecializedByMethod, lookupMSAMethod, lookupOverloadedMethod, lookupSuperField, lookupTopConcreteMethod, lookupTypeVariable, memberNeedsPrivilegedAccess, methods, methodsForCodeGen, nestedDescendsFrom, noAssertionsYet, noPossiblyInnerAssertionsYet, packageName, protoMethods, qualifiedName, register, registerNestedType, rmjAnnotate, setAssertHelperMethod, setAssertStaticInitMethod, setCheckedInterfaces, setCheckedMembers, setInnerClasses, setSuperClass, setTypeVariables, sourceFile, syntheticOuterThisInaccessible, toString, wrapSuperCallTo
 
Methods inherited from class org.multijava.mjc.CMember
access, addModifiers, deprecated, getCCompilationUnit, getField, getIdent, getJavaName, getMethod, getOwnerName, getQualNameWithSeparator, hasDefaultAccess, host, ident, isDeclaredNonNull, isDeprecated, isFinal, isPrivate, isProtected, isPublic, isStatic, modifiers, owner, setModifiers
 
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, wait, wait, wait
 
Methods inherited from interface org.multijava.mjc.CMemberHost
host, ident
 

Field Detail

isAnonymous

private boolean isAnonymous
Indicates whether the class represented by this is anonymous.


isMember

private boolean isMember
Indicates whether the class represented by this is a member type. A member type is a type that is declared inside another type but that is not an anonymous class or a local type declaration.

Constructor Detail

JmlBinarySourceClass

public JmlBinarySourceClass(Main compiler,
                            ClassInfo classInfo,
                            File file)
Constructs a class export from file.

Method Detail

buildReceiverClass

protected static CClass buildReceiverClass(CClass host,
                                           MethodInfo methodInfo)

buildExceptionTypes

private static CClassType[] buildExceptionTypes(MethodInfo methodInfo)

loadInterfaces

protected CClassType[] loadInterfaces(String[] interfaces)
Loads the interfaces specified by the Strings in the argument array (whether from other declarations in this compilation pass or from *.class files.)

Parameters:
interfaces - the names of the interfaces to load
Returns:
an array of the types of the interfaces

processInnerClassesAttr

protected final void processInnerClassesAttr(InnerClassInfo[] inners)
Loads the inner classes specified by the info in the argument array (whether from other declarations in this compilation pass or from *.class files.)

Parameters:
inners - the info of the inner classes to load

getOuterClassFrom

private static CClass getOuterClassFrom(String clazz)
Returns the surrounding class for the inner class named by the argument.

Parameters:
clazz - the name of the inner class
Returns:
the class representing the surrounding class

getHostFrom

private static CMemberHost getHostFrom(String clazz)
Returns the host for the class named by the argument.

Parameters:
clazz - the name of the class
Returns:
the host for the named class

isAnonymous

public boolean isAnonymous()
Overrides:
isAnonymous in class CSourceClass
Returns:
true if this class is anonymous

isMember

public boolean isMember()
Indicates whether the class represented by this is a member type. A member type is a type that is declared inside another type but that is not an anonymous class or a local type declaration.

Overrides:
isMember in class CSourceClass

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.