JML

org.jmlspecs.checker
Class JmlMethodDeclaration

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.util.compiler.Phylum
          extended byorg.multijava.mjc.JPhylum
              extended byorg.jmlspecs.checker.JmlNode
                  extended byorg.jmlspecs.checker.JmlMemberDeclaration
                      extended byorg.jmlspecs.checker.JmlMethodDeclaration
All Implemented Interfaces:
Annotatable, Cloneable, Comparable, Constants, Constants, Constants, JMemberDeclarationType, JMethodDeclarationType, PhylumType
Direct Known Subclasses:
JmlConstructorDeclaration, RacParser.RacMethodDeclaration

public class JmlMethodDeclaration
extends JmlMemberDeclaration
implements JMethodDeclarationType

JmlMethodDeclaration.java

Version:
$Revision: 1.100 $
Author:
Curtis Clifton

Nested Class Summary
 
Nested classes inherited from class org.jmlspecs.checker.JmlNode
JmlNode.DummyInitializerDeclaration
 
Field Summary
private  JExpression[] accessedFields
           
private  JmlAssignableFieldSet assignableFieldSet
           
private  JExpression[] assignedFields
           
private  JExpression[] calledMethods
           
private  JmlMethodSpecification combinedMethodSpecification
           
private  JMethodDeclaration delegee
           
private  JmlMethodSpecification methodSpecification
           
private  JmlAssignableFieldSet minAssignableFieldSet
           
private  int modifiers2
           
private  CMethodSet overriddenMethodSet
           
private  String thisStringRep
           
 
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.mjc.JPhylum
EMPTY
 
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_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
protected JmlMethodDeclaration(TokenReference where, JmlMethodSpecification methodSpecification, JMethodDeclaration delegee)
           
 
Method Summary
 void accept(MjcVisitor p)
          Accepts the specified visitor.
 void acceptDelegee(MjcVisitor p)
           
private  void accumulateNonNullStats(JmlContext context)
           
 void addParameter(JFormalParameter param)
          Adds an additional formal parameter to this method, appending it to the end of the existing parameter list.
 JBlock body()
          WMD TODO remove WMD TODO remove
 void checkAssignableFields(JmlDataGroupMemberMap dataGroupMap)
           
 CMember checkInterface(CContextType context)
          Checks the basic interfaces to make sure things generally look OK.
 CSourceMethod checkInterfaceType(CContextType context, MemberAccess access, String ident)
          Performs the interface checks that are common to all sorts of methods.
private  void checkMathModes(CContextType context)
           
private  void checkMethodSpecification(CClassContextType cContext, JmlSourceMethod self)
           
private  void checkNullityAdjustType(CContextType context)
          Ensures that at most one nullity modifier is used and that it is applied to a reference type.
private  void checkNullityForOverriddenMethods(CContextType context, JmlSourceMethod self)
           
 void checkOverriding(CContextType context, CMethodSet superMethods)
          Checks that this method appropriately overrides the given superclass methods.
private  void checkParamNullity(CContextType context, JmlSourceMethod self, JmlSourceMethod overriddenMeth)
          Ensure that nullity modifiers of the parameter(s) of self exactly match with the corresponding parameter(s) of overriddenMeth, a method that it overrides.
 void checkRefinementConsistency(CContextType context)
           
