org.jmlspecs.checker
Class JmlSourceClass

java.lang.Object
  org.multijava.util.Utils
      org.multijava.mjc.CMember
          org.multijava.mjc.CClass
              org.multijava.mjc.CSourceClass
                  org.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_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

JmlSourceClass(Main compiler, CClass owner, CMemberHost host, TokenReference where, long modifiers, String ident, String qualifiedName, 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, checkInstantiation, 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, 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, deprecated, getCCompilationUnit, getField, getIdent, getJavaName, getMethod, getOwnerName, getQualNameWithSeparator, hasDefaultAccess, host, ident, 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

JmlSourceClass

public JmlSourceClass(Main compiler,
                      CClass owner,
                      CMemberHost host,
                      TokenReference where,
                      long modifiers,
                      String ident,
                      String qualifiedName,
                      boolean isAnonymous,
                      boolean isMember,
                      boolean deprecated)

Constructs a class export from source

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