org.jmlspecs.jmlrac
Class RacParser.RacMethodDeclaration

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.JmlMethodDeclaration
                          org.jmlspecs.jmlrac.RacParser.RacMethodDeclaration

All Implemented Interfaces:

Annotatable, Cloneable, Comparable, Constants, Constants, Constants, JMemberDeclarationType, JMethodDeclarationType, PhylumType, RacNode

Enclosing class:

RacParser

public static class RacParser.RacMethodDeclaration

extends JmlMethodDeclaration

implements JMethodDeclarationType, RacNode

A RAC node class for representing method declarations. A RAC method declaration is represented verbatim as a sequence of lines, where a line can be a string, an END_OF_LINE marker, and an object representing other RAC/JML node.

Nested Class Summary

 

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

 

Field Summary
private  int	indent           Indentation level of this statement node.
private  String	name           Name of this statement node.
private  List	pieces           The list of elements constituting this statement node.
private  PreValueVars.Entry	varDecl           The variable declaration to be piggyback with this code.

 

Fields inherited from class org.jmlspecs.checker.JmlMethodDeclaration

 

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
private	RacParser.RacMethodDeclaration(List pieces)           Creates a new instance.

 

Method Summary
void	accept(MjcVisitor p)           Accepts the specified visitor.
RacNode	incrIndent()           Increments indentation level of this node .
int	indent()           Returns the current indentation level of this node.
Iterator	iterator()           Returns an interator that iterates over elements (sequence of RAC nodes) of this node.
String	name()           Returns the name of this node.
void	setName(String name)           Sets the name of this node.
void	setVarDecl(PreValueVars.Entry varDecl)           Sets the variable declaration to be piggyback with this code.
PreValueVars.Entry	varDecl()           Returns the variable declaration associated with this code.

 

Methods inherited from class org.jmlspecs.checker.JmlMethodDeclaration

acceptDelegee, addParameter, body, checkAssignableFields, checkInterface, checkInterfaceType, checkOverriding, checkRefinementConsistency, combineSpecifications, compareTo, createSelfContext, findDeclWithBody, genCode, getAssignableFieldSet, getCombinedSpecification, getExceptions, getMinAssignableFieldSet, hasBody, hasSpecification, ident, isAbstract, isConstructor, isExecutableModel, isExternal, isFinalizer, isHelper, isModel, isNative, isOverriding, isPrivate, isPublic, isRacMethod, isSpecProtected, isSpecPublic, isStatic, jmlAccess, jmlchecks, makeInstance, methodSpecification, modifiers, modifiers2, overriddenMethods, parameters, resetFinalFieldStatusIfConstructor, resolveExtMethods, resolveSpecializers, resolveTopMethods, returnType, setBody, setIdent, setModifiers, setModifiers2, setParameters, setRefinementLinks, setRefiningMethod, setSpecstoCombinedSpecs, stringRepresentation, typecheck, usesMultipleDispatch

 

Methods inherited from class org.jmlspecs.checker.JmlMemberDeclaration

checkRefinedModifiers, findJavaFileInRefinement, genComments, getCClass, getCombinedVarAssertions, getField, getMethod, getMostRefined, getRefinedMember, getRefiningMember, inBinaryClassFile, inJavaFile, inners, isDeprecated, isRefined, isRefiningMember, javadocComment, setRefinedMember, setRefiningMember

 

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.JMethodDeclarationType

addParameter, body, checkInterface, checkInterfaceType, checkOverriding, compareTo, createSelfContext, getExceptions, hasBody, ident, isExternal, isOverriding, modifiers, overriddenMethods, parameters, resolveExtMethods, resolveSpecializers, resolveTopMethods, returnType, setModifiers, setParameters, typecheck, usesMultipleDispatch

 

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

 

Field Detail

varDecl

private PreValueVars.Entry varDecl

The variable declaration to be piggyback with this code.

name

private String name

Name of this statement node.

pieces

private List pieces

The list of elements constituting this statement node.

indent

private int indent

Indentation level of this statement node.

RacParser.RacMethodDeclaration

private RacParser.RacMethodDeclaration(List pieces)

Creates a new instance.

 requires pieces != null;
 

indent

public int indent()

Description copied from interface: RacNode

Returns the current indentation level of this node.

Specified by:

indent in interface RacNode

incrIndent

public RacNode incrIndent()

Description copied from interface: RacNode

Increments indentation level of this node .

Specified by:

incrIndent in interface RacNode

iterator

public Iterator iterator()

Description copied from interface: RacNode

Returns an interator that iterates over elements (sequence of RAC nodes) of this node.

Specified by:

iterator in interface RacNode

accept

public void accept(MjcVisitor p)

Accepts the specified visitor.

Specified by:

accept in interface JMemberDeclarationType

Overrides:

accept in class JmlMethodDeclaration

Parameters:

p - the visitor

name

public String name()

Description copied from interface: RacNode

Returns the name of this node.

Specified by:

name in interface RacNode

setName

public void setName(String name)

Description copied from interface: RacNode

Sets the name of this node.

Specified by:

setName in interface RacNode

setVarDecl

public void setVarDecl(PreValueVars.Entry varDecl)

Sets the variable declaration to be piggyback with this code.

Specified by:

setVarDecl in interface RacNode

See Also:

varDecl()

varDecl

public PreValueVars.Entry varDecl()

Returns the variable declaration associated with this code. This method is used to piggyback a variable declaration with this code.

Specified by:

varDecl in interface RacNode

See Also:

setVarDecl(PreValueVars.Entry)