org.jmlspecs.checker
Class JmlTypeDeclaration

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Phylum
          org.multijava.mjc.JPhylum
              org.jmlspecs.checker.JmlNode
                  org.jmlspecs.checker.JmlMemberDeclaration
                      org.jmlspecs.checker.JmlTypeDeclaration

All Implemented Interfaces:

Annotatable, Cloneable, Comparable, CompilerPassEnterable, Constants, Constants, Constants, JMemberDeclarationType, JTypeDeclarationType, PhylumType

Direct Known Subclasses:

JmlClassDeclaration, JmlInterfaceDeclaration

public abstract class JmlTypeDeclaration

extends JmlMemberDeclaration

implements JTypeDeclarationType

This type represents a java class or interface in the syntax tree.

Nested Class Summary

 

Nested classes inherited from class org.jmlspecs.checker.JmlNode

JmlNode.DummyInitializerDeclaration

 

Field Summary
protected  JmlAxiom[]	axioms
private  CContextType	cachedContext
protected  JmlAxiom[]	combinedAxioms
protected  JmlConstraint[]	combinedConstraints
private  JFieldDeclarationType[]	combinedFields           The fields declared within the type represented by this, extracted from fieldsAndInits at initialization time and combined with any declarations refined by this type.
protected  JmlMemberDeclaration[]	combinedInners
protected  JmlInvariant[]	combinedInvariants
protected  JmlMemberDeclaration[]	combinedMethods
protected  JmlRepresentsDecl[]	combinedRepresentsDecls
protected  JmlVarAssertion[]	combinedVarAssertions
protected  JmlConstraint[]	constraints
protected  JmlDataGroupMemberMap	dataGroupMap
private  JTypeDeclaration	delegee
protected  boolean	hasBeenCombinedWithRefinedDecl
private  boolean	hasSourceInRefinement           Indicates whether this type declaration has a source file in the refinement chain.
protected  ArrayList	innerList
protected  JFieldDeclarationType[]	interfaceModelFields
protected  boolean[]	interfaceWeaklyFlags
protected  JmlInvariant[]	invariants
private  JmlMemberAccess	jmlAccess
protected  ArrayList	methodList
protected  JFieldDeclarationType[]	modelFields
protected  JmlRepresentsDecl[]	representsDecls
protected  JFieldDeclarationType[]	superClassModelFields
protected  JmlVarAssertion[]	varAssertions

 

Fields inherited from class org.jmlspecs.checker.JmlMemberDeclaration

refinedDecl, refiningDecl

 

Fields inherited from class org.jmlspecs.checker.JmlNode

MJCVISIT_MESSAGE

 

Fields inherited from class org.multijava.mjc.JPhylum

EMPTY

 

Fields inherited from class org.multijava.util.compiler.Phylum

 

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

JmlTypeDeclaration(TokenReference where, boolean[] interfaceWeaklyFlags, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JTypeDeclaration delegee)

 

