Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.checker
Class JMethodDeclarationWrapper

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.util.compiler.Phylum
          extended byorg.multijava.mjc.JPhylum
              extended byorg.multijava.mjc.JMemberDeclaration
                  extended byorg.multijava.mjc.JMethodDeclaration
                      extended byorg.jmlspecs.checker.JMethodDeclarationWrapper
All Implemented Interfaces:
Annotatable, Cloneable, Comparable, Constants, Constants, Constants, JMemberDeclarationType, JMethodDeclarationType, PhylumType
public class JMethodDeclarationWrapper
extends JMethodDeclaration
implements Constants

A class representing a method declaration in the syntax tree. This class provides JML-specific handling of method declarations by overriding several inherited methods. For example, the makeMethodSignature method now creates and returns an object of JmlSourceMethod instead of CSourceMethod, that can handle JML-specific behaviors (e.g., spec_public-ness).

Version:
$Revision: 1.13 $
Author:
Yoonsik Cheon

Field Summary
 
Fields inherited from class org.multijava.mjc.JMethodDeclaration
typevariables
 
Fields inherited from class org.multijava.mjc.JMemberDeclaration
 
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
JMethodDeclarationWrapper(TokenReference where, long modifiers, CType returnType, String ident, JFormalParameter[] parameters, CClassType[] exceptions, JBlock body, JavadocComment javadoc, JavaStyleComment[] comments)
          Construct a node in the parsing tree This method is directly called by the parser
 
Method Summary
 void checkOverriding(CContextType context, CMethodSet superMethods)
          Checks that this method appropriately overrides the given superclass methods.
 boolean isModel()
          Returns true iff this method is abstract or is a model method.
protected  MemberAccess makeMemberAccess(CContextType context, CClass owner)
           
protected  CSourceMethod makeMethodSignature(CContextType context, MemberAccess access, String ident, CSpecializedType[] parameterTypes)
          Generates the signature object for this method declaration.
protected  boolean noBodyOK(CContextType context, CMethod self)
           
 void typecheck(CContextType context)
          Typechecks this method declaration.
 
Methods inherited from class org.multijava.mjc.JMethodDeclaration
accept, addBridge, addParameter, body, checkInterface, checkInterfaceType, compareTo, createExtendedClassContext, createSelfContext, genCode, getExceptions, hasBody, ident, isExternal, isOverriding, modifiers, overriddenMethods, parameters, resolveExtMethods, resolveSpecializers, resolveTopMethods, returnType, setBody, setIdent, setModifiers, setParameters, toString, usesMultipleDispatch
 
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, wait, wait, wait
 
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
 

Constructor Detail

JMethodDeclarationWrapper

public JMethodDeclarationWrapper(TokenReference where,
                                 long modifiers,
                                 CType returnType,
                                 String ident,
                                 JFormalParameter[] parameters,
                                 CClassType[] exceptions,
                                 JBlock body,
                                 JavadocComment javadoc,
                                 JavaStyleComment[] comments)
Construct a node in the parsing tree This method is directly called by the parser

Parameters:
where - the line of this node in the source code
modifiers - list of modifiers
returnType - the return type of this method
ident - the name of this method
parameters - the parameters of this method
exceptions - the exceptions throw by this method
body - the body of this method
javadoc - javadoc comments, including whether this method is deprecated
comments - regular java style comments
Method Detail

makeMethodSignature

protected CSourceMethod makeMethodSignature(CContextType context,
                                            MemberAccess access,
                                            String ident,
                                            CSpecializedType[] parameterTypes)
Generates the signature object for this method declaration. This method overrides the inherited method to generate JML-specific signature object, i.e., an instance of JmlSourceMethod.

Overrides:
makeMethodSignature in class JMethodDeclaration

makeMemberAccess

protected MemberAccess makeMemberAccess(CContextType context,
                                        CClass owner)
Overrides:
makeMemberAccess in class JMethodDeclaration

isModel

public boolean isModel()
Returns true iff this method is abstract or is a model method.

noBodyOK

protected boolean noBodyOK(CContextType context,
                           CMethod self)
Overrides:
noBodyOK in class JMethodDeclaration

checkOverriding

public void checkOverriding(CContextType context,
                            CMethodSet superMethods)
                     throws PositionedError
Checks that this method appropriately overrides the given superclass methods. The checks are those given in JLS2, section 8.4.6.3 and CLCM 00 4.1.3.1 (extended per Clifton's thesis). 

 also requires context != null && superMethods != null;

Specified by:
checkOverriding in interface JMethodDeclarationType
Overrides:
checkOverriding in class JMethodDeclaration
Parameters:
context - the context in which this appears
superMethods - the super types methods that this may override.
Throws:
PositionedError - if a check fails

typecheck

public void typecheck(CContextType context)
               throws PositionedError
Description copied from class: JMethodDeclaration
Typechecks this method declaration. Mutates the context to record the information gathered during the checks.

Specified by:
typecheck in interface JMethodDeclarationType
Overrides:
typecheck in class JMethodDeclaration
Parameters:
context - the context in which this method appears
Throws:
PositionedError - if the checks fail and the failure cannot be recovered from
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
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.