private  void checkResultNullity(CContextType context, JmlSourceMethod self, JmlSourceMethod overriddenMeth)
          Ensure that nullity modifiers of the (return type of) self are consistent with overriddenMeth, a method that it overrides.
 void combineSpecifications()
           
 int compareTo(Object o)
          Compares this method to a given method and returns 0 if the methods belong to the same generic function, otherwise returns -1 or +1 to sort the methods.
 CMethodContextType createSelfContext(CClassContextType parent)
          Creates a context for this method declaration AST node.
 JmlMethodDeclaration findDeclWithBody()
          Returns the method declaration in the refinement chain that has a body.
 void genCode(CodeSequence code)
          Generates a sequence of bytecodes
 JmlAssignableFieldSet getAssignableFieldSet()
          Returns the maximal set of fields that can be assigned to by this method (takes the union of the assignable clauses from all specification cases).
 JmlMethodSpecification getCombinedSpecification()
          Returns the method specifications of this member declaration combined with the specifications of those it refines.
 CClassType[] getExceptions()
           
 JmlAssignableFieldSet getMinAssignableFieldSet(JmlDataGroupMemberMap dataGroupMap)
          Returns the minimal set of fields that can be assigned to by this method (takes the intersection of the assignable clauses from the specification cases).
 boolean hasBody()
          Indicates whether this method declaration has a body.
 boolean hasSpecification()
          Indicates whether the method declaration represented by this has an explicit specification.
 String ident()
           
 boolean isAbstract()
          Returns true if this method is a abstract method.
 boolean isConstructor()
          Returns true if this method is a constructor.
 boolean isDeclaredNonNull()
           
 boolean isExecutableModel()
          Returns true if this method is a model method and can be executed by simply commenting out annotation markers.
 boolean isExternal()
          Indicates whether this member is external.
 boolean isFinalizer()
          Returns true if this method is a finalizer.
 boolean isHelper()
          Returns true if this method is a helper.
 boolean isModel()
          Returns true if this method is a model method.
 boolean isNative()
          Returns true if this method is a native method.
 boolean isOverriding()
          Return true if this method declaration overrides any of its superclass (or interfaces) method declarations.
 boolean isPrivate()
          Returns true if this method is a private method.
 boolean isPublic()
          Returns true if this method is a public method.
 boolean isRacMethod()
          Returns true if this method is a RAC method.
 boolean isSpecProtected()
          Returns true if this method is spec_protected.
 boolean isSpecPublic()
          Returns true if this method is spec_public.
 boolean isStatic()
          Returns true if this method is a static method.
 JmlMemberAccess jmlAccess()
           
 void jmlchecks(CContextType context, JmlSourceMethod self)
           
static JmlMethodDeclaration makeInstance(TokenReference where, long modifiers, CTypeVariable[] typevariables, CType returnType, String ident, JFormalParameter[] parameters, CClassType[] exceptions, JBlock body, JavadocComment javadoc, JavaStyleComment[] comments, JmlMethodSpecification methodSpecification)
           
 JmlMethodSpecification methodSpecification()
           
 long modifiers()
           
 int modifiers2()
           
 CMethodSet overriddenMethods()
          Return the set of methods that are directly overriden (specialized) by this method declaration.
 JFormalParameter[] parameters()
           
protected  void resetFinalFieldStatusIfConstructor(CClassContextType context)
          Resets the final field definite assignment info if this is a constructor.
 void resolveExtMethods(CContextType context)
          Makes sure that all in-scope external generic functions are added to the appropriate augmentation maps before top method searches occur in later passes.
 void resolveSpecializers(CContextType context)
          Computes the values of specializer expressions used to dispatch on compile-time constants.
 void resolveTopMethods()
          Finds the top method of every declared method.
 CType returnType()
          Returns the return type of this method declaration.
 void setBody(JBlock body)
          Set the body of this method.
 void setIdent(String name)
          Set the name of this method; used by RAC.
 void setModifiers(long modifiers)
          Sets the modifiers of this method declaration
 void setModifiers2(int modifiers2)
          Sets the modifiers2 of this method declaration
 void setParameters(JFormalParameter[] parameters)
           
protected  void setRefinementLinks()
          Calculates and returns the method refined by this method.
protected  void setRefiningMethod(JmlMethodDeclaration refiningMethod)
           
 void setSpecstoCombinedSpecs()
           
 String stringRepresentation()
           
 void typecheck(CContextType context)
          Typechecks this method declaration.
 CTypeVariable[] typevariables()
           
 boolean usesMultipleDispatch()
          Indicates whether this method uses multiple dispatch
 
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.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

delegee

private JMethodDeclaration delegee

methodSpecification

private JmlMethodSpecification methodSpecification

overriddenMethodSet

private CMethodSet overriddenMethodSet

combinedMethodSpecification

private JmlMethodSpecification combinedMethodSpecification

assignableFieldSet

private JmlAssignableFieldSet assignableFieldSet

