JML

org.jmlspecs.checker
Class JmlSourceClass

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
All Implemented Interfaces:
Cloneable, CMemberHost, Comparable, Constants, Constants, Constants, org.jmlspecs.util.classfile.JmlModifiable
Direct Known Subclasses:
JmlBinarySourceClass

public class JmlSourceClass
extends CSourceClass
implements org.jmlspecs.util.classfile.JmlModifiable, Constants

A class for representing JML classes read from *.java files. 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.

See Also:
CMember

Nested Class Summary
 
Nested classes inherited from class org.multijava.mjc.CClass
CClass.NoDupStrategy, CClass.Observer
 
Field Summary
private  boolean finishedPreProcessing
           
protected  int levelNumber
          The level number is determined by the suffix of the source file.
private static CField modelField
           
protected  JmlSourceClass refinedSourceClass
          This field contains the source class of the type declaration that is refined by the current type; it is used when looking up names such as fields or classes.
protected  JmlSourceClass refiningSourceClass
           
private static int stackLevel
           
private  JmlMemberDeclaration typeAST
           
 
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
JmlSourceClass(Main compiler, CClass owner, CMemberHost host, TokenReference where, long modifiers, String ident, String qualifiedName, CTypeVariable[] typevariables, boolean isAnonymous, boolean isMember, boolean deprecated)
          Constructs a class export from source
 
Method Summary
protected  void accumLocalInternalMethods(String name, CClass.NoDupStrategy actor, CMethodSet accum, CClassType[] args)
          Accumulates the set of methods with identifier name declared in the type represented by this, using the strategy actor.
private  void accumMethodsJMLOnly(CClass.NoDupStrategy actor, String name, CMethodSet accum)
          Accumulates the set of methods with identifier name declared in the type represented by this, ignoring external methods, using the strategy actor.
protected  void accumMostSpecificMethods(String name, CClass.NoDupStrategy actor, CMethodSet accum, CClassType[] args, CContextType context)
          Accumulates the set of methods with identifier name declared in the type represented by this, or added to the type by external methods, using the strategy actor.
 void checkFileNameAndSuffix(JmlSourceClass refinedType)
          This method ensures that a file at a lower level only refines a file at the same or higher level; but this check is only done on the most refined definition of a class.
 int classesRefined()
           
protected  int compareLevelsTo(JmlSourceClass other)
           
 int compareTo(Object o)
          Compares this to a given object.
static int computeSuffixNumber(String fileName)
          Computes the number associated with the suffix of the given file name.
protected  ClassInfo createClassInfo(long modifiers, String superClass, File sourceFile)
          Creates an instance of ClassInfo.
 boolean descendsFrom(CClass maybeSuper)
          Indicates whether this host is a subclass of the given class, where "subclass" is the reflexive, transitive closure of the extends relation.
private static CMethodSet.MethodArgsPair[] filterModelMethods(CMethodSet.MethodArgsPair[] methods)
          Filters out all model methods and returns only non-model methods.
 void finishSymbolTable()
          Finishes pre-processing of this type so it can be used as a symbol table.
 void finishSymbolTableForInterfaces()
           
protected  FieldInfo[] genFields()
          Returns an array representing all the fields for bytecode.
protected  MethodInfo[] genMethods()
          Returns an array representing all the methods for bytecode.
 CMethodSet.MethodArgsPair[] getAbstractMethods()
          Returns a list of abstract methods.
 JmlMemberDeclaration getAST()
          Returns the AST for this method.
protected  CField getDeclaredField(String ident)
          Returns the signature of the field with the given name declared in this class, or null if this class does not declare a field with the given name.
protected  CClass getDeclaredInnerType(String name)
          Searches for the inner type with the given name.
 CMethodSet.MethodArgsPair[] getInterfaceMethods()
          Returns a list of interface methods.
 int getLevelNumber()
           
 JmlSourceClass getMostRefined()
           
 JmlSourceClass getRefinedType()
          Returns the refined 'JmlSourceClass' for this class
 JmlSourceClass getRefiningType()
          Returns the refining 'JmlSourceClass' for this class
 CClass getSuperClass()
          Returns the super class of this class
 boolean inJavaFile()
          Returns true if this member is declared in a '.java' file.
