JML

org.jmlspecs.checker
Class JmlOwnershipAdmissibilityVisitor

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.checker.JmlAbstractVisitor
          extended byorg.jmlspecs.jmlrac.RacAbstractVisitor
              extended byorg.jmlspecs.jmlrac.qexpr.AbstractExpressionVisitor
                  extended byorg.jmlspecs.checker.JmlAdmissibilityVisitor
                      extended byorg.jmlspecs.checker.JmlOwnershipAdmissibilityVisitor
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor, RacConstants, RacVisitor

class JmlOwnershipAdmissibilityVisitor
extends JmlAdmissibilityVisitor


Nested Class Summary
private static class JmlOwnershipAdmissibilityVisitor.State
          A data structure to store the current state of this visitor.
 
Nested classes inherited from class org.jmlspecs.checker.JmlAdmissibilityVisitor
JmlAdmissibilityVisitor.NotAdmissibleException
 
Field Summary
private  boolean isCastedToRep
          Was something casted to rep ?
private  boolean needsArrayBaseNotReadOnly
          Indicates whether the declared array base-type universe modifier must be checked when accessing the array.
private  boolean needsRep
          Indicates whether the pivot field g0 must be a rep field, i.e. whether rule 3 must be applied.
private  JExpression potentiallyNotAdmissible
          In order to get meaningful error messages, the JExpression where needsRep was set is stored.
private  Stack stateStack
          The state of this JmlOwnershipAdmissibilityVisitor is often saved at the beginning of a visit-method, and restored at its end.
 
Fields inherited from class org.jmlspecs.checker.JmlAdmissibilityVisitor
ADMISSIBILITY_CLASSICAL, ADMISSIBILITY_NONE, ADMISSIBILITY_OWNERSHIP, ectx, hasErrorsOrWarnings, modelField
 
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_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_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, 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, NULLITY_MODS, 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_SYNTHETIC, 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
 
Fields inherited from interface org.jmlspecs.jmlrac.RacConstants
MN_CHECK_HC, MN_CHECK_INV, MN_CHECK_POST, MN_CHECK_PRE, MN_CHECK_XPOST, MN_EVAL_OLD, MN_GHOST, MN_INIT, MN_INTERNAL, MN_MODEL, MN_MODEL_PUBLIC, MN_RESTORE_FROM, MN_SAVE_TO, MN_SPEC, MN_SPEC_PUBLIC, TN_JMLCHECKABLE, TN_JMLSURROGATE, TN_JMLUNIT_TEST_POSTFIX, TN_JMLUNIT_TESTDATA_POSTFIX, TN_JMLVALUE, TN_SURROGATE, VN_ASSERTION, VN_CATCH_VAR, VN_CLASS_INIT, VN_CONSTRUCTED, VN_DELEGEE, VN_ERROR_SET, VN_EXCEPTION, VN_FREE_VAR, VN_INIT, VN_OLD_VAR, VN_POST_VAR, VN_PRE_VAR, VN_PRECOND, VN_RAC_COMPILED, VN_RAC_LEVEL, VN_RESULT, VN_STACK_VAR, VN_XRESULT
 
Constructor Summary
(package private) JmlOwnershipAdmissibilityVisitor()
           
 
Method Summary
private  void clearCurrentState()
          Clears the current state of this visitor, i.e. sets all fields to their initial value.
private  void popState()
          Restores the last pushed state.
private  void pushState()
          Stores a copy of the current state and pushes this copy onto the top if stateStack.
protected  void visit(JExpression expr)
          This method calls the JExpression.accept(MjcVisitor) method of expr.
 void visitArrayAccessExpression(JArrayAccessExpression self)
          Visits the given array access expression, self.
 void visitArrayDimsAndInit(JArrayDimsAndInits self)
          Visits the given array dimension and initializer, self.
 void visitCastExpression(JCastExpression self)
          Visits the given cast expression, self.
 void visitConditionalExpression(JConditionalExpression self)
          Visits the given conditional expression, self.
 void visitFieldExpression(JClassFieldExpression self)
          Visits the given class field expression, self.
 void visitMethodCallExpression(JMethodCallExpression self)
          Visits the given method expression, self.
 void visitNewObjectExpression(JNewObjectExpression self)
          Visits the given new object expression, self.
 void visitThisExpression(JThisExpression self)
          Visits the given this expression, self.
 
Methods inherited from class org.jmlspecs.checker.JmlAdmissibilityVisitor
checkAdmissibility, checkInvariant, checkRepresentsClause, isAdmissibilityCheckEnabled, isAdmissibilityOwnershipEnabled, isThisAfterCasts, removeParentheses, warn
 
