org.jmlspecs.checker
Class JClassDeclarationWrapper

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Phylum
          org.multijava.mjc.JPhylum
              org.multijava.mjc.JMemberDeclaration
                  org.multijava.mjc.JTypeDeclaration
                      org.multijava.mjc.JClassDeclaration
                          org.jmlspecs.checker.JClassDeclarationWrapper

All Implemented Interfaces:

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

public class JClassDeclarationWrapper

extends JClassDeclaration

A wrapper class to JClassDeclaration to implement JML-specific typechecking.

Nested Class Summary

 

Nested classes inherited from class org.multijava.mjc.JTypeDeclaration

JTypeDeclaration.WrapResult

 

Field Summary
protected  boolean	isRefinedType

 

Fields inherited from class org.multijava.mjc.JClassDeclaration

self, superType

 

Fields inherited from class org.multijava.mjc.JTypeDeclaration

cachedContext, fieldsAndInits, ident, inners, instanceInit, interfaces, methods, modifiers, sourceClass, statInit, typevariables, uniqueSourceClass

 

Fields inherited from class org.multijava.mjc.JMemberDeclaration

 

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.multijava.mjc.Constants

ACC_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, 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

JClassDeclarationWrapper(TokenReference where, long modifiers, String ident, CClassType superType, CClassType[] interfaces, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JavadocComment javadoc, JavaStyleComment[] comments)           Constructs a class declaration in the parsing tree.

JClassDeclarationWrapper(TokenReference where, long modifiers, String ident, CTypeVariable[] typevariables, CClassType superType, CClassType[] interfaces, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JavadocComment javadoc, JavaStyleComment[] comments, boolean isRefinedType)           Constructs a class declaration in the parsing tree.

 

Method Summary
int	compareTo(Object o)           Compares this to a given object.
protected  JConstructorDeclarationType	constructDefaultConstructor()           Builds an AST node representing the default constructor for this class.
boolean	hasConstructor()           Returns true if this class declaration contains an explicit constructor declaration.
protected  boolean	inJavaFile()
boolean	isRefinedType()
protected  CSourceClass	makeSignature(Main compiler, CClass owner, CMemberHost host, String prefix, boolean isAnon, boolean isMember)           Generates the signature object for this class declaration.

 

Methods inherited from class org.multijava.mjc.JClassDeclaration

accept, checkInitializers, checkInterface, constructInitializers, createContext, ident, preprocessDependencies, resolveSpecializers, setInterfaces, setSuperClass, superName, typecheck

 

Methods inherited from class org.multijava.mjc.JTypeDeclaration

accumAllTypeSignatures, addMember, annotateInternalInterfaceMethods, cachePassParameters, checkForDups, checkForSameSignature, checkInitializers, checkInterface, dispatcherWrapMethods, fields, fieldsAndInits, generateInterface, getAllMethods, getDefaultConstructor, inners, interfaces, isAtTopLevel, isDeclaredInDifferentSourceFiles, methods, methodsToBeWrapped, modifiers, owner, preprocessDependencies, preprocessDependencies, registerSignature, resolveExtMethods, resolveSpecializers, resolveTopMethods, setDefaultConstructor, setFields, setFieldsOnly, setIdent, setInners, setMethods, setStatic, syntheticOuterThisInaccessible, translateMJ, translateMJ, typecheck, typevariables, uniqueSourceWarning, unsetStatic

 

Methods inherited from class org.multijava.mjc.JMemberDeclaration

genComments, getCClass, getField, getMethod, isDeprecated, javadocComment, setInterface

 

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

accumAllTypeSignatures, addMember, cachePassParameters, fields, fieldsAndInits, generateInterface, getAllMethods, getDefaultConstructor, inners, interfaces, isAtTopLevel, methods, modifiers, owner, resolveTopMethods, setDefaultConstructor, setIdent, setInners, setStatic, syntheticOuterThisInaccessible, translateMJ, unsetStatic

 

Methods inherited from interface org.multijava.mjc.JMemberDeclarationType

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

