org.jmlspecs.checker
Class JmlSourceMethod

java.lang.Object
  org.multijava.util.Utils
      org.multijava.mjc.CMember
          org.multijava.mjc.CMethod
              org.multijava.mjc.CSourceMethod
                  org.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

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)

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.