org.jmlspecs.checker
Class JmlMemberDeclaration

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Phylum
          org.multijava.mjc.JPhylum
              org.jmlspecs.checker.JmlNode
                  org.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.

JmlMemberDeclaration

public JmlMemberDeclaration(TokenReference where,
                            JMemberDeclaration delegee)

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