Methods inherited from class org.jmlspecs.jmlrac.qexpr.AbstractExpressionVisitor
visitAddExpression, visitArrayInitializer, visitArrayLengthExpression, visitAssignmentExpression, visitBinaryExpression, visitBitwiseExpression, visitClassExpression, visitCompoundAssignmentExpression, visitConditionalAndExpression, visitConditionalOrExpression, visitDivideExpression, visitEqualityExpression, visitExplicitConstructorInvocation, visitExpressions, visitInstanceofExpression, visitJmlDurationExpression, visitJmlElemTypeExpression, visitJmlFreshExpression, visitJmlInformalExpression, visitJmlInvariantForExpression, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLockSetExpression, visitJmlMaxExpression, visitJmlNonNullElementsExpression, visitJmlOldExpression, visitJmlPredicate, visitJmlPreExpression, visitJmlReachExpression, visitJmlRelationalExpression, visitJmlResultExpression, visitJmlSetComprehension, visitJmlSpaceExpression, visitJmlSpecExpression, visitJmlSpecQuantifiedExpression, visitJmlTypeExpression, visitJmlTypeOfExpression, visitJmlWorkingSpaceExpression, visitLocalVariableExpression, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitParenthesedExpression, visitPostfixExpression, visitPrefixExpression, visitRelationalExpression, visitShiftExpression, visitSuperExpression, visitTypeNameExpression, visitUnaryExpression, visitUnaryPromoteExpression
 
Methods inherited from class org.jmlspecs.jmlrac.RacAbstractVisitor
visitRacNode, visitRacPredicate
 
Methods inherited from class org.jmlspecs.checker.JmlAbstractVisitor
visitAssertStatement, visitBinaryExpression, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitByteLiteral, visitCatchClause, visitCharLiteral, visitClassBlock, visitClassDeclaration, visitClassOrGFImport, visitCompilationUnit, visitCompoundStatement, visitCompoundStatement, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDoStatement, visitDoubleLiteral, visitEmptyStatement, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFloatLiteral, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInterfaceDeclaration, visitIntLiteral, visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBehaviorSpec, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalBehaviorSpec, visitJmlExceptionalExample, visitJmlExceptionalSpecBody, visitJmlExceptionalSpecCase, visitJmlExpression, visitJmlExtendingSpecification, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlGeneralSpecCase, visitJmlGenericSpecBody, visitJmlGenericSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantStatement, visitJmlLetVarDecl, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNormalBehaviorSpec, visitJmlNormalExample, visitJmlNormalSpecBody, visitJmlNormalSpecCase, visitJmlNotAssignedExpression, visitJmlNotModifiedExpression, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicateKeyword, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlReturnsClause, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpecBody, visitJmlSpecification, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWritableIfVarAssertion, visitLabeledStatement, visitLongLiteral, visitMathModeExpression, visitMethodDeclaration, visitNullLiteral, visitOrdinalLiteral, visitPackageImport, visitPackageName, visitRealLiteral, visitReturnStatement, visitShortLiteral, visitStringLiteral, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement
 
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.jmlspecs.checker.JmlVisitor
visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBehaviorSpec, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalBehaviorSpec, visitJmlExceptionalExample, visitJmlExceptionalSpecBody, visitJmlExceptionalSpecCase, visitJmlExpression, visitJmlExtendingSpecification, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlGeneralSpecCase, visitJmlGenericSpecBody, visitJmlGenericSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantStatement, visitJmlLetVarDecl, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNormalBehaviorSpec, visitJmlNormalExample, visitJmlNormalSpecBody, visitJmlNormalSpecCase, visitJmlNotAssignedExpression, visitJmlNotModifiedExpression, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicateKeyword, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlReturnsClause, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpecBody, visitJmlSpecification, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWritableIfVarAssertion
 
Methods inherited from interface org.multijava.mjc.MjcVisitor
visitAssertStatement, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitCatchClause, visitCharLiteral, visitClassBlock, visitClassDeclaration, visitClassOrGFImport, visitCompilationUnit, visitCompoundStatement, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDoStatement, visitEmptyStatement, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInterfaceDeclaration, visitLabeledStatement, visitMathModeExpression, visitMethodDeclaration, visitNullLiteral, visitOrdinalLiteral, visitPackageImport, visitPackageName, visitRealLiteral, visitReturnStatement, visitStringLiteral, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement
 

Field Detail

needsRep

private boolean needsRep
Indicates whether the pivot field g0 must be a rep field, i.e. whether rule 3 must be applied.


needsArrayBaseNotReadOnly

private boolean needsArrayBaseNotReadOnly
Indicates whether the declared array base-type universe modifier must be checked when accessing the array.


isCastedToRep

