org.jmlspecs.checker
Class JmlSigBinaryMethod

java.lang.Object
  org.multijava.util.Utils
      org.multijava.mjc.CMember
          org.multijava.mjc.CMethod
              org.multijava.mjc.CBinaryMethod
                  org.jmlspecs.checker.JmlSigBinaryMethod

All Implemented Interfaces:

Cloneable, Comparable, Constants, Constants, Constants, org.jmlspecs.util.classfile.JmlModifiable

public class JmlSigBinaryMethod

extends CBinaryMethod

implements org.jmlspecs.util.classfile.JmlModifiable, Constants

A class to represent JML method declaratons read from bytecode files.

Author:

Yoonsik

Field Summary

 

Fields inherited from class org.multijava.mjc.CBinaryMethod

 

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

JmlSigBinaryMethod(CClass owner, org.jmlspecs.util.classfile.JmlMethodInfo methodInfo, CContextType declarationContext)           Creates a new instance by using the given method info methodInfo.

 

Method Summary
private static JmlMemberAccess	createMemberAccess(CClass owner, org.jmlspecs.util.classfile.JmlMethodInfo methodInfo)           Creates a JML member access for the given JML method info object methodInfo.
boolean	isApplicable(String ident, CType recvType, CType[] actuals)           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 field should be treated as a model method; the method itself is defined as model (or ghost) or it is defined in a model class or interface.
boolean	isGhost()           Returns true iff this method is explicitly declared as ghost.
boolean	isModel()           Returns true iff this method 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	isPure()           Returns true if this method is pure.
boolean	isSpecProtected()           Returns true if this method is spec_protected.
boolean	isSpecPublic()           Returns true if this method is spec_public.

 

Methods inherited from class org.multijava.mjc.CBinaryMethod

ambiguousDispatcherClass, anchorClass, checkTypes, dispatcherSignature, functionNumber, plantFunctionRef, plantOldFunctionRef, registerVisibleTypes, resolveTops, swallowReceivers

 

Methods inherited from class org.multijava.mjc.CMethod

apparentlySpecializes, apparentlySpecializes, apparentlySpecializes, bodyGenericSignature, bodyIdent, bodySignature, compareTo, declarationContext, equalParameters, equalParametersNoUniverses, equals, genDispatch, genGenericFunctionInfo, genGenFuncInvocation, genMethodInfo, getGenerateFrom, getGenericSignature, getMethod, getSignature, getSpecArgs, getTypeVariable, hashCode, hasSameSignature, hasSameSignature, hasSameSignatureNoUniverses, isAbstract, isApplicable, isConstructor, isExternal, isGenericMethod, isInExternalGF, isLocalTo, isMixedPleomorphic, isMoreSpecificThan, isMoreSpecificThan, isMoreSpecificThan, isMoreSpecificThan, isMoreSpecificThan, isNative, 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, 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

 

Constructor Detail

JmlSigBinaryMethod

public JmlSigBinaryMethod(CClass owner,
                          org.jmlspecs.util.classfile.JmlMethodInfo methodInfo,
                          CContextType declarationContext)

Creates a new instance by using the given method info methodInfo.

isModel

public boolean isModel()

Returns true iff this method is explicitly declared as model.

Specified by:

isModel in interface org.jmlspecs.util.classfile.JmlModifiable

isGhost

public boolean isGhost()

Returns true iff this method is explicitly declared as ghost.

Specified by:

isGhost in interface org.jmlspecs.util.classfile.JmlModifiable

isEffectivelyModel

public boolean isEffectivelyModel()

Returns true iff this field should be treated as a model method; the method itself is defined as model (or ghost) or it is defined in a model class or interface.

Specified by:

isEffectivelyModel in interface org.jmlspecs.util.classfile.JmlModifiable

isApplicable

public boolean isApplicable(String ident,
                            CType recvType,
                            CType[] actuals)

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

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[])

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.

isPure

public boolean isPure()

Returns true if this method is pure. A method is pure if it is annotated with the JML pure modifier or it inherits pureness from its owner or supertypes. A non-static method (including a constructor) is pure if its owner class or interface is pure, or if it overrides a pure method inherited from supertypes (classes and intefaces).

Overrides:

isPure in class CMethod

createMemberAccess

private static JmlMemberAccess createMemberAccess(CClass owner,
                                                  org.jmlspecs.util.classfile.JmlMethodInfo methodInfo)

Creates a JML member access for the given JML method info object methodInfo.