protected  CClassType[] innerClassesForAttribute()
          Collects all the inner classes that must be added to the InnerClasses attribute.
 boolean inSpecFile()
          Returns true if this member is declared in a '.spec' file.
 boolean isAccessibleFrom(CMemberHost from)
          Indicates whether this is accessible from the given host.
 boolean isEffectivelyModel()
          Returns true iff this class should be treated as a model class; the class itself is defined as model or it is defined in a model class or interface.
protected  boolean isFieldRedefined(String ident, CExpressionContextType dummyContext)
          Returns true iff a field with same name is already defined in a superclass or an implemented interface.
 boolean isFinishedPreProcessing()
          Returns true if this member has finished the pre-processing needed so it can be used as a symbol table, i.e., the type has been processed through the checkInitializer phase.
 boolean isGhost()
          returns true iff this class is explicitly annotated with the ghost modifier.
 boolean isLocalTo(CMemberHost from)
          Indicates whether the declaration of this member is local to the given host.
 boolean isModel()
          returns true iff this class is explicitly annotated with the model modifier.
 boolean isMoreRefinedThan(JmlSourceClass j)
          Returns true if the calling object is more refined (perhaps in more than one step) than the argument; Returns false if they are the same object or the calling argument is less refined or they are not part of the same refinement seqeuence.
 boolean isRefined()
           
 boolean isRefiningType()
           
 JmlMemberAccess jmlAccess()
           
protected  CField lookupFieldHelper(String name, CExpressionContextType context)
          Searches a field in current class and parent hierarchy as needed
 CMethodSet lookupJMLMethodName(String name, CContextType context)
          For looking up methods that are not overloaded and appear in JML clauses that list method calls.
(package private)  CMethodSet lookupJMLMethodsWithSameSig(CMethod specMethod)
          Searches for the methods with the same signature as the given method, looking in parent hierarchy as needed.
 JmlSourceField lookupRefinedField(CField specField)
          Searches for the field refined by a given field, looking in the refinement hierarchy as needed.
 JmlSourceClass lookupRefinedInnerType(CClass specType)
          Searches for the inner type refined by a given inner type, looking in the refinement hierarchy as needed.
 JmlSourceMethod lookupRefinedMethod(CMethod specMethod)
          Searches for the method refined by a given method, looking in the refinement hierarchy as needed.
protected  boolean refines(Object maybeRefined)
           
 void setAST(JmlMemberDeclaration typeAST)
          Sets the AST for this method.
 void setFinishedPreProcessing()
          Sets the flag to true that this member has finished the pre-processing needed so it can be used as a symbol table, i.e., the type has been processed through the checkInitializer phase.
 void setRefinedType(JmlSourceClass refinedType)
          Sets the refinedType field of this JmlSourceClass object.
 
Methods inherited from class org.multijava.mjc.CSourceClass
addRMJMethodAnnotation, appendCustomAttributes, genCode, genConstructorArray, genInit, genSyntheticParams, genSyntheticParamsForExplicitThis, getOuterLocalAccess, getSyntheticParamsForExplicitSuper, getUniverseVersion, hasUniverseRuntimeSupport, initializerChecked, isAnonymous, isMember, 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

levelNumber

protected int levelNumber
The level number is determined by the suffix of the source file. Level 9 -- ".class". Level 8 -- ".jml-refined". Level 7 -- ".spec-refined". Level 6 -- ".java-refined". Level 5 -- ".jml". Level 4 -- ".spec". Level 3 -- ".java". Level 2 -- ".refines-jml". Level 1 -- ".refines-spec". Level 0 -- ".refines-java". The level number is used to form an ordering of the allowable sequence of refining files. That is, if a file is the most refined definition of a class, then it can only refine a file at the same or higher level. Also, the most refined definition of a class must be declared in a file with the same name as the class so it will be found by the type checker when that class is loaded.


modelField

private static CField modelField

stackLevel

private static int stackLevel

refinedSourceClass

protected JmlSourceClass refinedSourceClass
This field contains the source class of the type declaration that is refined by the current type; it is used when looking up names such as fields or classes. This is only done when looking for a name referenced inside a specification.


refiningSourceClass

protected JmlSourceClass refiningSourceClass

typeAST

private JmlMemberDeclaration typeAST

finishedPreProcessing

private boolean finishedPreProcessing
Constructor Detail

JmlSourceClass