Method Summary
void	accumAllTypeSignatures(ArrayList accum)           Adds the signature CSourceClass of this, and of all nested types, to accum.
void	addMember(JMemberDeclarationType newMember)           Adds the given member to this type's interface and modifies sourceClass to include the new member
JmlAxiom[]	axioms()
void	cachePassParameters(CContextType context)           Caches the arguments for the compiler passes.
void	checkAssignableClauses()
private  void	checkFieldsInterface(String javaFileName)
private  void	checkForCycles(JmlTypeDeclaration refinedType)           Sets the refinedType field of this JmlTypeDeclaration object.
void	checkInitializers()           Invokes the checkInitializers method of the implementing class using previously cached arguments.
void	checkInitializers(CContextType context)           Checks the static initializers created during the checkInterface pass and performs some other checks that can be performed simply before full blown typechecking.
void	checkInterface()           Invokes the checkInterface method of the implementing class using previously cached arguments.
void	checkInterface(CContextType context)           Checks the basic interfaces to make sure things generally look OK.
private  void	checkMethodsInterface(String javaFileName)
private  void	checkModelFields(JFieldDeclarationType[] modelFields)
boolean	checkRacability(Compiler compiler)           Checks if every method is rac-compilable.
private  JmlTypeDeclaration	checkRedundantRepresents(JmlRepresentsDecl redundantRep, String ident)
private  void	combineClassSpecs()
JmlAxiom[]	combinedAxioms()
JmlConstraint[]	combinedConstraints()
JmlInvariant[]	combinedInvariants()
JmlRepresentsDecl[]	combinedRepresentsDecls()
JmlVarAssertion[]	combinedVarAssertions()
private  void	combineFieldAndMethodModifiersOfNestedTypes()
private  void	combineFieldModifiersAndSetInitializer()
private  void	combineFieldSpecs()
private  void	combineMethodModifiersAndSetBody()
private  void	combineMethodSpecs()
private  void	combineNestedClassSpecs()
private  void	combineParameterModifiers(JmlMethodDeclaration meth)
void	combineSpecifications()
int	compareTo(Object o)           Compares this to a given object.
JmlConstraint[]	constraints()
JFieldDeclarationType[]	fields()
JPhylum[]	fieldsAndInits()           Returns an array of the static and instance initializers for the type represented by this.
JmlTypeDeclaration	findTypeWithRepresentsFor(CField field)           Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration.
void	generateInterface(Main compiler, CClass owner, CMemberHost host, String prefix, boolean isAnon, boolean isMember)           Generates a CSourceClass class signature singleton for this declaration.
JFieldDeclarationType[]	getAllInterfaceModelFields()           Returns all model fields inherited through the interface hierarchy.
ArrayList	getAllMethods()           Walks up the extends hierarchy and adds all methods to the returned ArrayList.
JFieldDeclarationType[]	getAllSuperClassModelFields()           Returns all model fields inherited from abstract superclasses.
JFieldDeclarationType[]	getCombinedFields()
JmlMemberDeclaration[]	getCombinedInners()
JmlMemberDeclaration[]	getCombinedMethods()
JmlDataGroupMemberMap	getDataGroupMap()           Computes the data group map (if it has not already been computed) and returns it.
JConstructorDeclarationType	getDefaultConstructor()
JFieldDeclarationType[]	getModelFields()           Computes and stores the model fields of this type into an array.
boolean	hasSourceInRefinement()           Returns true if this type declaration has a source file in the refinement chain.
String	ident()           Returns the identifier for this type declaration.
private  void	includeAllFields()
private  void	includeAllMethods()
private  void	includeAllNestedClasses()
protected  void	initializeDataGroupMap()           Initializes the map from JmlSourceField, a data group, to a JmlAssignableFieldSet, the set of fields in that data group.
boolean	inJavaFile()           Returns true if this member is declared in a '.java' file.
ArrayList	inners()           Returns null unless overridden by a subclass.
CClassType[]	interfaces()           Returns the set of interfaces that this type implements or extends.
boolean[]	interfaceWeaklyFlags()
JmlInvariant[]	invariants()
boolean	isAtTopLevel()
abstract  boolean	isClass()           Returns true if this is a class declaration.
boolean	isFinal()           Returns true if this type declaration is for a final type.
boolean	isInterface()           Returns true if this is an interface declaration.
JmlMemberAccess	jmlAccess()
private  void	linkFieldRefinements()           Links the fields in a refinement chain of this JmlTypeDeclaration object.
private  void	linkInnerTypeRefinements()           Links the inner types of a refinement chain of this JmlTypeDeclaration object.
private  void	linkMethodRefinements()           Links the methods in a refinement chain of this JmlTypeDeclaration object.
ArrayList	methods()
long	modifiers()
CClass	owner()           Returns the logical owner of this type.
void	preprocessDependencies()           Performs preliminary processing on compilation units and types.
void	preprocessDependencies(CContextType context)           Performs preliminary processing on compilation units and types.
JmlRepresentsDecl[]	representsDecls()
void	resolveSpecializers()           Resolves value specializer expressions to the compile-time constants they represent.
abstract  void	resolveSpecializers(CContextType context)           Computes the values of specializer expressions used to dispatch on compile-time constants.
void	resolveTopMethods()           Finds the top method of every declared method.
void	setDefaultConstructor(JConstructorDeclarationType defaultConstructor)
void	setFields(JPhylum[] fields)
void	setFieldsOnly(JFieldDeclarationType[] fields)
void	setHasSourceInRefinement(boolean flag)           Sets that if this type declaration has a source file in the refinement chain.
void	setIdent(String ident)
void	setInners(ArrayList v)
void	setMembersToCombinedMembers()
void	setMethods(ArrayList m)
void	setRefinedType(JmlBinaryType refinedType)           Registers that the given type declaration, refinedType, is refined by this type declaration.
void	setRefinedType(JmlTypeDeclaration refinedType)           Registers that the given type declaration, refinedType, is refined by this type declaration.
private  void	setRefiningType(JmlTypeDeclaration refiningDecl)
void	setStatic()           Marks this type as static.
void	syntheticOuterThisInaccessible()           Records the fact that even though the class is an inner class, we should not generate an outer this for it, because the outer this is not accessible.
void	translateMJ()           Invokes the translateMJ method of the implementing class using previously cached arguments.
void	translateMJ(CContextType context)           Refactors this to include dispatchers for multimethods and other code necessary for running MultiJava code on a standard JVM.
void	typecheck()           Invokes the typecheck method of the implementing class using previously cached arguments.
void	typecheck(CContextType context)           Typechecks this type declaration in the context in which it appears.
private  void	typecheckSuperTypes()
CTypeVariable[]	typevariables()
void	unsetStatic()           Marks this type as non-static.
JmlVarAssertion[]	varAssertions()

 