checkInitializers, checkInterface, getTokenReference, preprocessDependencies, resolveSpecializers, translateMJ, typecheck

 

Field Detail

isRefinedType

protected boolean isRefinedType

JClassDeclarationWrapper

public JClassDeclarationWrapper(TokenReference where,
                                long modifiers,
                                String ident,
                                CClassType superType,
                                CClassType[] interfaces,
                                ArrayList methods,
                                ArrayList inners,
                                JPhylum[] fieldsAndInits,
                                JavadocComment javadoc,
                                JavaStyleComment[] comments)

Constructs a class declaration in the parsing tree.

Parameters:

where - the line of this node in the source code

modifiers - the list of modifiers of this class

ident - the short name of this class

superType - the name of this class's superclass

interfaces - the names of this types's interfaces

methods - a list of JMethodDeclarationTypes giving the methods of this type

inners - a list of JTypeDeclarationTypes giving the inner classes (and interfaces) of this type

fieldsAndInits - the fields and initializers of this type, passed together because the order matters for class and object initialization, members of the array should be instances of JFieldDeclarationType or JClassBlock

javadoc - javadoc comments including whether this type declaration is deprecated

comments - regular java comments

JClassDeclarationWrapper

public JClassDeclarationWrapper(TokenReference where,
                                long modifiers,
                                String ident,
                                CTypeVariable[] typevariables,
                                CClassType superType,
                                CClassType[] interfaces,
                                ArrayList methods,
                                ArrayList inners,
                                JPhylum[] fieldsAndInits,
                                JavadocComment javadoc,
                                JavaStyleComment[] comments,
                                boolean isRefinedType)

Constructs a class declaration in the parsing tree.

Parameters:

where - the line of this node in the source code

modifiers - the list of modifiers of this class

ident - the short name of this class

superType - the name of this class's superclass

interfaces - the names of this types's interfaces

methods - a list of JMethodDeclarationTypes giving the methods of this type

inners - a list of JTypeDeclarationTypes giving the inner classes (and interfaces) of this type

fieldsAndInits - the fields and initializers of this type, passed together because the order matters for class and object initialization, members of the array should be instances of JFieldDeclarationType or JClassBlock

javadoc - javadoc comments including whether this type declaration is deprecated

comments - regular java comments

makeSignature

protected CSourceClass makeSignature(Main compiler,
                                     CClass owner,
                                     CMemberHost host,
                                     String prefix,
                                     boolean isAnon,
                                     boolean isMember)

Generates the signature object for this class declaration. This method overrides the inherited method to generate JML-specific signature object, i.e., an instance of JmlSourceClass.

Overrides:

makeSignature in class JTypeDeclaration

Parameters:

compiler - the compiler instance for which this signature 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

hasConstructor

public boolean hasConstructor()

Returns true if this class declaration contains an explicit constructor declaration. This method is used by checkInterface to determine whether or not to create a default constructor for this type, i.e., when no explicit constructor is found. In a refinement chain, if this declaration is not a '.java' file, then true is returned. (True is returned because the default constructor should only be automatically generated for the '.java' file.)

Specified by:

hasConstructor in interface JClassDeclarationType

Overrides:

hasConstructor in class JClassDeclaration

constructDefaultConstructor

protected JConstructorDeclarationType constructDefaultConstructor()

Builds an AST node representing the default constructor for this class.

Overrides:

constructDefaultConstructor in class JClassDeclaration

Returns:

an AST node

inJavaFile

protected boolean inJavaFile()

compareTo

public int compareTo(Object o)
              throws ClassCastException

Description copied from class: JTypeDeclaration

Compares this to a given object.

also
ensures (* \result == lexically ordered according to the type name *);
also
requires o != null && !(o instanceof JTypeDeclaration);
signals_only ClassCastException;
 

Specified by:

compareTo in interface Comparable

Overrides:

compareTo in class JTypeDeclaration

Throws:

ClassCastException

isRefinedType

public boolean isRefinedType()