public JmlSourceClass(Main compiler,
                      CClass owner,
                      CMemberHost host,
                      TokenReference where,
                      long modifiers,
                      String ident,
                      String qualifiedName,
                      CTypeVariable[] typevariables,
                      boolean isAnonymous,
                      boolean isMember,
                      boolean deprecated)
Constructs a class export from source

Method Detail

getSuperClass

public CClass getSuperClass()
Returns the super class of this class

Overrides:
getSuperClass in class CClass

checkFileNameAndSuffix

public void checkFileNameAndSuffix(JmlSourceClass refinedType)
                            throws UnpositionedError
This method ensures that a file at a lower level only refines a file at the same or higher level; but this check is only done on the most refined definition of a class. Also, the most refined definition of a class must be declared in a file with the same name as the class so it will be found by the type checker when that class is loaded. The level number is based on the suffix of the source file, see method computeSuffixNumber.

Throws:
UnpositionedError

getRefinedType

public JmlSourceClass getRefinedType()
Returns the refined 'JmlSourceClass' for this class


getRefiningType

public JmlSourceClass getRefiningType()
Returns the refining 'JmlSourceClass' for this class


isMoreRefinedThan

public boolean isMoreRefinedThan(JmlSourceClass j)
Returns true if the calling object is more refined (perhaps in more than one step) than the argument; Returns false if they are the same object or the calling argument is less refined or they are not part of the same refinement seqeuence.


setRefinedType

public void setRefinedType(JmlSourceClass refinedType)
Sets the refinedType field of this JmlSourceClass object. Throws an exception if setting this field would have created a cycle in the refinement sequence.


isRefiningType

public boolean isRefiningType()

isRefined

public boolean isRefined()

getMostRefined

public JmlSourceClass getMostRefined()

classesRefined

public int classesRefined()

setAST

public void setAST(JmlMemberDeclaration typeAST)
Sets the AST for this method.


getAST

public JmlMemberDeclaration getAST()
Returns the AST for this method.


compareTo

public int compareTo(Object o)
              throws ClassCastException
Compares this to a given object.

 also
   requires (o instanceof JmlSourceClass) &&
     qualifiedName().equals(((JmlSourceClass)o).qualifiedName());
	 ensures (* \result is ordered according to suffix of the source files *);
  also
   requires o != null && !(o instanceof JmlSourceClass);
   signals_only ClassCastException;
 

Specified by:
compareTo in interface Comparable
Overrides:
compareTo in class CClass
Parameters:
o - an Object value to compare to this
Returns:
0 if this.equals(o)
Throws:
ClassCastException - if o is incomparable to this

compareLevelsTo

protected int compareLevelsTo(JmlSourceClass other)

getLevelNumber

public int getLevelNumber()

descendsFrom

public boolean descendsFrom(CClass maybeSuper)
Indicates whether this host is a subclass of the given class, where "subclass" is the reflexive, transitive closure of the extends relation.

Specified by:
descendsFrom in interface CMemberHost
Overrides:
descendsFrom in class CClass
Parameters:
maybeSuper - the potential superclass

refines

protected boolean refines(Object maybeRefined)

lookupFieldHelper

protected CField lookupFieldHelper(String name,
                                   CExpressionContextType context)
                            throws UnpositionedError
Searches a field in current class and parent hierarchy as needed

Overrides:
lookupFieldHelper in class CClass
Parameters:
name - the simple name of the field
context - the context in which the reference appears, used for accessibility checks
Throws:
UnpositionedError - this error will be positioned soon

getDeclaredField

protected CField getDeclaredField(String ident)
Returns the signature of the field with the given name declared in this class, or null if this class does not declare a field with the given name. If not found in this class object, continue looking in any refined JmlSourceClass objects.

Overrides:
getDeclaredField in class CClass

isFieldRedefined

protected boolean isFieldRedefined(String ident,
                                   CExpressionContextType dummyContext)
                            throws UnpositionedError
Returns true iff a field with same name is already defined in a superclass or an implemented interface.

Overrides:
isFieldRedefined in class CClass
Parameters:
ident - the name of the field
Throws:
UnpositionedError

isAccessibleFrom

public boolean isAccessibleFrom(CMemberHost from)
Indicates whether this is accessible from the given host.

