org.jmlspecs.checker
Class JmlMethodDeclaration

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Phylum
          org.multijava.mjc.JPhylum
              org.jmlspecs.checker.JmlNode
                  org.jmlspecs.checker.JmlMemberDeclaration
                      org.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.84 $

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.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
protected	JmlMethodDeclaration(TokenReference where, JmlMethodSpecification methodSpecification, JMethodDeclaration delegee)

 

Method Summary
void	accept(MjcVisitor p)           Accepts the specified visitor.
void	acceptDelegee(MjcVisitor p)
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	checkMethodSpecification(CClassContextType cContext, JmlSourceMethod self)
void	checkOverriding(CContextType context, CMethodSet superMethods)           Checks that this method appropriately overrides the given superclass methods.
void	checkRefinementConsistency(CContextType context)
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	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, 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.
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

JmlMethodDeclaration

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

makeInstance

public static JmlMethodDeclaration makeInstance(TokenReference where,
                                                long modifiers,
                                                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

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.

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

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