minAssignableFieldSet

private JmlAssignableFieldSet minAssignableFieldSet

assignedFields

private JExpression[] assignedFields

accessedFields

private JExpression[] accessedFields

calledMethods

private JExpression[] calledMethods

thisStringRep

private String thisStringRep

modifiers2

private int modifiers2
Constructor Detail

JmlMethodDeclaration

protected JmlMethodDeclaration(TokenReference where,
                               JmlMethodSpecification methodSpecification,
                               JMethodDeclaration delegee)
Method Detail

makeInstance

public static JmlMethodDeclaration makeInstance(TokenReference where,
                                                long modifiers,
                                                CTypeVariable[] typevariables,
                                                CType returnType,
                                                String ident,
                                                JFormalParameter[] parameters,
                                                CClassType[] exceptions,
                                                JBlock body,
                                                JavadocComment javadoc,
                                                JavaStyleComment[] comments,
                                                JmlMethodSpecification methodSpecification)

hasBody

public boolean hasBody()
Indicates whether this method declaration has a body.

Specified by:
hasBody in interface JMethodDeclarationType

findDeclWithBody

public JmlMethodDeclaration findDeclWithBody()
Returns the method declaration in the refinement chain that has a body.


hasSpecification

public boolean hasSpecification()
Indicates whether the method declaration represented by this has an explicit specification.


methodSpecification

public JmlMethodSpecification methodSpecification()

parameters

public JFormalParameter[] parameters()
Specified by:
parameters in interface JMethodDeclarationType

setParameters

public void setParameters(JFormalParameter[] parameters)
Specified by:
setParameters in interface JMethodDeclarationType

typevariables

public CTypeVariable[] typevariables()

addParameter

public void addParameter(JFormalParameter param)
Adds an additional formal parameter to this method, appending it to the end of the existing parameter list.

 also
   requires param != null;
 

Specified by:
addParameter in interface JMethodDeclarationType

ident

public String ident()
Specified by:
ident in interface JMethodDeclarationType

returnType

public CType returnType()
Returns the return type of this method declaration. If this method declaration is a constructor, the returned object is the object denoting the void type.

Specified by:
returnType in interface JMethodDeclarationType

getExceptions

public CClassType[] getExceptions()
Specified by:
getExceptions in interface JMethodDeclarationType

modifiers

public long modifiers()
Specified by:
modifiers in interface JMethodDeclarationType

setModifiers

public void setModifiers(long modifiers)
Sets the modifiers of this method declaration

Specified by:
setModifiers in interface JMethodDeclarationType

isHelper

public boolean isHelper()
Returns true if this method is a helper.


isAbstract

public boolean isAbstract()
Returns true if this method is a abstract method.


isStatic

public boolean isStatic()
Returns true if this method is a static method.


isSpecPublic

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


isSpecProtected

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


isPublic

public boolean isPublic()
Returns true if this method is a public method.


isPrivate

public boolean isPrivate()
Returns true if this method is a private method.


isNative

public boolean isNative()
Returns true if this method is a native method.


isModel

public boolean isModel()
Returns true if this method is a model method.


isConstructor

public boolean isConstructor()
Returns true if this method is a constructor.


isFinalizer

public boolean isFinalizer()
Returns true if this method is a finalizer.


isDeclaredNonNull

public boolean isDeclaredNonNull()
Specified by:
isDeclaredNonNull in interface JMethodDeclarationType

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.


body

public JBlock body()
Description copied from interface: JMethodDeclarationType
WMD TODO remove WMD TODO remove

Specified by:
body in interface JMethodDeclarationType

setIdent

public void setIdent(String name)
Set the name of this method; used by RAC.


setBody

public void setBody(JBlock body)
Set the body of this method.


isOverriding

public boolean isOverriding()
Return true if this method declaration overrides any of its superclass (or interfaces) method declarations.

Specified by:
isOverriding in interface JMethodDeclarationType

overriddenMethods

public CMethodSet overriddenMethods()
Return the set of methods that are directly overriden (specialized) by this method declaration.

Specified by:
overriddenMethods in interface JMethodDeclarationType