Specified by:
isAccessibleFrom in interface CMemberHost
Overrides:
isAccessibleFrom in class CMember
Parameters:
from - the host that wants access
Returns:
true iff the given host is allowed access to this host's members

isLocalTo

public boolean isLocalTo(CMemberHost from)
Indicates whether the declaration of this member is local to the given host. It adds another case to the two cases handled by the super class CMember: (See method isLocalTo in CMember for an explanation of those two cases). The additional case involves refinement and is necessary for private fields, methods, and classes declared inside a class declaration refined by the host of this member.
  1. If the given host is a class, then this member is local to the given host if the given host class refines the declaration where this member appears.

Overrides:
isLocalTo in class CMember
Parameters:
from - the given host

isEffectivelyModel

public boolean isEffectivelyModel()
Returns true iff this class should be treated as a model class; the class itself is defined as model or it is defined in a model class or interface.

Specified by:
isEffectivelyModel in interface org.jmlspecs.util.classfile.JmlModifiable

isModel

public boolean isModel()
returns true iff this class is explicitly annotated with the model modifier.

Specified by:
isModel in interface org.jmlspecs.util.classfile.JmlModifiable

isGhost

public boolean isGhost()
returns true iff this class is explicitly annotated with the ghost modifier.

Specified by:
isGhost in interface org.jmlspecs.util.classfile.JmlModifiable

getAbstractMethods

public CMethodSet.MethodArgsPair[] getAbstractMethods()
Returns a list of abstract methods. This method is called to check whether all abstract methods are implemented by the concrete class being type-checked. Thus, it is refined here to return only non-model methods.

Overrides:
getAbstractMethods in class CClass

getInterfaceMethods

public CMethodSet.MethodArgsPair[] getInterfaceMethods()
Returns a list of interface methods. This method is called to check whether all interface methods are implemented by the class being type-checked. Thus, it is refined here to return only non-model methods.

Overrides:
getInterfaceMethods in class CClass

accumMostSpecificMethods

protected void accumMostSpecificMethods(String name,
                                        CClass.NoDupStrategy actor,
                                        CMethodSet accum,
                                        CClassType[] args,
                                        CContextType context)
                                 throws UnpositionedError
Accumulates the set of methods with identifier name declared in the type represented by this, or added to the type by external methods, using the strategy actor. Only searches supertypes if no matches have been accumulated while searching the type represented by this. In this overriding method, we also accumulate methods from the refined class declaration of the refines clause, but only if no matches have been accumulated from this type and its supertypes.

Overrides:
accumMostSpecificMethods in class CClass
Parameters:
name - method name
actor - the strategy for selecting methods
accum - a method set in which to accumulate the results
context - the context in which the method reference appears, used for resolving augmenting
Throws:
UnpositionedError - at the discretion of the strategy actor

filterModelMethods

private static CMethodSet.MethodArgsPair[] filterModelMethods(CMethodSet.MethodArgsPair[] methods)
Filters out all model methods and returns only non-model methods.


computeSuffixNumber

public static int computeSuffixNumber(String fileName)
Computes the number associated with the suffix of the given file name. Suffixes are grouped for the purpose of handling and checking refinement sequences. The level number is determined by the suffix of the source file. Level 8 -- ".jml-refined". Level 7 -- ".spec-refined". Level 6 -- ".java-refined". Level 5 -- ".jml". Level 4 -- ".spec". Level 3 -- ".java". Level 2 -- ".refines-jml". Level 1 -- ".refines-spec". Level 0 -- ".refines-java". The level number is used to form an ordering of the allowable sequence of refining files. That is, a file at a lower level can only refine a file at the same or higher level, if it is the most refined definition of a class. Also, the most refined definition of a class must be declared in a file with the same name as the class so it will be found by the type checker when that class is loaded.


finishSymbolTable

public void finishSymbolTable()
Finishes pre-processing of this type so it can be used as a symbol table.


finishSymbolTableForInterfaces

public void finishSymbolTableForInterfaces()

accumLocalInternalMethods

protected void accumLocalInternalMethods(String name,
                                         CClass.NoDupStrategy actor,
                                         CMethodSet accum,
                                         CClassType[] args)
                                  throws UnpositionedError
Accumulates the set of methods with identifier name declared in the type represented by this, using the strategy actor. Searches neither external methods nor supertypes. This overriding method does, however, search refining types.

