org.jmlspecs.checker
Class JmlClassDeclaration

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
                          org.jmlspecs.checker.JmlClassDeclaration

All Implemented Interfaces:

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

public class JmlClassDeclaration

extends JmlTypeDeclaration

implements JClassDeclarationType

This type represents a java class declaration in the syntax tree.

Nested Class Summary

 

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

JmlNode.DummyInitializerDeclaration

 

Field Summary
protected  JClassDeclarationWrapper	delegee
private  boolean	isRacable           Is this class declaration runtime assertion checkable?
private  boolean	isWeakSubtype

 

Fields inherited from class org.jmlspecs.checker.JmlTypeDeclaration

axioms, combinedAxioms, combinedConstraints, combinedInners, combinedInvariants, combinedMethods, combinedRepresentsDecls, combinedVarAssertions, constraints, dataGroupMap, hasBeenCombinedWithRefinedDecl, innerList, interfaceModelFields, interfaceWeaklyFlags, invariants, methodList, modelFields, representsDecls, superClassModelFields, 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.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_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
protected	JmlClassDeclaration(TokenReference where, boolean isWeakSubtype, boolean[] interfaceWeaklyFlags, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JClassDeclarationWrapper delegee)           Constructs a new JML class declaration; clients should use factory method makeInstance instead.

 

Method Summary
void	accept(MjcVisitor p)           Accepts the specified visitor.
CClassContextType	createContext(CContextType parent)           Creates a class context for this class declaration.
boolean	hasConstructor()           Returns true if this class declaration contains an explicit constructor declaration.
boolean	isClass()           Returns true if this is a class declaration.
boolean	isRacable()           Is this class declaration runtime assertion checkable?
boolean	isWeakSubtype()
static JmlClassDeclaration	makeInstance(TokenReference where, long modifiers, String ident, CClassType superType, boolean isWeakSubtype, CClassType[] interfaces, boolean[] interfaceWeaklyFlags, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JavadocComment javadoc, JavaStyleComment[] comment, boolean isRefinedType)           Constructs a class declaration in the parsing tree.
void	resolveSpecializers(CContextType context)           Computes the values of specializer expressions used to dispatch on compile-time constants.
void	setInterfaces(CClassType[] interfaces)           Sets the super class
void	setRacable()           Indicates that this class declaration is runtime assertion checkable.
void	setSuperClass(CClassType superType)           Sets the super class
String	superName()

 

Methods inherited from class org.jmlspecs.checker.JmlTypeDeclaration

accumAllTypeSignatures, addMember, axioms, cachePassParameters, checkAssignableClauses, checkInitializers, checkInitializers, checkInterface, checkInterface, checkRacability, combinedAxioms, combinedConstraints, combinedInvariants, combinedRepresentsDecls, combinedVarAssertions, combineSpecifications, compareTo, constraints, fields, fieldsAndInits, findTypeWithRepresentsFor, generateInterface, getAllInterfaceModelFields, getAllMethods, getAllSuperClassModelFields, getCombinedFields, getCombinedInners, getCombinedMethods, getDataGroupMap, getDefaultConstructor, getModelFields, hasSourceInRefinement, ident, initializeDataGroupMap, inJavaFile, inners, interfaces, interfaceWeaklyFlags, invariants, isAtTopLevel, isFinal, isInterface, jmlAccess, methods, modifiers, owner, preprocessDependencies, preprocessDependencies, representsDecls, resolveSpecializers, resolveTopMethods, setDefaultConstructor, setFields, setFieldsOnly, setHasSourceInRefinement, setIdent, setInners, setMembersToCombinedMembers, setMethods, setRefinedType, setRefinedType, setStatic, syntheticOuterThisInaccessible, translateMJ, translateMJ, typecheck, typecheck, unsetStatic, varAssertions

 

Methods inherited from class org.jmlspecs.checker.JmlMemberDeclaration

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

