JML

org.jmlspecs.checker
Class JmlSourceMethod

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.mjc.CMember
          extended byorg.multijava.mjc.CMethod
              extended byorg.multijava.mjc.CSourceMethod
                  extended byorg.jmlspecs.checker.JmlSourceMethod
All Implemented Interfaces:
Cloneable, Comparable, Constants, Constants, Constants, org.jmlspecs.util.classfile.JmlMethodable, org.jmlspecs.util.classfile.JmlModifiable, SigSourceMember

public class JmlSourceMethod
extends CSourceMethod
implements org.jmlspecs.util.classfile.JmlMethodable, Constants

A class for representing JML method declaration in the signature forest. It includes the type signature of the method and operations for checking the method's applicability and whether it is more specfic than a given method.

Version:
$Revision: 1.34 $
Author:
Yoonsik Cheon

Field Summary
private  JmlMemberDeclaration methodAST
           
 
Fields inherited from class org.multijava.mjc.CSourceMethod
 
Fields inherited from class org.multijava.mjc.CMethod
declarationContext, generatefrom, needsPrivacyModifierRemoved, specArgs, synthetic, topConcreteMethod
 
Fields inherited from class org.multijava.mjc.CMember
 
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
JmlSourceMethod(CSourceMethod method)
           
JmlSourceMethod(MemberAccess access, String ident, CType returnType, CSpecializedType[] paramTypes, CClassType[] exceptions, CTypeVariable[] typevariables, boolean deprecated, JBlock body, CContextType declarationContext, JMethodDeclaration declarationASTNode)
           
 
Method Summary
protected  MethodInfo createCMethodInfo(int modifiers, String name, String type, String[] exceptions, CSourceMethod method, boolean deprecated, boolean synthetic)
          Creates a method info object.
