jml2b.structure.bytecode
Class ClassDefaultConstructor

java.lang.Object
  extended byjml2b.util.Profiler
      extended byjml2b.structure.java.ParsedItem
          extended byjml2b.structure.java.NamedNode
              extended byjml2b.structure.java.Declaration
                  extended byjml2b.structure.AMethod
                      extended byjml2b.structure.bytecode.ClassMethod
                          extended byjml2b.structure.bytecode.ClassDefaultConstructor
All Implemented Interfaces:
IModifiers, IModifiesField, jml.JmlDeclParserTokenTypes, Linkable, java.io.Serializable

public class ClassDefaultConstructor
extends ClassMethod

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
ClassDefaultConstructor(ClassFile cf)
           
 
Method Summary
 boolean exactMatch(java.util.Vector param_types)
           
 java.lang.String getName()
           
 IAParameters getParams()
           
 Type getReturnType()
           
 java.lang.String getSignature()
           
 boolean isCompatible(java.util.Vector param_types)
           
 boolean isConstructor()
           
 boolean isDefaultConstructor(java.lang.String name)
           
 boolean isExternalVisible()
           
 boolean isFinal()
           
 boolean isPackageVisible()
           
 boolean isPrivate()
           
 boolean isProtected()
           
 boolean isProtectedNotSpecPublic()
           
 boolean isStatic()
           
 boolean matchingSignaturesF(java.util.Vector field_types)
           
 void parse(IJml2bConfiguration config)
           
 
Methods inherited from class jml2b.structure.bytecode.ClassMethod
emit, getClonedSpecCases, getDefiningClass, getInfo, getInfo, getModifiers, getNormalizedEnsures, getNormalizedRequires, getRequires, getSpecCases, link, linkStatements, parse
 
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

ClassDefaultConstructor

public ClassDefaultConstructor(ClassFile cf)
Method Detail

isExternalVisible

public boolean isExternalVisible()
Specified by:
isExternalVisible in interface IModifiers
Overrides:
isExternalVisible in class ClassMethod

isFinal

public boolean isFinal()
Specified by:
isFinal in interface IModifiers
Overrides:
isFinal in class ClassMethod

isPackageVisible

public boolean isPackageVisible()
Specified by:
isPackageVisible in interface IModifiers
Overrides:
isPackageVisible in class ClassMethod

isPrivate

public boolean isPrivate()
Specified by:
isPrivate in interface IModifiers
Overrides:
isPrivate in class ClassMethod

isProtected

public boolean isProtected()
Specified by:
isProtected in interface IModifiers
Overrides:
isProtected in class ClassMethod

isProtectedNotSpecPublic

public boolean isProtectedNotSpecPublic()
Specified by:
isProtectedNotSpecPublic in interface IModifiers
Overrides:
isProtectedNotSpecPublic in class ClassMethod

isStatic

public boolean isStatic()
Specified by:
isStatic in interface IModifiers
Overrides:
isStatic in class ClassMethod

parse

public void parse(IJml2bConfiguration config)
           throws Jml2bException
Overrides:
parse in class ClassMethod
Throws:
Jml2bException

exactMatch

public boolean exactMatch(java.util.Vector param_types)
Overrides:
exactMatch in class ClassMethod
Parameters:
param_types -
Returns:

matchingSignaturesF

public boolean matchingSignaturesF(java.util.Vector field_types)
Overrides:
matchingSignaturesF in class ClassMethod

isCompatible

public boolean isCompatible(java.util.Vector param_types)

getName

public java.lang.String getName()
Overrides:
getName in class ClassMethod

getSignature

public java.lang.String getSignature()
Overrides:
getSignature in class ClassMethod

getParams

public IAParameters getParams()
Overrides:
getParams in class ClassMethod

isConstructor

public boolean isConstructor()
Overrides:
isConstructor in class ClassMethod

getReturnType

public Type getReturnType()
Overrides:
getReturnType in class ClassMethod

isDefaultConstructor

public boolean isDefaultConstructor(java.lang.String name)
Overrides:
isDefaultConstructor in class ClassMethod
Returns: