jml2b.structure.bytecode
Class ClassMethod

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.java.ParsedItem
          jml2b.structure.java.NamedNode
              jml2b.structure.java.Declaration
                  jml2b.structure.AMethod
                      jml2b.structure.bytecode.ClassMethod

All Implemented Interfaces:

IModifiers, IModifiesField, jml.JmlDeclParserTokenTypes, Linkable, java.io.Serializable

Direct Known Subclasses:

ClassDefaultConstructor

public class ClassMethod

extends AMethod

implements IModifiers

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

Fields inherited from class jml2b.structure.java.NamedNode

garbage, nameIndex

Fields inherited from interface jml2b.link.Linkable

STATE_LINKED, STATE_LINKED_STATEMENTS, STATE_LINKED_TYPE_CHECKED, STATE_UNLINKED

Fields inherited from interface jml.JmlDeclParserTokenTypes

ABRUPT_BEHAVIOR, ACCESSIBLE, ACCESSIBLE_KEYWORD, ACCESSIBLE_REDUNDANTLY, ACCESSIBLE_SEQ, ADDITIVE_ASSIGNMENT_OP, ADDITIVE_OP, AFFIRM_KEYWORD, ALSO, AND, ARRAY_DECLARATOR, ASGNABLE_SEQ, ASSERT, ASSERT_REDUNDANTLY, ASSIGN, ASSIGNABLE, ASSIGNABLE_KEYWORD, ASSIGNABLE_REDUNDANTLY, ASSUME, ASSUME_KEYWORD, ASSUME_REDUNDANTLY, AXIOM, BACKWARD_IMPLIES, BADCHAR, BAND, BAND_ASSIGN, BEHAVIOR, BITWISE_ASSIGNMENT_OP, BITWISE_OP, BNOT, BOR, BOR_ASSIGN, BREAKS, BREAKS_KEYWORD, BREAKS_REDUNDANTLY, BREAKS_SEQ, BSR, BSR_ASSIGN, BXOR, BXOR_ASSIGN, CALLABLE, CALLABLE_KEYWORD, CALLABLE_REDUNDANTLY, CALLABLE_SEQ, CASE, CAST, CHAR_LITERAL, CHOOSE, CHOOSE_IF, COLON, COMMA, CONJOINABLE_SPEC, CONSTRAINT, CONSTRAINT_KEYWORD, CONSTRAINT_REDUNDANTLY, CONSTRUCTOR, CONT_SEQ, CONTINUES, CONTINUES_KEYWORD, CONTINUES_REDUNDANTLY, DEC, DECREASES, DECREASES_REDUNDANTLY, DECREASING, DECREASING_KEYWORD, DECREASING_REDUNDANTLY, DEPENDS, DEPENDS_KEYWORD, DEPENDS_REDUNDANTLY, DIM_EXPRS, DIMS, DINFORMALLY, DIV, DIV_ASSIGN, DIV_SEQ, DIVERGES, DIVERGES_KEYWORD, DIVERGES_REDUNDANTLY, DOC_ATSIGN, DOC_ATSIGN_KEYWORD, DOC_AUTHOR, DOC_COMMENT, DOC_COMMENT_START, DOC_DEPRECATED, DOC_EXCEPTION, DOC_JML_SPECS, DOC_NL_WS, DOC_NON_EMPTY_TEXTLINE, DOC_NON_NL_WS, DOC_PARAM, DOC_RETURN, DOC_SEE, DOC_SERIAL, DOC_SERIALDATA, DOC_SERIALFIELD, DOC_SINCE, DOC_THROWS, DOC_UNKNOWN_KEYWORD, DOC_VERSION, DOT, DOT_DOT, ELSE, ENS_SEQ, ENSURES, ENSURES_KEYWORD, ENSURES_REDUNDANTLY, EOF, EQUAL, EQUALITY_OP, EQUIV, EQUIVALENCE_OP, ESC, EXAMPLE, EXCEPTIONAL_BEHAVIOR, EXCEPTIONAL_EXAMPLE, EXPONENT, EXSURES, EXSURES_REDUNDANTLY, EXT_ALSO, EXT_AND, FLOAT_SUFFIX, FOR, FOR_EXAMPLE, FOR_INIT, FOR_TEST, FOR_UPDATER, FORALL, GE, GHOST, GT, HENCE_BY, HENCE_BY_KEYWORD, HENCE_BY_REDUNDANTLY, HEX_DIGIT, IDENT, IGNORED_AT_IN_COMMENT, IMPLICATION_OP, IMPLIES_THAT, INC, INFORMAL_DESCRIPTION, INIT, INITIALIZER, INITIALLY, INSTANCE, INSTANCE_INIT, INVARIANT, INVARIANT_KEYWORD, INVARIANT_REDUNDANTLY, IS_SUBTYPE_OF, JAVA_BUILTIN_TYPE, JAVA_MODIFIER, JML_BACKSLASH_SEQUENCE, JML_MODIFIER, L_ARROW, LABEL, LABEL_KEYWORD, LAND, LBRACK, LCURLY, LCURLY_VBAR, LE, LET, LETOLD_KEYWORD, LIMPLIES, LITERAL_abstract, LITERAL_assert, LITERAL_boolean, LITERAL_break, LITERAL_byte, LITERAL_case, LITERAL_catch, LITERAL_char, LITERAL_class, LITERAL_const, LITERAL_continue, LITERAL_default, LITERAL_do, LITERAL_double, LITERAL_else, LITERAL_extends, LITERAL_false, LITERAL_final, LITERAL_finally, LITERAL_float, LITERAL_for, LITERAL_if, LITERAL_implements, LITERAL_import, LITERAL_instanceof, LITERAL_int, LITERAL_interface, LITERAL_long, LITERAL_native, LITERAL_new, LITERAL_null, LITERAL_package, LITERAL_private, LITERAL_protected, LITERAL_public, LITERAL_return, LITERAL_short, LITERAL_static, LITERAL_strictfp, LITERAL_super, LITERAL_switch, LITERAL_synchronized, LITERAL_this, LITERAL_throw, LITERAL_throws, LITERAL_transient, LITERAL_true, LITERAL_try, LITERAL_void, LITERAL_volatile, LITERAL_while, LNOT, LOGICAL_OP, LOOP_ASGNABLE_SEQ, LOOP_ASSIGNABLE_KEYWORD, LOOP_EXSURES, LOOP_INV_SEQ, LOOP_INVARIANT, LOOP_INVARIANT_REDUNDANTLY, LOOP_MODIFIES, LOOP_SIG_SEQ, LOR, LPAREN, LT, MAINTAINING, MAINTAINING_KEYWORD, MAINTAINING_REDUNDANTLY, MEASURED_BY, MEASURED_BY_KEYWORD, MEASURED_BY_REDUNDANTLY, METH, MINUS, MINUS_ASSIGN, ML_COMMENT, MOD, MOD_ASSIGN, MODEL, MODEL_PROGRAM, MODIFIABLE, MODIFIABLE_REDUNDANTLY, MODIFIER_SET, MODIFIES, MODIFIES_REDUNDANTLY, MONITORED, MONITORED_BY, MULTIPLICATIVE_ASSIGNMENT_OP, MULTIPLICATIVE_OP, NESTED_CLASS, NL_WS, NON_NL_WS, NON_NULL, NORMAL_BEHAVIOR, NORMAL_EXAMPLE, NOT_EQUAL, NOT_EQUIV, NOWARN_LABEL, NOWARN_LABEL_LIST, NULL_TREE_LOOKAHEAD, NUM_FLOAT, NUM_INT, OLD, OR, PARAM, PLUS, PLUS_ASSIGN, POST, POST_DEC, POST_INC, POST_INCREMENT_OP, POST_REDUNDANTLY, PRE, PRE_INCREMENT_OP, PRE_REDUNDANTLY, PRIVACY_MODIFIER, PURE, QUANT_VARS, QUANTIFIED_EXPR, QUANTIFIER_TOKEN, QUESTION, R_ARROW, RBRACK, RCURLY, READABLE_IF, REFINE, RELATIONAL_OP, REPLACE, REPRESENTS, REPRESENTS_KEYWORD, REPRESENTS_REDUNDANTLY, REQUIRES, REQUIRES_KEYWORD, REQUIRES_REDUNDANTLY, RETURNS, RETURNS_KEYWORD, RETURNS_REDUNDANTLY, RETURNS_SEQ, RPAREN, SEMI, SET, SET_COMPR, SHIFT_ASSIGNMENT_OP, SHIFT_OP, SIG_SEQ, SIGNALS, SIGNALS_KEYWORD, SIGNALS_REDUNDANTLY, SL, SL_ASSIGN, SL_COMMENT, SPEC_CASE, SPEC_PROTECTED, SPEC_PUBLIC, SPEC_SL_COMMENT, SPEC_STATEMENT, SR, SR_ASSIGN, STAR, STAR_ASSIGN, STAR_ELEMS, STATIC_INITIALIZER, STRING_LITERAL, SUBCLASSING_CONTRACT, T_ELEMTYPE, T_EVERYTHING, T_EXISTS, T_FIELDS_OF, T_FORALL, T_FRESH, T_INVARIANT_FOR, T_IS_INITIALIZED, T_LBLNEG, T_LBLPOS, T_LOCKSET, T_MAX, T_MIN, T_NONNULLELEMENTS, T_NOT_MODIFIED, T_NOT_SPECIFIED, T_NOTHING, T_NUM_OF, T_OLD, T_OTHER, T_PRODUCT, T_REACH, T_RESULT, T_SUCH_THAT, T_SUM, T_TYPE, T_TYPEOF, T_TYPEOFALLTYPES, UNARY_NUMERIC_OP, UNINITIALIZED, UNREACHABLE, VAR_DECL, VBAR_RCURLY, VF_SEQ, VOCAB, WEAKLY, WHEN, WHEN_KEYWORD, WHEN_REDUNDANTLY, WS