Methods inherited from class org.jmlspecs.checker.JmlMemberDeclaration

accept, checkRefinedModifiers, findJavaFileInRefinement, genComments, getCClass, getCombinedSpecification, getCombinedVarAssertions, getField, getMethod, getMostRefined, getRefinedMember, getRefiningMember, inBinaryClassFile, isDeprecated, isRefined, isRefiningMember, javadocComment, setRefinedMember, setRefiningMember, stringRepresentation

 

Methods inherited from class org.jmlspecs.checker.JmlNode

enterSpecScope, enterSpecScope, exitSpecScope, exitSpecScope, privacy, privacyString

 

Methods inherited from class org.multijava.mjc.JPhylum

check, check, check, check, fail, fail, fail, warn, warn, warn, warn

 

Methods inherited from class org.multijava.util.compiler.Phylum

getTokenReference, setTokenReference

 

Methods inherited from class org.multijava.util.Utils

assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Methods inherited from interface org.multijava.mjc.JTypeDeclarationType

createContext

 

Methods inherited from interface org.multijava.mjc.JMemberDeclarationType

accept, genComments, getCClass, getField, getMethod, isDeprecated

 

Methods inherited from interface org.multijava.util.compiler.PhylumType

getTokenReference, setTokenReference

 

Methods inherited from interface org.multijava.javadoc.Annotatable

javadocComment

 

Methods inherited from interface org.multijava.mjc.CompilerPassEnterable

accept, getTokenReference

 

Field Detail

cachedContext

private CContextType cachedContext

delegee

private JTypeDeclaration delegee

jmlAccess

private JmlMemberAccess jmlAccess

interfaceWeaklyFlags

protected boolean[] interfaceWeaklyFlags

invariants

protected JmlInvariant[] invariants

constraints

protected JmlConstraint[] constraints

representsDecls

protected JmlRepresentsDecl[] representsDecls

axioms

protected JmlAxiom[] axioms

varAssertions

protected JmlVarAssertion[] varAssertions

combinedInvariants

protected JmlInvariant[] combinedInvariants

combinedConstraints

protected JmlConstraint[] combinedConstraints

combinedRepresentsDecls

protected JmlRepresentsDecl[] combinedRepresentsDecls

combinedAxioms

protected JmlAxiom[] combinedAxioms

combinedVarAssertions

protected JmlVarAssertion[] combinedVarAssertions

combinedFields

private JFieldDeclarationType[] combinedFields

The fields declared within the type represented by this, extracted from fieldsAndInits at initialization time and combined with any declarations refined by this type.

methodList

protected ArrayList methodList

combinedMethods

protected JmlMemberDeclaration[] combinedMethods

innerList

protected ArrayList innerList

combinedInners

protected JmlMemberDeclaration[] combinedInners

modelFields

protected JFieldDeclarationType[] modelFields

superClassModelFields

protected JFieldDeclarationType[] superClassModelFields

interfaceModelFields

protected JFieldDeclarationType[] interfaceModelFields

