org.jmlspecs.checker
Class JmlFieldDeclaration

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Phylum
          org.multijava.mjc.JPhylum
              org.jmlspecs.checker.JmlNode
                  org.jmlspecs.checker.JmlMemberDeclaration
                      org.jmlspecs.checker.JmlFieldDeclaration

All Implemented Interfaces:

Annotatable, Cloneable, Constants, Constants, Constants, JFieldDeclarationType, JMemberDeclarationType, PhylumType

public class JmlFieldDeclaration

extends JmlMemberDeclaration

implements JFieldDeclarationType

JmlFieldDeclaration.java

Version:

$Revision: 1.52 $

Author:

Curtis Clifton

Nested Class Summary
(package private)  class	JmlFieldDeclaration.JmlFieldSpecsContext           A special flow control context class for typechecking JML data group clauses.

 

Nested classes inherited from class org.jmlspecs.checker.JmlNode

JmlNode.DummyInitializerDeclaration

 

Field Summary
private  JStatement	assertionCode           Java source code generated by jmlrac for runtime assertion checking.
private  JmlInGroupClause[]	combinedInGroups
private  JmlMapsIntoClause[]	combinedMapsIntoGroups
private  JmlVarAssertion[]	combinedVarAssertions
ArrayList	datagroupContents
private  JFieldDeclaration	delegee
private  JmlInGroupClause[]	inGroups
private  JmlMapsIntoClause[]	mapsIntoGroups
private  JmlVarAssertion[]	varAssertions

 

Fields inherited from class org.jmlspecs.checker.JmlMemberDeclaration

refinedDecl, refiningDecl

 

Fields inherited from class org.jmlspecs.checker.JmlNode

MJCVISIT_MESSAGE

 

Fields inherited from class org.multijava.util.compiler.Phylum

 

Fields inherited from class org.multijava.util.Utils

DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO

 

Fields inherited from interface org.jmlspecs.checker.Constants

ACC2_RAC_METHOD, ACC_CODE, ACC_CODE_BIGINT_MATH, ACC_CODE_JAVA_MATH, ACC_CODE_SAFE_MATH, ACC_GHOST, ACC_HELPER, ACC_INSTANCE, ACC_MODEL, ACC_MONITORED, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_QUERY, ACC_SECRET, ACC_SPEC_BIGINT_MATH, ACC_SPEC_JAVA_MATH, ACC_SPEC_PROTECTED, ACC_SPEC_PUBLIC, ACC_SPEC_SAFE_MATH, ACC_UNINITIALIZED, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_BIGINT_MATH, EVERYTHING, JML_JMLObjectSet, NOT_SPECIFIED, NOTHING, OPE_BACKWARD_IMPLIES, OPE_EQUIV, OPE_EXISTS, OPE_FORALL, OPE_IMPLIES, OPE_L_ARROW, OPE_MAX, OPE_MIN, OPE_NOT_EQUIV, OPE_NUM_OF, OPE_PRODUCT, OPE_R_ARROW, OPE_SUBTYPE, OPE_SUM, SAME, TID_BIGINT, TID_REAL, TID_TYPE, TN_JMLOBJECTSET, TN_JMLTYPE, TN_JMLVALUESET

 

Fields inherited from interface org.multijava.mjc.Constants

ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP

 

Fields inherited from interface org.multijava.util.classfile.Constants

ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID

 

Constructor Summary
protected	JmlFieldDeclaration(TokenReference where, JmlVarAssertion[] varAssertions, JmlDataGroupAccumulator dataGroups, JFieldDeclaration delegee)

 

Method Summary
void	accept(MjcVisitor p)           Accepts the specified visitor.
void	addSelfToInDataGroups(JmlSourceField self, JmlInGroupClause inGroupClause, JmlDataGroupMemberMap dataGroupMap)
void	addToDataGroups(JmlDataGroupMemberMap dataGroupMap)
JStatement	assertionCode()           Returns the Java source code generated by jmlrac for runtime assertion checking.
void	checkFieldSpecs(CFlowControlContextType context, JmlSourceField self)           Typechecks the specifications associated with this field, i.e., data group specifications.
CSourceField	checkInterface(CClassContextType context)           Checks the basic interfaces to make sure things generally look OK.
void	checkRefinementConsistency(CContextType context)
void	combineDataGroups(JmlFieldDeclaration refField)
void	combineSpecifications()
JmlFieldDeclaration	findDeclWithInitializer()           Returns the field declaration in the refinement chain that has an initializer.
void	genCode(CodeSequence code)           Generates a sequence of bytecodes
JmlInGroupClause[]	getCombinedInGroupClauses()
JmlMapsIntoClause[]	getCombinedMapsIntoClauses()
JmlVarAssertion[]	getCombinedVarAssertions()           Returns the variable assertions of this member declaration combined with the assertions of those it refines.
JExpression	getInitializer()
CType	getType()           Returns the type of this field
boolean	hasAssertionCode()           Returns true if this field declaration has the Java source code generated by jmlrac.
boolean	hasAssertions()           Indicates whether this field declaration has an accompanying jml-var-assertion.
boolean	hasInitializer()           Returns true if this field declarator has an initializer (should be initialized)
String	ident()           Returns the identifier of this field declaration
JmlInGroupClause[]	inGroupClauses()
boolean	isModel()           Returns true if this member is declared with a 'model' modifier.
JmlMemberAccess	jmlAccess()
static JmlFieldDeclaration	makeInstance(TokenReference where, JVariableDefinition var, JavadocComment javadoc, JavaStyleComment[] comment, JmlVarAssertion[] varAssertions, JmlDataGroupAccumulator dataGroups)
JmlMapsIntoClause[]	mapsIntoClauses()
long	modifiers()           Returns the modifiers of this field declaration
boolean	needInitialization()           Returns true if this field need to be initialized WARNING: this method returns true when initial value corresponds to a default value ====> a second check should be made after typecheck to ensure that an initialization is really needed
void	setAssertionCode(JStatement code)           Sets the Java source code generated by jmlrac for runtime assertion checking.
void	setInitializer(JExpression expr)           Sets the initialization expression for this field.
void	setModifiers(long mod)           Set the modifiers of this field declaration.
protected  void	setRefinementLinks()           Determines the field refined by this field (if there is one).
protected  void	setRefiningField(JmlFieldDeclaration refiningField)
void	setSpecstoCombinedSpecs()
void	typecheck(CFlowControlContextType context)           Checks whether this field declaration includes a field initializer and mutates the context to store this information about the field.
JmlVarAssertion[]	varAssertions()           Returns the jml-var-assertion associated with this.
JVariableDefinition	variable()

 

Methods inherited from class org.jmlspecs.checker.JmlMemberDeclaration

checkRefinedModifiers, findJavaFileInRefinement, genComments, getCClass, getCombinedSpecification, getField, getMethod, getMostRefined, getRefinedMember, getRefiningMember, inBinaryClassFile, inJavaFile, inners, isDeprecated, isRefined, isRefiningMember, javadocComment, setRefinedMember, setRefiningMember, stringRepresentation

 

Methods inherited from class org.jmlspecs.checker.JmlNode

enterSpecScope, enterSpecScope, exitSpecScope, exitSpecScope, privacy, privacyString

 

Methods inherited from class org.multijava.mjc.JPhylum

check, check, check, check, fail, fail, fail, warn, warn, warn, warn

 

Methods inherited from class org.multijava.util.compiler.Phylum

getTokenReference, setTokenReference

 

Methods inherited from class org.multijava.util.Utils

assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray

 

Methods inherited from class java.lang.Object

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

 

Methods inherited from interface org.multijava.mjc.JMemberDeclarationType

genComments, getCClass, getField, getMethod, isDeprecated

 

Methods inherited from interface org.multijava.util.compiler.PhylumType

getTokenReference, setTokenReference

 

Methods inherited from interface org.multijava.javadoc.Annotatable

javadocComment

 

Field Detail

varAssertions

private JmlVarAssertion[] varAssertions

combinedVarAssertions

private JmlVarAssertion[] combinedVarAssertions

inGroups

private JmlInGroupClause[] inGroups

combinedInGroups

private JmlInGroupClause[] combinedInGroups

mapsIntoGroups

private JmlMapsIntoClause[] mapsIntoGroups

combinedMapsIntoGroups

private JmlMapsIntoClause[] combinedMapsIntoGroups

datagroupContents

public ArrayList datagroupContents

delegee

private JFieldDeclaration delegee

assertionCode

private JStatement assertionCode

Java source code generated by jmlrac for runtime assertion checking. E.g., initialzer for ghost variables.

JmlFieldDeclaration

protected JmlFieldDeclaration(TokenReference where,
                              JmlVarAssertion[] varAssertions,
                              JmlDataGroupAccumulator dataGroups,
                              JFieldDeclaration delegee)

makeInstance

public static JmlFieldDeclaration makeInstance(TokenReference where,
                                               JVariableDefinition var,
                                               JavadocComment javadoc,
                                               JavaStyleComment[] comment,
                                               JmlVarAssertion[] varAssertions,
                                               JmlDataGroupAccumulator dataGroups)

hasAssertions

public boolean hasAssertions()

Indicates whether this field declaration has an accompanying jml-var-assertion.

 ensures \result <==> varAssertions != null && varAssertions.length > 0;
 

varAssertions

public JmlVarAssertion[] varAssertions()

Returns the jml-var-assertion associated with this.

 requires hasAssertions();
 

hasInitializer

public boolean hasInitializer()

Returns true if this field declarator has an initializer (should be initialized)

Specified by:

hasInitializer in interface JFieldDeclarationType

getInitializer

public JExpression getInitializer()

Returns:

the value of this field at initialization

setInitializer

public void setInitializer(JExpression expr)

Sets the initialization expression for this field.

findDeclWithInitializer

public JmlFieldDeclaration findDeclWithInitializer()

Returns the field declaration in the refinement chain that has an initializer.

getType

public CType getType()

Returns the type of this field

Specified by:

getType in interface JFieldDeclarationType

needInitialization

public boolean needInitialization()

Returns true if this field need to be initialized WARNING: this method returns true when initial value corresponds to a default value ====> a second check should be made after typecheck to ensure that an initialization is really needed

Specified by:

needInitialization in interface JFieldDeclarationType

variable

public JVariableDefinition variable()

Specified by:

variable in interface JFieldDeclarationType

modifiers

public long modifiers()

Returns the modifiers of this field declaration

Specified by:

modifiers in interface JFieldDeclarationType

setModifiers

public void setModifiers(long mod)

Set the modifiers of this field declaration.

ident

public String ident()

Returns the identifier of this field declaration

Specified by:

ident in interface JFieldDeclarationType

assertionCode

public JStatement assertionCode()

Returns the Java source code generated by jmlrac for runtime assertion checking. E.g., initialzer for ghost variables.

hasAssertionCode

public boolean hasAssertionCode()

Returns true if this field declaration has the Java source code generated by jmlrac. E.g., initialzer for ghost variables.

setAssertionCode

public void setAssertionCode(JStatement code)

Sets the Java source code generated by jmlrac for runtime assertion checking. E.g., initialzer for ghost variables.

jmlAccess

public JmlMemberAccess jmlAccess()

Returns:

the member access information object for this member.

isModel

public boolean isModel()

Returns true if this member is declared with a 'model' modifier.

checkInterface

public CSourceField checkInterface(CClassContextType context)
                            throws PositionedError

Checks the basic interfaces to make sure things generally look OK. This pass gathers information about the type signatures of everything (imported class files, classes being compiled, methods, fields, etc...) needed for the later passes. This information is stored in a context hierarchy that is bound to the AST.

Specified by:

checkInterface in interface JFieldDeclarationType

Parameters:

context - the context in which this field appears

Returns:

the signature of this field

Throws:

PositionedError - an error with reference to the source file

typecheck

public void typecheck(CFlowControlContextType context)
               throws PositionedError

Checks whether this field declaration includes a field initializer and mutates the context to store this information about the field. Records the value of a compile-time constant initializer.

Specified by:

typecheck in interface JFieldDeclarationType

Parameters:

context - the context in which this field is declared

Throws:

PositionedError - if any checks fail

checkFieldSpecs

public void checkFieldSpecs(CFlowControlContextType context,
                            JmlSourceField self)
                     throws PositionedError

Typechecks the specifications associated with this field, i.e., data group specifications.

Parameters:

context - the context in which this field is declared

Throws:

PositionedError - if any checks fail

genCode

public void genCode(CodeSequence code)

Generates a sequence of bytecodes

Specified by:

genCode in interface JFieldDeclarationType

Parameters:

code - the code list

accept

public void accept(MjcVisitor p)

Accepts the specified visitor.

Specified by:

accept in interface JMemberDeclarationType

Overrides:

accept in class JmlMemberDeclaration

Parameters:

p - the visitor

checkRefinementConsistency

public void checkRefinementConsistency(CContextType context)
                                throws PositionedError

Throws:

PositionedError

setRefinementLinks

protected void setRefinementLinks()

Determines the field refined by this field (if there is one). Caches the result for later calls to #getRefinedMember(). Also links the refined field back to this, so they are linked to each other.

setRefiningField

protected void setRefiningField(JmlFieldDeclaration refiningField)

setSpecstoCombinedSpecs

public void setSpecstoCombinedSpecs()

getCombinedVarAssertions

public JmlVarAssertion[] getCombinedVarAssertions()

Returns the variable assertions of this member declaration combined with the assertions of those it refines. Returns null if it does not have any combined variable assertions.

Overrides:

getCombinedVarAssertions in class JmlMemberDeclaration

combineSpecifications

public void combineSpecifications()

Description copied from class: JmlMemberDeclaration

Combine the specifications of this declaration with the specifications of the declarations it refines.

combineDataGroups

public void combineDataGroups(JmlFieldDeclaration refField)

inGroupClauses

public JmlInGroupClause[] inGroupClauses()

getCombinedInGroupClauses

public JmlInGroupClause[] getCombinedInGroupClauses()

mapsIntoClauses

public JmlMapsIntoClause[] mapsIntoClauses()

getCombinedMapsIntoClauses

public JmlMapsIntoClause[] getCombinedMapsIntoClauses()

addToDataGroups

public void addToDataGroups(JmlDataGroupMemberMap dataGroupMap)

addSelfToInDataGroups

public void addSelfToInDataGroups(JmlSourceField self,
                                  JmlInGroupClause inGroupClause,
                                  JmlDataGroupMemberMap dataGroupMap)