JML

org.jmlspecs.checker
Class JmlMemberDeclaration

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.util.compiler.Phylum
          extended byorg.multijava.mjc.JPhylum
              extended byorg.jmlspecs.checker.JmlNode
                  extended byorg.jmlspecs.checker.JmlMemberDeclaration
All Implemented Interfaces:
Annotatable, Cloneable, Constants, Constants, Constants, JMemberDeclarationType, PhylumType
Direct Known Subclasses:
JmlBinaryMember, JmlFieldDeclaration, JmlMethodDeclaration, JmlTypeDeclaration

public abstract class JmlMemberDeclaration
extends JmlNode
implements JMemberDeclarationType

This type represents a java declaration in the syntax tree.


Nested Class Summary
 
Nested classes inherited from class org.jmlspecs.checker.JmlNode
JmlNode.DummyInitializerDeclaration
 
Field Summary
private  JMemberDeclaration delegee
           
protected  JmlMemberDeclaration refinedDecl
          The declaration that is refined by this declaration.
protected  JmlMemberDeclaration refiningDecl
          The declaration that refines this declaration.
 
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
JmlMemberDeclaration(TokenReference where, JMemberDeclaration delegee)
           
 
Method Summary
 void accept(MjcVisitor p)
          Accepts the specified visitor
 void checkRefinedModifiers(CContextType context, JmlMemberDeclaration member)
          Makes the general modifier consistency checks between refined declarations that are required of all refining members.
abstract  void combineSpecifications()
          Combine the specifications of this declaration with the specifications of the declarations it refines.
 String findJavaFileInRefinement()
           
 void genComments(MjcVisitor p)
          Generate the code in pure java form It is useful to debug and tune compilation process
 CClass getCClass()
           
 JmlMethodSpecification getCombinedSpecification()
          Returns null unless overridden by a subclass.
 JmlVarAssertion[] getCombinedVarAssertions()
          Returns null unless overridden by a subclass.
 CField getField()
           
 CMethod getMethod()
           
 JmlMemberDeclaration getMostRefined()
           
 JmlMemberDeclaration getRefinedMember()
           
 JmlMemberDeclaration getRefiningMember()
           
 boolean inBinaryClassFile()
          Returns true if this member comes from a '.class' file.
 boolean inJavaFile()
          Returns true if this member is declared in a '.java' file.
 ArrayList inners()
          Returns null unless overridden by a subclass.
 boolean isDeprecated()
          Returns true if this member is deprecated
 boolean isRefined()
           
 boolean isRefiningMember()
           
 JavadocComment javadocComment()
           
abstract  JmlMemberAccess jmlAccess()
           
 void setRefinedMember(JmlMemberDeclaration refinedDecl)
          Sets the field referencing the declaration refined by this declaration.
 void setRefiningMember(JmlMemberDeclaration refiningDecl)
          Sets the field referencing the declaration that refines this declaration.
 String 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.JMemberDeclarationType
ident, modifiers
 
Methods inherited from interface org.multijava.util.compiler.PhylumType
getTokenReference, setTokenReference
 

Field Detail

delegee

private JMemberDeclaration delegee

refinedDecl

protected JmlMemberDeclaration refinedDecl
The declaration that is refined by this declaration.


refiningDecl

protected JmlMemberDeclaration refiningDecl
The declaration that refines this declaration.

Constructor Detail

JmlMemberDeclaration

public JmlMemberDeclaration(TokenReference where,
                            JMemberDeclaration delegee)
Method Detail

isDeprecated

public boolean isDeprecated()
Returns true if this member is deprecated

Specified by:
isDeprecated in interface JMemberDeclarationType

getField

public CField getField()
Specified by:
getField in interface JMemberDeclarationType
Returns:
the field signature

getMethod

public CMethod getMethod()
Specified by:
getMethod in interface JMemberDeclarationType
Returns:
the method signature

getCClass

public CClass getCClass()
Specified by:
getCClass in interface JMemberDeclarationType
Returns:
the type signature

genComments

public void genComments(MjcVisitor p)
Generate the code in pure java form It is useful to debug and tune compilation process

Specified by:
genComments in interface JMemberDeclarationType
Parameters:
p - the printwriter into the code is generated

javadocComment

public JavadocComment javadocComment()
Specified by:
javadocComment in interface Annotatable

checkRefinedModifiers

public void checkRefinedModifiers(CContextType context,
                                  JmlMemberDeclaration member)
                           throws PositionedError
Makes the general modifier consistency checks between refined declarations that are required of all refining members.

Throws:
PositionedError

stringRepresentation

public String stringRepresentation()
Returns:
the name representation of this member.

isRefined

public boolean isRefined()
Returns:
true iff this member refined by another member.

isRefiningMember

public boolean isRefiningMember()
Returns:
true iff this member refines another member.

setRefinedMember

public void setRefinedMember(JmlMemberDeclaration refinedDecl)
Sets the field referencing the declaration refined by this declaration.


setRefiningMember

public void setRefiningMember(JmlMemberDeclaration refiningDecl)
Sets the field referencing the declaration that refines this declaration.


getRefinedMember

public JmlMemberDeclaration getRefinedMember()
Returns:
the member refined by this, or null if it does not refine another member.

getRefiningMember

public JmlMemberDeclaration getRefiningMember()
Returns:
the member that refines this, or null if it is not refined by another member.

getMostRefined

public JmlMemberDeclaration getMostRefined()

findJavaFileInRefinement

public String findJavaFileInRefinement()

jmlAccess

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

combineSpecifications

public abstract void combineSpecifications()
Combine the specifications of this declaration with the specifications of the declarations it refines.


inJavaFile

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


inBinaryClassFile

public boolean inBinaryClassFile()
Returns true if this member comes from a '.class' file.


getCombinedSpecification

public JmlMethodSpecification getCombinedSpecification()
Returns null unless overridden by a subclass. Returns null if it does not have any combined method specifications.


getCombinedVarAssertions

public JmlVarAssertion[] getCombinedVarAssertions()
Returns null unless overridden by a subclass. Returns null if it does not have any combined variable assertions.


inners

public ArrayList inners()
Returns null unless overridden by a subclass. Returns null if it does not have any inner type declarations.


accept

public void accept(MjcVisitor p)
Accepts the specified visitor

Specified by:
accept in interface JMemberDeclarationType
Overrides:
accept in class JmlNode
Parameters:
p - the visitor

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.