usesMultipleDispatch

public boolean usesMultipleDispatch()
Indicates whether this method uses multiple dispatch

Specified by:
usesMultipleDispatch in interface JMethodDeclarationType
Returns:
true iff a parameter of this method has a dynamic dispatch annotation or, for an external method, this methods receiver is of a different type than the generic function's top method

compareTo

public int compareTo(Object o)
              throws ClassCastException
Compares this method to a given method and returns 0 if the methods belong to the same generic function, otherwise returns -1 or +1 to sort the methods. This comparator is used to separate methods by generic function in the MJGenericFunctionDispatcher class.

Specified by:
compareTo in interface JMethodDeclarationType
Parameters:
o - the object to be compared against, must be a JMethodDeclarationType
Returns:
-1, +1, or 0
Throws:
ClassCastException - if o is not an instance of CType

isExternal

public boolean isExternal()
Indicates whether this member is external. Always returns false for this but is overridden for external subclasses.

Specified by:
isExternal in interface JMethodDeclarationType
Returns:
a flag indicating whether this member is external

jmlAccess

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

checkInterface

public CMember checkInterface(CContextType context)
                       throws PositionedError
Checks the basic interfaces to make sure things generally look OK. This pass gathers information about the type signatures of everything (imported class files, classes being compiled, methods, fields, etc...) needed for the later passes. This information is stored in a context hierarchy that is bound to the AST.

Specified by:
checkInterface in interface JMethodDeclarationType
Returns:
a source code representation of the method, iff sub tree is correct enough to check code
Throws:
PositionedError - an error with reference to the source file

checkInterfaceType

public CSourceMethod checkInterfaceType(CContextType context,
                                        MemberAccess access,
                                        String ident)
                                 throws PositionedError
Performs the interface checks that are common to all sorts of methods. Gets the signatures of the return type, parameters and exceptions, and generates the source code representation, CSourceMethod.

