org.jmlspecs.checker
Class JmlOwnershipAdmissibilityVisitor

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.checker.JmlAbstractVisitor
          org.jmlspecs.jmlrac.RacAbstractVisitor
              org.jmlspecs.jmlrac.qexpr.AbstractExpressionVisitor
                  org.jmlspecs.checker.JmlAdmissibilityVisitor
                      org.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

JmlOwnershipAdmissibilityVisitor

JmlOwnershipAdmissibilityVisitor()

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