accumAllTypeSignatures, addMember, cachePassParameters, checkInitializers, checkInterface, fields, fieldsAndInits, generateInterface, getAllMethods, getDefaultConstructor, ident, inners, interfaces, isAtTopLevel, methods, modifiers, owner, preprocessDependencies, resolveTopMethods, setDefaultConstructor, setIdent, setInners, setStatic, syntheticOuterThisInaccessible, translateMJ, typecheck, 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

 

Methods inherited from interface java.lang.Comparable

compareTo

 

Field Detail

delegee

protected JClassDeclarationWrapper delegee

isWeakSubtype

private boolean isWeakSubtype

isRacable

private boolean isRacable

Is this class declaration runtime assertion checkable? This flag is used by the jmlc.

JmlClassDeclaration

protected JmlClassDeclaration(TokenReference where,
                              boolean isWeakSubtype,
                              boolean[] interfaceWeaklyFlags,
                              JmlInvariant[] invariants,
                              JmlConstraint[] constraints,
                              JmlRepresentsDecl[] representsDecls,
                              JmlAxiom[] axioms,
                              JmlVarAssertion[] varAssertions,
                              JClassDeclarationWrapper delegee)

Constructs a new JML class declaration; clients should use factory method makeInstance instead. Because this class and the super class both hold aliases to the same delegee (to avoid casts during delegation), this constructor is private.

makeInstance

public static JmlClassDeclaration makeInstance(TokenReference where,
                                               long modifiers,
                                               String ident,
                                               CClassType superType,
                                               boolean isWeakSubtype,
                                               CClassType[] interfaces,
                                               boolean[] interfaceWeaklyFlags,
                                               ArrayList methods,
                                               ArrayList inners,
                                               JPhylum[] fieldsAndInits,
                                               JmlInvariant[] invariants,
                                               JmlConstraint[] constraints,
                                               JmlRepresentsDecl[] representsDecls,
                                               JmlAxiom[] axioms,
                                               JmlVarAssertion[] varAssertions,
                                               JavadocComment javadoc,
                                               JavaStyleComment[] comment,
                                               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 JTypeDeclarations 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

comment - regular java comments

See Also:

JMethodDeclarationType, JFieldDeclarationType, JClassBlock

isClass

public boolean isClass()

Returns true if this is a class declaration.

isWeakSubtype

public boolean isWeakSubtype()

isRacable

public boolean isRacable()

Is this class declaration runtime assertion checkable? This method is used by jmlc.

setRacable

public void setRacable()

Indicates that this class declaration is runtime assertion checkable. This method is used by jmlc.

setSuperClass

public void setSuperClass(CClassType superType)

Sets the super class

Specified by:

setSuperClass in interface JClassDeclarationType

setInterfaces

public void setInterfaces(CClassType[] interfaces)

Sets the super class

Specified by:

setInterfaces in interface JClassDeclarationType

createContext

public CClassContextType createContext(CContextType parent)

Creates a class context for this class declaration.

Specified by:

createContext in interface JClassDeclarationType

Parameters:

parent - the parent context or null

Returns:

returns a CClassContextType that represents this context

superName

public String superName()

Specified by:

superName in interface JClassDeclarationType

hasConstructor

public boolean hasConstructor()

Description copied from interface: JClassDeclarationType

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.

Specified by:

hasConstructor in interface JClassDeclarationType

accept

public void accept(MjcVisitor p)

Accepts the specified visitor.

Specified by:

accept in interface JMemberDeclarationType

Overrides:

accept in class JmlMemberDeclaration

Parameters:

p - the visitor

resolveSpecializers

public void resolveSpecializers(CContextType context)
                         throws PositionedError

Computes the values of specializer expressions used to dispatch on compile-time constants.

Specified by:

resolveSpecializers in interface JTypeDeclarationType

Parameters:

context - the context in which this class declaration appears

Throws:

PositionedError - if the check fails