Specified by:
checkInterfaceType in interface JMethodDeclarationType
Parameters:
context - the context in which this method appears
access - the member access for this method
ident - the method name (passed as a parameter instead of using the field to properly handle constructors where the field is the class name but ident is <init>
Returns:
a source code representation of the method, iff sub tree is correct enough to check code
Throws:
PositionedError - an error with reference to the source file

resolveExtMethods

public void resolveExtMethods(CContextType context)
Description copied from interface: JMethodDeclarationType
Makes sure that all in-scope external generic functions are added to the appropriate augmentation maps before top method searches occur in later passes.

Specified by:
resolveExtMethods in interface JMethodDeclarationType

resolveTopMethods

public void resolveTopMethods()
                       throws PositionedError
Finds the top method of every declared method. Called after the checkInitializers pass. This cannot be done before then because the external generic function mappings are not complete until the end of the checkInterface pass and the constant value specializers are not known until after the checkInitializers pass. This must be done before the typecheck pass so that all specialized argument positions for generic functions are known for ambiguity checking.

Specified by:
resolveTopMethods in interface JMethodDeclarationType
Throws:
PositionedError

createSelfContext

public CMethodContextType createSelfContext(CClassContextType parent)
Creates a context for this method declaration AST node.

Specified by:
createSelfContext in interface JMethodDeclarationType
Parameters:
parent - the parent context

resolveSpecializers

public void resolveSpecializers(CContextType context)
                         throws PositionedError
Computes the values of specializer expressions used to dispatch on compile-time constants.

Specified by:
resolveSpecializers in interface JMethodDeclarationType
Parameters:
context - the context in which this class declaration appears
Throws:
PositionedError - if the check fails

typecheck

public void typecheck(CContextType context)
               throws PositionedError
Typechecks this method declaration. Mutates the context to record the information gathered during the checks.

Specified by:
typecheck in interface JMethodDeclarationType
Parameters:
context - the context in which this method appears
Throws:
PositionedError - if the checks fail and the failure cannot be recovered from

checkNullityAdjustType

private void checkNullityAdjustType(CContextType context)
                             throws PositionedError
Ensures that at most one nullity modifier is used and that it is applied to a reference type. Also set the return type of this method to non-null if appropriate.

Throws:
PositionedError

checkNullityForOverriddenMethods

private void checkNullityForOverriddenMethods(CContextType context,
                                              JmlSourceMethod self)
                                       throws PositionedError
Throws:
PositionedError

checkParamNullity

private void checkParamNullity(CContextType context,
                               JmlSourceMethod self,
                               JmlSourceMethod overriddenMeth)
                        throws PositionedError
Ensure that nullity modifiers of the parameter(s) of self exactly match with the corresponding parameter(s) of overriddenMeth, a method that it overrides.

Throws:
PositionedError

checkResultNullity

private void checkResultNullity(CContextType context,
                                JmlSourceMethod self,
                                JmlSourceMethod overriddenMeth)
                         throws PositionedError
Ensure that nullity modifiers of the (return type of) self are consistent with overriddenMeth, a method that it overrides. If inconsistent, then report a problem to the user.

Throws:
PositionedError

checkMathModes

private void checkMathModes(CContextType context)
                     throws PositionedError
Throws:
PositionedError

checkMethodSpecification

private void checkMethodSpecification(CClassContextType cContext,
                                      JmlSourceMethod self)
                               throws PositionedError
Throws:
PositionedError

genCode

public void genCode(CodeSequence code)
Generates a sequence of bytecodes

Parameters:
code - the code list

resetFinalFieldStatusIfConstructor

protected void resetFinalFieldStatusIfConstructor(CClassContextType context)
Resets the final field definite assignment info if this is a constructor.


jmlchecks

public void jmlchecks(CContextType context,
                      JmlSourceMethod self)
               throws PositionedError
Throws:
PositionedError

getAssignableFieldSet

public JmlAssignableFieldSet getAssignableFieldSet()
Returns the maximal set of fields that can be assigned to by this method (takes the union of the assignable clauses from all specification cases).


getMinAssignableFieldSet

public JmlAssignableFieldSet getMinAssignableFieldSet(JmlDataGroupMemberMap dataGroupMap)
Returns the minimal set of fields that can be assigned to by this method (takes the intersection of the assignable clauses from the specification cases). This set is used in the checking of assignable fields when there are calls in the method body.


checkAssignableFields

public void checkAssignableFields(JmlDataGroupMemberMap dataGroupMap)

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

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

accept

public void accept(MjcVisitor p)
Accepts the specified visitor.

Specified by:
accept in interface JMemberDeclarationType
Overrides:
accept in class JmlMemberDeclaration
Parameters:
p - the visitor

acceptDelegee

public void acceptDelegee(MjcVisitor p)

stringRepresentation

public String stringRepresentation()
Overrides:
stringRepresentation in class JmlMemberDeclaration
Returns:
the name representation of this member.

setRefinementLinks

protected void setRefinementLinks()
Calculates and returns the method refined by this method. Caches the result for later calls to #getRefinedMember(). Also sets the refining method of the method returned so they are linked to each other.


setRefiningMethod

protected void setRefiningMethod(JmlMethodDeclaration refiningMethod)

checkRefinementConsistency

public void checkRefinementConsistency(CContextType context)
                                throws PositionedError
Throws:
PositionedError

setSpecstoCombinedSpecs

public void setSpecstoCombinedSpecs()

getCombinedSpecification

public JmlMethodSpecification getCombinedSpecification()
Returns the method specifications of this member declaration combined with the specifications of those it refines. Returns null if it does not have any combined method specifications.

Overrides:
getCombinedSpecification in class JmlMemberDeclaration

combineSpecifications

public void combineSpecifications()
Description copied from class: JmlMemberDeclaration
Combine the specifications of this declaration with the specifications of the declarations it refines.


setModifiers2

public void setModifiers2(int modifiers2)
Sets the modifiers2 of this method declaration


modifiers2

public int modifiers2()

isRacMethod

public boolean isRacMethod()
Returns true if this method is a RAC method. Such kind of method needs to be printed in RAC instead of in mjc


accumulateNonNullStats

private void accumulateNonNullStats(JmlContext context)
                             throws PositionedError
Throws:
PositionedError

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.