jml2b.structure.bytecode
Class ClassFile

java.lang.Object
  extended byjml2b.util.Profiler
      extended byjml2b.structure.java.ParsedItem
          extended byjml2b.structure.java.NamedNode
              extended byjml2b.structure.java.AClass
                  extended byjml2b.structure.bytecode.ClassFile
All Implemented Interfaces:
IModifiers, jml.JmlDeclParserTokenTypes, Linkable, java.io.Serializable

public class ClassFile
extends AClass
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
ClassFile(org.apache.bcel.classfile.JavaClass class1)
           
 
Method Summary
 java.lang.String emit()
           
 AMethod getConstructor(IJml2bConfiguration config, java.util.Vector param_types)
           
 AMethod getDefaultConstructor()
           
 java.util.Enumeration getDepends()
           
 AField getField(java.lang.String name, AClass from)
           
 java.util.Enumeration getFields()
           
 java.lang.String getFullyQualifiedName()
           
 java.util.Enumeration getImplements()
           
 java.util.Enumeration getMemberInvariants()
           
 AMethod getMethod(java.lang.String name, Parameters p)
           
 IModifiers getModifiers()
           
 java.lang.String getName()
           
 java.util.Vector getOwnFields()
           
 Package getPackage()
           
 java.util.Enumeration getRepresents()
           
 java.util.Enumeration getStaticFinalFieldsInvariant()
           
 Expression getStaticFinalFieldsInvariants()
           
 java.util.Enumeration getStaticInvariants()
           
 boolean isExternalVisible()
           
 boolean isFinal()
           
 boolean isInterface()
           
 boolean isPackageVisible()
           
 boolean isPrivate()
           
 boolean isProtected()
           
 boolean isProtectedNotSpecPublic()
           
 boolean isStatic()
           
 void link(IJml2bConfiguration config)
           
 void link(IJml2bConfiguration config, LinkContext f)
           
 int linkStatements(IJml2bConfiguration config, LinkContext f)
           
 AMethod lookupMethodCurrentClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate)
           
 void parse(IJml2bConfiguration config)
           
 
Methods inherited from class jml2b.structure.java.AClass
addSuperFields, getField, getSuper, getSuperClass, getSuperDefaultConstructor, implementsInterface, isObject, isSubclassOf, lookupMethod, lookupMethodClass, lookupMethodInterface
 
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

ClassFile

public ClassFile(org.apache.bcel.classfile.JavaClass class1)
Method Detail

parse

public void parse(IJml2bConfiguration config)
           throws Jml2bException
Parameters:
config -
Throws:
Jml2bException

link

public void link(IJml2bConfiguration config)

emit

public java.lang.String emit()
Specified by:
emit 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

isStatic

public boolean isStatic()
Specified by:
isStatic in interface IModifiers

getOwnFields

public java.util.Vector getOwnFields()
Specified by:
getOwnFields in class AClass
Returns:

getConstructor

public AMethod getConstructor(IJml2bConfiguration config,
                              java.util.Vector param_types)
                       throws Jml2bException
Specified by:
getConstructor in class AClass
Throws:
Jml2bException

getDefaultConstructor

public AMethod getDefaultConstructor()
Specified by:
getDefaultConstructor in class AClass

getMethod

public AMethod getMethod(java.lang.String name,
                         Parameters p)
Specified by:
getMethod in class AClass

getModifiers

public IModifiers getModifiers()
Specified by:
getModifiers in class AClass

getField

public AField getField(java.lang.String name,
                       AClass from)
Specified by:
getField in class AClass

getFields

public java.util.Enumeration getFields()
Specified by:
getFields in class AClass

getFullyQualifiedName

public java.lang.String getFullyQualifiedName()
Specified by:
getFullyQualifiedName in class AClass

getDepends

public java.util.Enumeration getDepends()
Specified by:
getDepends in class AClass

getImplements

public java.util.Enumeration getImplements()
Specified by:
getImplements in class AClass

getMemberInvariants

public java.util.Enumeration getMemberInvariants()
Specified by:
getMemberInvariants in class AClass

getName

public java.lang.String getName()
Specified by:
getName in class AClass

getPackage

public Package getPackage()
Specified by:
getPackage in class AClass

getRepresents

public java.util.Enumeration getRepresents()
Specified by:
getRepresents in class AClass

getStaticFinalFieldsInvariant

public java.util.Enumeration getStaticFinalFieldsInvariant()
Specified by:
getStaticFinalFieldsInvariant in class AClass

getStaticFinalFieldsInvariants

public Expression getStaticFinalFieldsInvariants()
Specified by:
getStaticFinalFieldsInvariants in class AClass

getStaticInvariants

public java.util.Enumeration getStaticInvariants()
Specified by:
getStaticInvariants in class AClass

isInterface

public boolean isInterface()
Specified by:
isInterface in class AClass

lookupMethodCurrentClass

public AMethod lookupMethodCurrentClass(IJml2bConfiguration config,
                                        java.lang.String mth_name,
                                        java.util.Vector param_types,
                                        AMethod candidate)
                                 throws Jml2bException
Specified by:
lookupMethodCurrentClass in class AClass
Throws:
Jml2bException

isExternalVisible

public boolean isExternalVisible()
Specified by:
isExternalVisible in interface IModifiers

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

isProtectedNotSpecPublic

public boolean isProtectedNotSpecPublic()
Specified by:
isProtectedNotSpecPublic in interface IModifiers
Returns: