jml2b.structure.java
Class Field

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.java.ParsedItem
          jml2b.structure.java.NamedNode
              jml2b.structure.java.Declaration
                  jml2b.structure.AField
                      jml2b.structure.java.Field

All Implemented Interfaces:

jml.JmlDeclParserTokenTypes, Linkable, java.io.Serializable

Direct Known Subclasses:

TemporaryField

public class Field

extends AField

implements java.io.Serializable

Class representing fields. It stores the name and the type of a field or variable. This class is also used to represent local variables. In that case, the modifiers can be null.

Author:

A. Requet

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

Field()

Field(ParsedItem pi, Modifiers m, Type t, java.lang.String n, Expression a)

Field(ParsedItem pi, Type t, java.lang.String n)

Method Summary

java.lang.String	emit()
Expression	getAssign() Returns the Expression object corresponding to the assign clause of this field The assign clause of a field corresponds to its initialisation, when an initialisation is given during the declaration of the field.
java.lang.String	getBName() Returns the B name of the field.
Expression	getDefaultInitialiser()
java.lang.String	getName() Returns the name of the field.
Type	getType() Retursn the type of the field.
boolean	isExpanded()
boolean	isLocal() Indicates wether the field correspond to a local variable or to a parameter.
void	link(IJml2bConfiguration config, LinkContext f)
int	linkStatements(IJml2bConfiguration config, LinkContext f)
antlr.collections.AST	parse(JmlFile jmlFile, antlr.collections.AST a) Deprecated. The VarDeclParser class should be used instead of this method.
static Field[]	parseVarDecl(JmlFile jmlFile, antlr.collections.AST vardecl, Modifiers mods)
void	setAssign(Expression a) Sets the Expression object corresponding to the assign clause of the field.
void	setParsedItem(ParsedItem pi)

Methods inherited from class jml2b.structure.java.Declaration

getDefiningClass, getModifiers, isVisibleFrom, setDefiningClass

Methods inherited from class jml2b.structure.java.NamedNode

clearName, 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

Field

public Field()

Field

public Field(ParsedItem pi,
             Modifiers m,
             Type t,
             java.lang.String n,
             Expression a)

Field

public Field(ParsedItem pi,
             Type t,
             java.lang.String n)

Method Detail

parse

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

Deprecated. The VarDeclParser class should be used instead of this method.

Parses the AST. This method has been removed since fields are parsed using the VarDeclParser class.

Specified by:

parse in class Declaration

Parameters:

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

a - 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

getAssign

public Expression getAssign()

Returns the Expression object corresponding to the assign clause of this field The assign clause of a field corresponds to its initialisation, when an initialisation is given during the declaration of the field.

Specified by:

getAssign in class AField

Returns:

Expression the expression object corresponding to the assign clause of the field.

setAssign

public void setAssign(Expression a)

Sets the Expression object corresponding to the assign clause of the field. The assign clause of a field corresponds to its initialisation, when an initialisation is given during the declaration of the field.

Parameters:

a - the expression corresponding to the assign clause.

isLocal

public boolean isLocal()

Indicates wether the field correspond to a local variable or to a parameter.

Specified by:

isLocal in class AField

Returns:

boolean

getDefaultInitialiser

public Expression getDefaultInitialiser()

getName

public java.lang.String getName()

Returns the name of the field.

Specified by:

getName in class NamedNode

Returns:

String the name of the field.

getBName

public java.lang.String getBName()

Returns the B name of the field.

Overrides:

getBName in class NamedNode

Returns:

String a B identifier corresponding to the name fo the field.

getType

public Type getType()

Retursn the type of the field.

Specified by:

getType in class AField

Returns:

Type the type of the field.

parseVarDecl

public static Field[] parseVarDecl(JmlFile jmlFile,
                                   antlr.collections.AST vardecl,
                                   Modifiers mods)
                            throws Jml2bException

Throws:

Jml2bException

isExpanded

public boolean isExpanded()

Specified by:

isExpanded in class AField

emit

public java.lang.String emit()

setParsedItem

public void setParsedItem(ParsedItem pi)