Constructor Summary

ClassMethod(org.apache.bcel.classfile.Method method, ClassFile cf)

Method Summary

java.lang.String	emit()
boolean	exactMatch(java.util.Vector param_types)
java.util.Vector	getClonedSpecCases(ParsedItem pi)
AClass	getDefiningClass() Returns the class that defines the declaration.
java.lang.String	getInfo()
java.lang.String	getInfo(java.lang.String ret)
IModifiers	getModifiers() Returns the visibility modifiers associated to this declaration.
java.lang.String	getName()
Expression	getNormalizedEnsures(IJml2bConfiguration config)
Expression	getNormalizedRequires(IJml2bConfiguration config)
IAParameters	getParams()
Expression	getRequires()
Type	getReturnType()
java.lang.String	getSignature()
java.util.Enumeration	getSpecCases(IJml2bConfiguration config)
boolean	isConstructor()
boolean	isDefaultConstructor(java.lang.String name)
boolean	isExternalVisible()
boolean	isFinal()
boolean	isPackageVisible()
boolean	isPrivate()
boolean	isProtected()
boolean	isProtectedNotSpecPublic()
boolean	isStatic()
void	link(IJml2bConfiguration config, LinkContext f)
int	linkStatements(IJml2bConfiguration config, LinkContext f)
boolean	matchingSignaturesF(java.util.Vector field_types)
void	parse(IJml2bConfiguration config)
antlr.collections.AST	parse(JmlFile jmlFile, antlr.collections.AST ast) Parses the content of the declaration.