Overrides:
accumLocalInternalMethods in class CClass
Parameters:
name - method name
actor - the strategy for selecting methods
accum - a method set in which to accumulate the results
Throws:
UnpositionedError - at the discretion of the strategy actor

lookupJMLMethodName

public CMethodSet lookupJMLMethodName(String name,
                                      CContextType context)
                               throws UnpositionedError
For looking up methods that are not overloaded and appear in JML clauses that list method calls.

Throws:
UnpositionedError

lookupRefinedMethod

public JmlSourceMethod lookupRefinedMethod(CMethod specMethod)
Searches for the method refined by a given method, looking in the refinement hierarchy as needed.

Parameters:
specMethod - the method that is doing the specializing
Returns:
The method refined by specMethod, or null if it does not refine a method declared in a type refined by this type.
Throws:
UnpositionedError - -- should not happen

lookupRefinedField

public JmlSourceField lookupRefinedField(CField specField)
Searches for the field refined by a given field, looking in the refinement hierarchy as needed.

Parameters:
specField - the refining field
Returns:
The field refined by specField, or null if it does not refine a field declared in a type refined by this type.

lookupRefinedInnerType

public JmlSourceClass lookupRefinedInnerType(CClass specType)
Searches for the inner type refined by a given inner type, looking in the refinement hierarchy as needed.

Parameters:
specType - the refining inner type
Returns:
The inner type refined by specType, or null if it does not refine an inner type declared in a type refined by this type.

getDeclaredInnerType

protected CClass getDeclaredInnerType(String name)
Searches for the inner type with the given name. If not found in this class object, continue looking in any refined JmlSourceClass objects.


accumMethodsJMLOnly

private void accumMethodsJMLOnly(CClass.NoDupStrategy actor,
                                 String name,
                                 CMethodSet accum)
Accumulates the set of methods with identifier name declared in the type represented by this, ignoring external methods, using the strategy actor. Always searches supertypes, but only those parsed by the JML parser.

Parameters:
name - method name
actor - the strategy for selecting methods
accum - a method set in which to accumulate the results, satisfying the invariant that all methods in accum are applicable to the other arguments and any two distinct methods in accum are incomparable by the specializes relationship
Throws:
UnpositionedError - at the discretion of the strategy actor

lookupJMLMethodsWithSameSig

CMethodSet lookupJMLMethodsWithSameSig(CMethod specMethod)
Searches for the methods with the same signature as the given method, looking in parent hierarchy as needed.

Parameters:
specMethod - the method that is doing the overriding
Returns:
A set of methods, all with the same static type tuple and ident as specMethod, such that specMethod immediately specializes each method in the set.

jmlAccess

public JmlMemberAccess jmlAccess()
Returns:
the member access information object for this member.

inJavaFile

public boolean inJavaFile()
Returns true if this member is declared in a '.java' file.


inSpecFile

public boolean inSpecFile()
Returns true if this member is declared in a '.spec' file.


isFinishedPreProcessing

public boolean isFinishedPreProcessing()
Returns true if this member has finished the pre-processing needed so it can be used as a symbol table, i.e., the type has been processed through the checkInitializer phase.


setFinishedPreProcessing

public void setFinishedPreProcessing()
Sets the flag to true that this member has finished the pre-processing needed so it can be used as a symbol table, i.e., the type has been processed through the checkInitializer phase.


createClassInfo

protected ClassInfo createClassInfo(long modifiers,
                                    String superClass,
                                    File sourceFile)
Creates an instance of ClassInfo. This method is overridden here to return an instnace of the class JmlClassInfo.

Overrides:
createClassInfo in class CClass

genFields

protected FieldInfo[] genFields()
Returns an array representing all the fields for bytecode. This method is overridden here to return field infos for combined fields through the refinement chain.

Overrides:
genFields in class CClass

genMethods

protected MethodInfo[] genMethods()
Returns an array representing all the methods for bytecode. This method is overridden here to return method infos for combined methods through the refinement chain.

Overrides:
genMethods in class CClass

innerClassesForAttribute

protected CClassType[] innerClassesForAttribute()
Collects all the inner classes that must be added to the InnerClasses attribute. This method is overridden here to combine inner classes through the refinement chain. Refer to the method genInners.

Overrides:
innerClassesForAttribute in class CClass

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.