protected  MethodInfo createMethodInfo(int modifiers, String name, String type, String[] exceptions, CodeInfo code, boolean deprecated, boolean synthetic)
          Creates a method info object.
 JmlMemberDeclaration getAST()
          Returns the AST for this method.
 JFormalParameter[] getASTparameters()
          Returns the parameters (AST's) for this method.
 String getGenericSignature()
           
 JmlSourceMethod getMostRefined()
          Returns the most refined declaration AST for this method.
 JmlMethodSpecification getSpecification()
          Returns the specification AST for this method.
 boolean inJavaFile()
          Returns true if the file in which this member is declared is a '.java' file.
 boolean isApplicable(String ident, CType recvType, CType[] actuals, CClassType[] args)
          Returns true if this method is applicable to a method call with the given identifier and actual (static) argument types.
 boolean isEffectivelyModel()
          Returns true iff this method should be treated as a model method; the method itself is model or it is declared inside a model class or interface.
 boolean isExecutableModel()
          Returns true if this method is a model method and can be executed by simply commenting out annotation markers.
 boolean isGhost()
          Returns always false.
 boolean isModel()
          Returns true iff this field is explicitly declared as model.
 boolean isPrivate()
          Returns true if this member is private.
 boolean isProtected()
          Returns true if this member is protected, including spec_protected in a JML specification scope.
 boolean isPublic()
          Returns true if this member is public, including spec_public in a JML specification scope.
 boolean isRefined()
           
 boolean isSpecProtected()
          Returns true if this method is spec_protected.
 boolean isSpecPublic()
          Returns true if this method is spec_public.
 JmlMemberAccess jmlAccess()
           
 void setAST(JmlMemberDeclaration methAST)
          Sets the AST for this method.
 
Methods inherited from class org.multijava.mjc.CSourceMethod
addFilteredDispatcher, ambiguousDispatcherClass, anchorClass, body, createCMethodInfo, createMethodInfo, declarationASTNode, dispatcherClassName, dispatcherMethod, dispatcherSignature, exceptionsAsStringArray, filteredDispatchers, functionNumber, genCode, genGenericFunctionInfo, genMethodInfo, getBody, getSignature, isTopLevelAbstractMethod, isUsed, markAsTopLevelAbstractMethod, nonEmptyMethodInfo, optimizingLevel, plantBodyBytecode, plantFunctionRef, plantOldFunctionRef, removePrivacyModifierIfNecessary, setDispatcherMethod, setParmsAndOptimizeCode, setUsed, toString
 
Methods inherited from class org.multijava.mjc.CMethod
apparentlySpecializes, apparentlySpecializes, apparentlySpecializes, bodyGenericSignature, bodyIdent, bodySignature, compareTo, declarationContext, equalParameters, equalParametersNoUniverses, equals, genDispatch, genGenFuncInvocation, getGenerateFrom, getMethod, getSpecArgs, getTypeVariable, hashCode, hasSameSignature, hasSameSignature, hasSameSignatureNoUniverses, isAbstract, isConstructor, isExternal, isGenericMethod, isInExternalGF, isLocalTo, isMixedPleomorphic, isMoreSpecificThan, isMoreSpecificThan, isMoreSpecificThan, isMoreSpecificThan, isMoreSpecificThan, isNative, isPure, isSynthetic, lookupTypeVariable, mmGenericSignature, mmSignature, overriddenMethodSet, parameters, parametersSize, plantMMInvocation, plantSelfArguments, purityWasChanged, receiverType, returnType, setGenerateFrom, setIDs, setIsMixedPleomorphic, setOverriddenMethodSet, setOverriddenMethodSet, setParameters, setReturnType, setSynthetic, setThrowables, specializes, swallowReceiver, throwables, topConcreteMethod, toString
 
Methods inherited from class org.multijava.mjc.CMember
access, addModifiers, deprecated, getCClass, getCCompilationUnit, getField, getIdent, getJavaName, getOwnerName, getQualNameWithSeparator, hasDefaultAccess, hasProtectedVisibilityIn, host, ident, isAccessibleFrom, isDeclaredNonNull, isDeprecated, isFinal, isLocalTo, isStatic, modifiers, owner, qualifiedName, setModifiers
 
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, finalize, getClass, notify, notifyAll, wait, wait, wait
 
Methods inherited from interface org.jmlspecs.util.classfile.JmlMethodable
isPure
 

Field Detail

methodAST

private JmlMemberDeclaration methodAST
Constructor Detail

JmlSourceMethod

public JmlSourceMethod(MemberAccess access,
                       String ident,
                       CType returnType,
                       CSpecializedType[] paramTypes,
                       CClassType[] exceptions,
                       CTypeVariable[] typevariables,
                       boolean deprecated,
                       JBlock body,
                       CContextType declarationContext,
                       JMethodDeclaration declarationASTNode)

JmlSourceMethod

public JmlSourceMethod(CSourceMethod method)
Method Detail

isEffectivelyModel

public boolean isEffectivelyModel()
Returns true iff this method should be treated as a model method; the method itself is model or it is declared inside a model class or interface.

Specified by:
isEffectivelyModel in interface org.jmlspecs.util.classfile.JmlModifiable

isModel

public boolean isModel()
Returns true iff this field is explicitly declared as model.

Specified by:
isModel in interface org.jmlspecs.util.classfile.JmlModifiable

isExecutableModel

public boolean isExecutableModel()
Returns true if this method is a model method and can be executed by simply commenting out annotation markers. This method must be called after typechecking.


isApplicable

public boolean isApplicable(String ident,
                            CType recvType,
                            CType[] actuals,
                            CClassType[] args)
Returns true if this method is applicable to a method call with the given identifier and actual (static) argument types. This method refines the inherited method to make model methods applicable only in specfication contexts (i.e., in spec scope).

Overrides:
isApplicable in class CMethod
Parameters:
ident - the identifier to match
recvType - receiver type
actuals - the method call static argument types
Returns:
true if this method is applicable
See Also:
CMethod#isApplicable(String, CType, CType[])

inJavaFile

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


isPublic

public boolean isPublic()
Returns true if this member is public, including spec_public in a JML specification scope.

Overrides:
isPublic in class CMember
See Also:
isProtected(), isPrivate()

isProtected

public boolean isProtected()
Returns true if this member is protected, including spec_protected in a JML specification scope.

Overrides:
isProtected in class CMember
See Also:
isPublic(), isPrivate()

isPrivate

public boolean isPrivate()
Returns true if this member is private. In a JML specification scope, it also means not being spec_public nor spec_protected.

Overrides:
isPrivate in class CMember
See Also:
isProtected(), isPublic()

isSpecPublic

public boolean isSpecPublic()
Returns true if this method is spec_public.


isSpecProtected

public boolean isSpecProtected()
Returns true if this method is spec_protected.


isGhost

public boolean isGhost()
Returns always false. This is a dumb method to implement the interface JmlMethodable.

Specified by:
isGhost in interface org.jmlspecs.util.classfile.JmlModifiable

getGenericSignature

public String getGenericSignature()
Overrides:
getGenericSignature in class CSourceMethod

getASTparameters

public JFormalParameter[] getASTparameters()
Returns the parameters (AST's) for this method.


setAST

public void setAST(JmlMemberDeclaration methAST)
Sets the AST for this method.


getAST

public JmlMemberDeclaration getAST()
Returns the AST for this method.


getMostRefined

public JmlSourceMethod getMostRefined()
Returns the most refined declaration AST for this method.


getSpecification

public JmlMethodSpecification getSpecification()
Returns the specification AST for this method.


isRefined

public boolean isRefined()

jmlAccess

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

createCMethodInfo

protected MethodInfo createCMethodInfo(int modifiers,
                                       String name,
                                       String type,
                                       String[] exceptions,
                                       CSourceMethod method,
                                       boolean deprecated,
                                       boolean synthetic)
Creates a method info object. This is a factory method that may be overridden by the subclass.


createMethodInfo

protected MethodInfo createMethodInfo(int modifiers,
                                      String name,
                                      String type,
                                      String[] exceptions,
                                      CodeInfo code,
                                      boolean deprecated,
                                      boolean synthetic)
Creates a method info object. This is a factory method that may be overridden by the subclass.


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.