jml2b.structure.java
Class Constructor

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.java.Method
                          extended byjml2b.structure.java.Constructor
All Implemented Interfaces:
IModifiesField, jml.JmlDeclParserTokenTypes, Linkable, java.io.Serializable, TypeCheckable

public class Constructor
extends Method

Specialisation of the Method class suitable for representing constructors. Constructors are handled the same as methods, excepted that they are parsed a bit differently, due to the fact that they do not declare a return type.

Author:
A. Requet
See Also:
Serialized Form

Field Summary
 
Fields inherited from class jml2b.structure.java.Method
lemmas, wellDefinednessLemmas
 
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
 
Method Summary
 void completeModifiesWithOwnFields(IJml2bConfiguration config)
           
 boolean isConstructor()
           
 antlr.collections.AST parse(JmlFile jmlFile, antlr.collections.AST ast)
          Parses the content of the declaration.
 void restore()
           
 
Methods inherited from class jml2b.structure.java.Method
addAnnotation, addAnnotation, addComputedModifies, addComputedRequires, annotate, emitSpecCase, exactMatch, getAnnotatedModifies, getAnnotatedPostcondition, getAnnotatedPrecondition, getBody, getCalledMethods, getClonedSpecCases, getDefaultLoopModifies, getEnsuresAsExpression, getExsuresAsExpression, getFirstLine, getInfo, getInfo, getLemmas, getLoopAtLine, getName, getNormalizedEnsures, getNormalizedRequires, getParams, getParamsString, getPmiName, getRequires, getReturnType, getSignature, getSpecCases, getSpecCasesV, getSpecType, getSuperMethod, getWellDefinednessLemmas, hasNoCode, isAnnotated, isStatic, link, linkStatements, matchWith, nbPo, nbPoChecked, nbPoProved, nbPoProved, save, setPmiName, setRequires, setReturnType, setSpecCases, toString, typeCheck
 
Methods inherited from class jml2b.structure.AMethod
getNameForModifies
 
Methods inherited from class jml2b.structure.java.Declaration
getDefiningClass, getModifiers, 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, wait, wait, wait
 
Methods inherited from interface jml2b.formula.IModifiesField
getNameForModifies
 

Method Detail

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.

Overrides:
parse in class Method
Throws:
Jml2bException

isConstructor

public boolean isConstructor()
Overrides:
isConstructor in class Method

completeModifiesWithOwnFields

public void completeModifiesWithOwnFields(IJml2bConfiguration config)
                                   throws PogException,
                                          Jml2bException
Throws:
PogException
Jml2bException

restore

public void restore()