dataGroupMap

protected JmlDataGroupMemberMap dataGroupMap

hasSourceInRefinement

private boolean hasSourceInRefinement

Indicates whether this type declaration has a source file in the refinement chain. This field is used by jmlrac.

hasBeenCombinedWithRefinedDecl

protected boolean hasBeenCombinedWithRefinedDecl

JmlTypeDeclaration

public JmlTypeDeclaration(TokenReference where,
                          boolean[] interfaceWeaklyFlags,
                          JmlInvariant[] invariants,
                          JmlConstraint[] constraints,
                          JmlRepresentsDecl[] representsDecls,
                          JmlAxiom[] axioms,
                          JmlVarAssertion[] varAssertions,
                          JTypeDeclaration delegee)

generateInterface

public void generateInterface(Main compiler,
                              CClass owner,
                              CMemberHost host,
                              String prefix,
                              boolean isAnon,
                              boolean isMember)

Generates a CSourceClass class signature singleton for this declaration.

Specified by:

generateInterface in interface JTypeDeclarationType

Parameters:

compiler - the compiler instance for which this singleton is generated

owner - the class signature singleton for the logical outer class of this, or null if this is a top level declaration

host - the signature singleton of the context in which this is declared, a CCompilationUnit for top-level declarations

prefix - the prefix prepended to this declaration's identifier to achieve the fully qualified name, just the package name (using '/' separators) for top-level classes, package name plus $-delimited outer class names plus synthetic index for inner classes

isAnon - true if this is an anonymous class, in which case the fully qualified name is just prefix

isMember - true if this is a member type, i.e., a nested type that is not a local type or an anonymous class

interfaceWeaklyFlags

public boolean[] interfaceWeaklyFlags()

invariants

public JmlInvariant[] invariants()

constraints

public JmlConstraint[] constraints()

representsDecls

public JmlRepresentsDecl[] representsDecls()

axioms

public JmlAxiom[] axioms()

varAssertions

public JmlVarAssertion[] varAssertions()

combinedInvariants

public JmlInvariant[] combinedInvariants()

combinedConstraints

public JmlConstraint[] combinedConstraints()

combinedRepresentsDecls

public JmlRepresentsDecl[] combinedRepresentsDecls()

combinedAxioms

public JmlAxiom[] combinedAxioms()

combinedVarAssertions

public JmlVarAssertion[] combinedVarAssertions()

typevariables

public CTypeVariable[] typevariables()

interfaces

public CClassType[] interfaces()

Description copied from interface: JTypeDeclarationType

Returns the set of interfaces that this type implements or extends.

Specified by:

interfaces in interface JTypeDeclarationType

fieldsAndInits

public JPhylum[] fieldsAndInits()

Returns an array of the static and instance initializers for the type represented by this.

Specified by:

fieldsAndInits in interface JTypeDeclarationType

methods

public ArrayList methods()

Specified by:

methods in interface JTypeDeclarationType

setMethods

public void setMethods(ArrayList m)

inners

public ArrayList inners()

Description copied from class: JmlMemberDeclaration

Returns null unless overridden by a subclass. Returns null if it does not have any inner type declarations.

Specified by:

inners in interface JTypeDeclarationType

Overrides:

inners in class JmlMemberDeclaration

setInners

public void setInners(ArrayList v)

Specified by:

setInners in interface JTypeDeclarationType

isAtTopLevel

public boolean isAtTopLevel()

Specified by:

isAtTopLevel in interface JTypeDeclarationType

Returns:

true if this class is at top level

fields

public JFieldDeclarationType[] fields()

Specified by:

fields in interface JTypeDeclarationType

getDefaultConstructor

public JConstructorDeclarationType getDefaultConstructor()

Specified by:

getDefaultConstructor in interface JTypeDeclarationType

setDefaultConstructor

public void setDefaultConstructor(JConstructorDeclarationType defaultConstructor)

Specified by:

setDefaultConstructor in interface JTypeDeclarationType

setIdent

public void setIdent(String ident)

Specified by:

setIdent in interface JTypeDeclarationType

ident

public String ident()

Returns the identifier for this type declaration.

Specified by:

ident in interface JTypeDeclarationType

Returns:

the unqualified identifier for this type declaration

addMember

public void addMember(JMemberDeclarationType newMember)

Adds the given member to this type's interface and modifies sourceClass to include the new member

Specified by:

addMember in interface JTypeDeclarationType

Parameters:

newMember - a member to be added to this type

setFields

public void setFields(JPhylum[] fields)

setFieldsOnly

public void setFieldsOnly(JFieldDeclarationType[] fields)

owner

public CClass owner()

Returns the logical owner of this type.

Specified by:

owner in interface JTypeDeclarationType

modifiers

public long modifiers()

Specified by:

modifiers in interface JTypeDeclarationType

setStatic

public void setStatic()

Marks this type as static.

 also
   requires (* this.generateInterface(...) has not been invoked *);
   requires_redundantly (* sourceClass == null *); 
   ensures hasFlag(delegee.modifiers(), ACC_STATIC);
 

Specified by:

setStatic in interface JTypeDeclarationType

unsetStatic

public void unsetStatic()

Marks this type as non-static.

 also 
 ensures !hasFlag(delegee.modifiers,ACC_STATIC);
 

Specified by:

unsetStatic in interface JTypeDeclarationType

syntheticOuterThisInaccessible

public void syntheticOuterThisInaccessible()

Records the fact that even though the class is an inner class, we should not generate an outer this for it, because the outer this is not accessible. The sourceClass field should not be null.

Specified by:

syntheticOuterThisInaccessible in interface JTypeDeclarationType

accumAllTypeSignatures

public void accumAllTypeSignatures(ArrayList accum)

Adds the signature CSourceClass of this, and of all nested types, to accum.

Specified by:

accumAllTypeSignatures in interface JTypeDeclarationType

isFinal

public boolean isFinal()

Returns true if this type declaration is for a final type.

isClass

public abstract boolean isClass()

Returns true if this is a class declaration.

isInterface

public boolean isInterface()

Returns true if this is an interface declaration.

hasSourceInRefinement

public boolean hasSourceInRefinement()

Returns true if this type declaration has a source file in the refinement chain. This method is used by jmlrac.

setHasSourceInRefinement

public void setHasSourceInRefinement(boolean flag)

Sets that if this type declaration has a source file in the refinement chain. This method is used by jmlrac.

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.

Overrides:

inJavaFile in class JmlMemberDeclaration

getDataGroupMap

public JmlDataGroupMemberMap getDataGroupMap()

Computes the data group map (if it has not already been computed) and returns it. The data group map is a map from each field to the set of fields in its data group. Only model, spec_public, and spec_protected fields can have more than one field (itself) in this set.

getModelFields

public JFieldDeclarationType[] getModelFields()

Computes and stores the model fields of this type into an array. These are the fields that need to have a represents clause and have an associated data group. Returns an array of the model fields of this type (not including model fields inherited from interfaces implemented or from the superclass).

initializeDataGroupMap

protected void initializeDataGroupMap()

Initializes the map from JmlSourceField, a data group, to a JmlAssignableFieldSet, the set of fields in that data group.

getAllSuperClassModelFields

public JFieldDeclarationType[] getAllSuperClassModelFields()

Returns all model fields inherited from abstract superclasses. This method must be called at the end of typechecking.

getAllInterfaceModelFields

public JFieldDeclarationType[] getAllInterfaceModelFields()

Returns all model fields inherited through the interface hierarchy. This method must be called at the end of typechecking.

findTypeWithRepresentsFor

public JmlTypeDeclaration findTypeWithRepresentsFor(CField field)

Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration. If such a clause is found, returns the type declaration that includes the clause; otherwise, returns null.

 requires field != null && hasFlag(field.modifiers(),ACC_MODEL);
 ensures \result != null ==> (* \result has represents clause  r 
   such that !r.isRedundantly() && r.usesAbstractionFunction() && 
   r.storeRef() refers to field *);
 

checkRedundantRepresents

private JmlTypeDeclaration checkRedundantRepresents(JmlRepresentsDecl redundantRep,
                                                    String ident)

getAllMethods

public ArrayList getAllMethods()

Walks up the extends hierarchy and adds all methods to the returned ArrayList.

Specified by:

getAllMethods in interface JTypeDeclarationType

Returns:

a ArrayList that includes the CMethods for all methods in this class and all direct ancestors

preprocessDependencies

public void preprocessDependencies(CContextType context)
                            throws PositionedError

Performs preliminary processing on compilation units and types. Processes type imports so external methods' receiver types can be analyzed and supertypes can be resolved. Groups external methods by name, corresponding to the anchor classes that will eventually be generated. Mutates the name space management in CTopLevel to record a CGenericFunctionCollection singleton for each anchor class.

Specified by:

preprocessDependencies in interface JTypeDeclarationType

Throws:

PositionedError

checkInterface

public void checkInterface(CContextType context)
                    throws PositionedError

Checks the basic interfaces to make sure things generally look OK. This pass gathers information about the type signatures of everything (imported class files, classes being compiled, methods, fields, etc...) needed for the later passes. This information is stored in a CCompilationUnit instance and instances of CMember that are bound to the AST. Also adds things like the default constructor and the initializer method to the AST (these are suppressed during pretty-printing).

Specified by:

checkInterface in interface JTypeDeclarationType

Parameters:

context - the context in which this decl appears

Throws:

PositionedError - an error with reference to the source file

checkInitializers

public void checkInitializers(CContextType context)
                       throws PositionedError

Checks the static initializers created during the checkInterface pass and performs some other checks that can be performed simply before full blown typechecking.

Specified by:

checkInitializers in interface JTypeDeclarationType

Parameters:

context - the context in which this class declaration appears

Throws:

PositionedError - if check fails

resolveSpecializers

public abstract void resolveSpecializers(CContextType context)
                                  throws PositionedError

Computes the values of specializer expressions used to dispatch on compile-time constants. The JML-specific combining of specifications is done during this pass so computing the data group members and the assignable fields of a method can be computed during typechecking.

Specified by:

resolveSpecializers in interface JTypeDeclarationType

Parameters:

context - the context in which this class declaration appears

Throws:

PositionedError - if the check fails

resolveTopMethods

public void resolveTopMethods()
                       throws PositionedError

Finds the top method of every declared method. Called after the checkInitializers pass. This cannot be done before then because the external generic function mappings are not complete until the end of the checkInterface pass and the constant value specializers are not known until after the checkInitializers pass. This must be done before the typecheck pass so that all specialized argument positions for generic functions are known for ambiguity checking.

Specified by:

resolveTopMethods in interface JTypeDeclarationType

Throws:

PositionedError

typecheck

public void typecheck(CContextType context)
               throws PositionedError

Typechecks this type declaration in the context in which it appears. Mutates the context to record the information learned during checking. Actually just updates the context by adding a CSourceClass representation of this. Overriding methods in subclasses of this handle the actual checks.

Specified by:

typecheck in interface JTypeDeclarationType

Parameters:

context - the context in which this type declaration appears

Throws:

PositionedError - if any checks fail

translateMJ

public void translateMJ(CContextType context)

Refactors this to include dispatchers for multimethods and other code necessary for running MultiJava code on a standard JVM.

Specified by:

translateMJ in interface JTypeDeclarationType

compareTo

public int compareTo(Object o)
              throws ClassCastException

Compares this to a given object.

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

Specified by:

compareTo in interface Comparable

Parameters:

o - an Object value to compare to this

Returns:

0 if this.equals(o)

Throws:

ClassCastException - if o is incomparable to this

cachePassParameters

public void cachePassParameters(CContextType context)

Caches the arguments for the compiler passes.

Specified by:

cachePassParameters in interface JTypeDeclarationType

See Also:

!FIXME! this spec (or the implementation) is wrong, delegee's state is not changed

 also
  ensures delegee.arePassParametersCached;
 

preprocessDependencies

public void preprocessDependencies()
                            throws PositionedError

Performs preliminary processing on compilation units and types. Processes type imports so external methods' receiver types can be analyzed and supertypes can be resolved. Groups external methods by name, corresponding to the anchor classes that will eventually be generated. Mutates the name space management in CTopLevel to record a CGenericFunctionCollection singleton for each anchor class.

Specified by:

preprocessDependencies in interface CompilerPassEnterable

Throws:

PositionedError

checkInterface

public void checkInterface()
                    throws PositionedError

Description copied from interface: CompilerPassEnterable

Invokes the checkInterface method of the implementing class using previously cached arguments.

 requires arePassParametersCached;
 