Methods inherited from class jml2b.structure.AMethod

getNameForModifies

Methods inherited from class jml2b.structure.java.Declaration

isVisibleFrom, setDefiningClass

Methods inherited from class jml2b.structure.java.NamedNode

clearName, getBName, hasBName, newName

Methods inherited from class jml2b.structure.java.ParsedItem

change, change, getColumn, getJmlFile, getLine, save, setBox

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ClassMethod

public ClassMethod(org.apache.bcel.classfile.Method method,
                   ClassFile cf)

Method Detail

parse

public void parse(IJml2bConfiguration config)
           throws Jml2bException

Throws:

Jml2bException

emit

public java.lang.String emit()

Specified by:

emit in interface IModifiers

isExternalVisible

public boolean isExternalVisible()

Specified by:

isExternalVisible in interface IModifiers

isFinal

public boolean isFinal()

Specified by:

isFinal in interface IModifiers

isPackageVisible

public boolean isPackageVisible()

Specified by:

isPackageVisible in interface IModifiers

isPrivate

public boolean isPrivate()

Specified by:

isPrivate in interface IModifiers

isProtected

public boolean isProtected()

Specified by:

isProtected in interface IModifiers

isProtectedNotSpecPublic

public boolean isProtectedNotSpecPublic()

Specified by:

isProtectedNotSpecPublic in interface IModifiers

Returns:

isStatic

public boolean isStatic()

Specified by:

isStatic in interface IModifiers

exactMatch

public boolean exactMatch(java.util.Vector param_types)

Specified by:

exactMatch in class AMethod

Parameters:

param_types -

Returns:

matchingSignaturesF

public boolean matchingSignaturesF(java.util.Vector field_types)

getName

public java.lang.String getName()

Specified by:

getName in class AMethod

Returns:

getSignature

public java.lang.String getSignature()

Specified by:

getSignature in class AMethod

getParams

public IAParameters getParams()

Specified by:

getParams in class AMethod

getInfo

public java.lang.String getInfo()

Specified by:

getInfo in class AMethod

getInfo

public java.lang.String getInfo(java.lang.String ret)

Specified by:

getInfo in class AMethod

isConstructor

public boolean isConstructor()

Specified by:

isConstructor in class AMethod

getReturnType

public Type getReturnType()

Specified by:

getReturnType in class AMethod

getSpecCases

public java.util.Enumeration getSpecCases(IJml2bConfiguration config)
                                   throws Jml2bException,
                                          PogException

Specified by:

getSpecCases in class AMethod

Throws:

Jml2bException

PogException

getNormalizedRequires

public Expression getNormalizedRequires(IJml2bConfiguration config)
                                 throws Jml2bException,
                                        PogException

Specified by:

getNormalizedRequires in class AMethod

Throws:

Jml2bException

PogException

getNormalizedEnsures

public Expression getNormalizedEnsures(IJml2bConfiguration config)
                                throws Jml2bException,
                                       PogException

Specified by:

getNormalizedEnsures in class AMethod

Throws:

Jml2bException

PogException

parse

public antlr.collections.AST parse(JmlFile jmlFile,
                                   antlr.collections.AST ast)
                            throws Jml2bException

Description copied from class: Declaration

Parses the content of the declaration.

Specified by:

parse in class Declaration

Parameters:

jmlFile - the file the class that defines the declaration is loaded from.

ast - the AST containing the declaration tree.

Returns:

AST the AST following the declaration.

Throws:

Jml2bException - in case of parse error.

link

public void link(IJml2bConfiguration config,
                 LinkContext f)
          throws Jml2bException

Specified by:

link in interface Linkable

Throws:

Jml2bException

linkStatements

public int linkStatements(IJml2bConfiguration config,
                          LinkContext f)
                   throws Jml2bException

Specified by:

linkStatements in interface Linkable

Throws:

Jml2bException

getClonedSpecCases

public java.util.Vector getClonedSpecCases(ParsedItem pi)

Specified by:

getClonedSpecCases in class AMethod

getRequires

public Expression getRequires()

Specified by:

getRequires in class AMethod

Returns:

isDefaultConstructor

public boolean isDefaultConstructor(java.lang.String name)

Returns:

getDefiningClass

public AClass getDefiningClass()

Description copied from class: Declaration

Returns the class that defines the declaration.

Overrides:

getDefiningClass in class Declaration

Returns:

Class the defining class.

getModifiers

public IModifiers getModifiers()

Description copied from class: Declaration

Returns the visibility modifiers associated to this declaration.

Overrides:

getModifiers in class Declaration

Returns:

Modifiers the modifiers.