private boolean isCastedToRep
Was something casted to rep ? Needed for arrays casted to rep to remember that it was casted.

See Also:
visitArrayAccessExpression(JArrayAccessExpression)

potentiallyNotAdmissible

private JExpression potentiallyNotAdmissible
In order to get meaningful error messages, the JExpression where needsRep was set is stored.


stateStack

private final Stack stateStack
The state of this JmlOwnershipAdmissibilityVisitor is often saved at the beginning of a visit-method, and restored at its end. To avoid tedious introduction of local variables and so on, stateStack can be used to save, restore and clear the current state.

See Also:
pushState(), popState(), clearCurrentState(), JmlOwnershipAdmissibilityVisitor.State
Constructor Detail

JmlOwnershipAdmissibilityVisitor

JmlOwnershipAdmissibilityVisitor()
Method Detail

pushState

private void pushState()
Stores a copy of the current state and pushes this copy onto the top if stateStack. The state of "this" is left unchanged.


popState

private void popState()
Restores the last pushed state. The st


clearCurrentState

private void clearCurrentState()
Clears the current state of this visitor, i.e. sets all fields to their initial value. stateStack is not affected.


visit

protected void visit(JExpression expr)
Description copied from class: JmlAdmissibilityVisitor
This method calls the JExpression.accept(MjcVisitor) method of expr. It enables subclasses overridding this method to introduce custom initialization and termination control.

Overrides:
visit in class JmlAdmissibilityVisitor

visitArrayAccessExpression

public void visitArrayAccessExpression(JArrayAccessExpression self)
Visits the given array access expression, self. By default, this method visits both prefix and accessor of self. The logic is as follows: needsRep && isCastedToRep && isArrayBaseElement: impossible needsRep && isCastedToRep && !isArrayBaseElement: impossible needsRep && !isCastedToRep && isArrayBaseElement: set needsArrayBaseNotReadOnly needsRep && !isCastedToRep && !isArrayBaseElement: no action !needsRep && isCastedToRep && isArrayBaseElement: clear isCastedToRep, set needsRep !needsRep && isCastedToRep && !isArrayBaseElement: no action !needsRep && !isCastedToRep && isArrayBaseElement: set needsRep !needsRep && !isCastedToRep && !isArrayBaseElement: set needsRep

Specified by:
visitArrayAccessExpression in interface MjcVisitor
Overrides:
visitArrayAccessExpression in class AbstractExpressionVisitor

visitFieldExpression

public void visitFieldExpression(JClassFieldExpression self)
Visits the given class field expression, self. By default, this method visits the prefix of self if it is not null.

Specified by:
visitFieldExpression in interface MjcVisitor
Overrides:
visitFieldExpression in class AbstractExpressionVisitor

visitMethodCallExpression

public void visitMethodCallExpression(JMethodCallExpression self)
Visits the given method expression, self. By default, this method visits both prefix and arguments of self. Method calls are not supported yet, but the receiver object and the method parameters are checked.

Specified by:
visitMethodCallExpression in interface MjcVisitor
Overrides:
visitMethodCallExpression in class AbstractExpressionVisitor

visitNewObjectExpression

public void visitNewObjectExpression(JNewObjectExpression self)
Visits the given new object expression, self. By default, this method visits both the this expression and parameters of self. Object creation is not supported yet, but the receiver object and the parameters are checked.

Specified by:
visitNewObjectExpression in interface MjcVisitor
Overrides:
visitNewObjectExpression in class AbstractExpressionVisitor

visitConditionalExpression

public void visitConditionalExpression(JConditionalExpression self)
Visits the given conditional expression, self. By default, this method visits the condition, left and right expressions of self.

Specified by:
visitConditionalExpression in interface MjcVisitor
Overrides:
visitConditionalExpression in class AbstractExpressionVisitor

visitArrayDimsAndInit

public void visitArrayDimsAndInit(JArrayDimsAndInits self)
Visits the given array dimension and initializer, self. By default, this method visits both the dimension expression and initializer of self.

Specified by:
visitArrayDimsAndInit in interface MjcVisitor
Overrides:
visitArrayDimsAndInit in class AbstractExpressionVisitor

visitThisExpression

public void visitThisExpression(JThisExpression self)
Visits the given this expression, self. By default, this method does nothing.

Specified by:
visitThisExpression in interface MjcVisitor
Overrides:
visitThisExpression in class AbstractExpressionVisitor

visitCastExpression

public void visitCastExpression(JCastExpression self)
Visits the given cast expression, self. By default, this method visits the expression of self. If the cast does not involve universe types, then there is no problem, otherwise ...

Specified by:
visitCastExpression in interface MjcVisitor
Overrides:
visitCastExpression in class AbstractExpressionVisitor

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.