Specified by:

checkInterface in interface CompilerPassEnterable

Throws:

PositionedError

checkInitializers

public void checkInitializers()
                       throws PositionedError

Description copied from interface: CompilerPassEnterable

Invokes the checkInitializers method of the implementing class using previously cached arguments.

 requires arePassParametersCached;
 

Specified by:

checkInitializers in interface CompilerPassEnterable

Throws:

PositionedError

resolveSpecializers

public void resolveSpecializers()
                         throws PositionedError

Description copied from interface: CompilerPassEnterable

Resolves value specializer expressions to the compile-time constants they represent. Must come after the checkInitializers phase.

Specified by:

resolveSpecializers in interface CompilerPassEnterable

Throws:

PositionedError

typecheck

public void typecheck()
               throws PositionedError

Description copied from interface: CompilerPassEnterable

Invokes the typecheck method of the implementing class using previously cached arguments.

 requires arePassParametersCached;
 

Specified by:

typecheck in interface CompilerPassEnterable

Throws:

PositionedError

translateMJ

public void translateMJ()

Description copied from interface: CompilerPassEnterable

Invokes the translateMJ method of the implementing class using previously cached arguments.

 requires arePassParametersCached;
 

Specified by:

translateMJ in interface CompilerPassEnterable

setRefinedType

public void setRefinedType(JmlBinaryType refinedType)

Registers that the given type declaration, refinedType, is refined by this type declaration.

setRefinedType

public void setRefinedType(JmlTypeDeclaration refinedType)
                    throws PositionedError

Registers that the given type declaration, refinedType, is refined by this type declaration.

Throws:

PositionedError

checkForCycles

private void checkForCycles(JmlTypeDeclaration refinedType)
                     throws PositionedError

Sets the refinedType field of this JmlTypeDeclaration object. Throws an exception if setting this field would have created a cycle in the refinement sequence.

Throws:

PositionedError

setRefiningType

private void setRefiningType(JmlTypeDeclaration refiningDecl)

checkFieldsInterface

private void checkFieldsInterface(String javaFileName)

checkModelFields

private void checkModelFields(JFieldDeclarationType[] modelFields)

typecheckSuperTypes

private void typecheckSuperTypes()

checkMethodsInterface

private void checkMethodsInterface(String javaFileName)

checkAssignableClauses

public void checkAssignableClauses()
                            throws PositionedError

Throws:

PositionedError

getCombinedFields

public JFieldDeclarationType[] getCombinedFields()

getCombinedMethods

public JmlMemberDeclaration[] getCombinedMethods()

getCombinedInners

public JmlMemberDeclaration[] getCombinedInners()

setMembersToCombinedMembers

public void setMembersToCombinedMembers()

combineFieldModifiersAndSetInitializer

private void combineFieldModifiersAndSetInitializer()

combineMethodModifiersAndSetBody

private void combineMethodModifiersAndSetBody()

combineParameterModifiers

private void combineParameterModifiers(JmlMethodDeclaration meth)

combineFieldAndMethodModifiersOfNestedTypes

private void combineFieldAndMethodModifiersOfNestedTypes()

combineSpecifications

public void combineSpecifications()

Description copied from class: JmlMemberDeclaration

Combine the specifications of this declaration with the specifications of the declarations it refines.

linkFieldRefinements

private void linkFieldRefinements()

Links the fields in a refinement chain of this JmlTypeDeclaration object.

linkMethodRefinements

private void linkMethodRefinements()

Links the methods in a refinement chain of this JmlTypeDeclaration object.

linkInnerTypeRefinements

private void linkInnerTypeRefinements()
                               throws PositionedError

Links the inner types of a refinement chain of this JmlTypeDeclaration object.

Throws:

PositionedError

combineMethodSpecs

private void combineMethodSpecs()

includeAllMethods

private void includeAllMethods()

combineFieldSpecs

private void combineFieldSpecs()

includeAllFields

private void includeAllFields()

combineNestedClassSpecs

private void combineNestedClassSpecs()

includeAllNestedClasses

private void includeAllNestedClasses()

combineClassSpecs

private void combineClassSpecs()

checkRacability

public boolean checkRacability(Compiler compiler)

Checks if every method is rac-compilable. That is, checks that all concrete methods have body.