org.jmlspecs.checker
Class JmlAdmissibilityVisitor

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.checker.JmlAbstractVisitor
          org.jmlspecs.jmlrac.RacAbstractVisitor
              org.jmlspecs.jmlrac.qexpr.AbstractExpressionVisitor
                  org.jmlspecs.checker.JmlAdmissibilityVisitor

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor, RacConstants, RacVisitor

Direct Known Subclasses:

JmlClassicalAdmissibilityVisitor, JmlOwnershipAdmissibilityVisitor

public abstract class JmlAdmissibilityVisitor

extends AbstractExpressionVisitor

A visitor class to check admissibility of JML invariants and represents clauses. Static invariants and static represents clauses, as well as static fields and methods calls appearing in invariants and represents clauses are not yet supported. For more datails about admissibility see "Modular Invariants for Layered Object Structures" by P. Mueller, A. Poetzsch-Heffter and G. Leavens, 2004. FIXME: Known Issues: 1. New Array Creation with Initializer: new Object{peerfield}[0] is admissible but rejected. Hard to fix (IMHO) 2. Hidden this: (field < 0 ? this : this).field == 0 is admissible but rejected. Quite easy to fix (IMHO)

Version:

0.01

Author:

rzakhejm

Nested Class Summary
protected  class	JmlAdmissibilityVisitor.NotAdmissibleException           An Exception which is thrown when some was found not to be admissible.

 

Field Summary
static String	ADMISSIBILITY_CLASSICAL           Command line option to enable classical admissibility checks
static String	ADMISSIBILITY_NONE           Command line option to disable admissibility checks
static String	ADMISSIBILITY_OWNERSHIP           Command line option to enable ownership admissibility checks
protected  JmlExpressionContext	ectx           The context of the expression to check
protected  boolean	hasErrorsOrWarnings           Whether warnings or errors occured during the admissibility check.
protected  CFieldAccessor	modelField           In the case of a represents clause, this field saves a reference to the model field, in order to enable it to appear in the represents expression and to ignore subclass separation for this field.

 

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

JmlAdmissibilityVisitor()

 

Method Summary
protected static boolean	checkAdmissibility(JExpression expr, JmlExpressionContext ectx, CFieldAccessor modelField)           Admissibility checks a JExpression.
static boolean	checkInvariant(JmlInvariant expr, JmlExpressionContext ectx)           Admissibility checks an invariant.
static boolean	checkRepresentsClause(JmlRepresentsDecl decl, JmlExpressionContext ectx)           Admissibility checks a represents clause.
private static String	getAdmissibility()           This method takes the command line admissibility string and returns the appropriate canonical admissibility option string.
private static JmlAdmissibilityVisitor	getVisitor()           Returns a new instance of the appropriate subclass of JmlAdmissibilityVisitor or null according to the chosen command line option "ownership", "classical" or "none."
static boolean	isAdmissibilityCheckEnabled()           Are the admissibility checks enabled ?
static boolean	isAdmissibilityOwnershipEnabled()           Is the ownership admissibility check enabled ?
protected static boolean	isThisAfterCasts(JExpression expr)           Whether the expr, after removing casts (JCastExpression, JUnaryPromote) is of type JThisExpression.
protected static JExpression	removeParentheses(JExpression expr)           If expr is of type JParenthesedExpression, this method returns the first child of expr which is not a JPatenthesedExpression.
protected  void	visit(JExpression expr)           This method calls the JExpression.accept(MjcVisitor) method of expr.
protected  void	warn(JExpression expr, MessageDescription desc)           Emits a warning.

 

Methods inherited from class org.jmlspecs.jmlrac.qexpr.AbstractExpressionVisitor

visitAddExpression, visitArrayAccessExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssignmentExpression, visitBinaryExpression, visitBitwiseExpression, visitCastExpression, visitClassExpression, visitCompoundAssignmentExpression, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitDivideExpression, visitEqualityExpression, visitExplicitConstructorInvocation, visitExpressions, visitFieldExpression, 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, visitMethodCallExpression, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitNewObjectExpression, visitParenthesedExpression, visitPostfixExpression, visitPrefixExpression, visitRelationalExpression, visitShiftExpression, visitSuperExpression, visitThisExpression, 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

ADMISSIBILITY_CLASSICAL

public static final String ADMISSIBILITY_CLASSICAL

Command line option to enable classical admissibility checks

ADMISSIBILITY_NONE

public static final String ADMISSIBILITY_NONE

Command line option to disable admissibility checks

ADMISSIBILITY_OWNERSHIP

public static final String ADMISSIBILITY_OWNERSHIP

Command line option to enable ownership admissibility checks

ectx

protected JmlExpressionContext ectx

The context of the expression to check

hasErrorsOrWarnings

protected boolean hasErrorsOrWarnings

Whether warnings or errors occured during the admissibility check. Errors and warnings are not distinguished since in both cases admissibility is not (yet) assured. An error occures when an expression is not admissible, a warning when certain language constructs are not (yet) supported.

modelField

protected CFieldAccessor modelField

In the case of a represents clause, this field saves a reference to the model field, in order to enable it to appear in the represents expression and to ignore subclass separation for this field.

JmlAdmissibilityVisitor

public JmlAdmissibilityVisitor()

checkInvariant

public static boolean checkInvariant(JmlInvariant expr,
                                     JmlExpressionContext ectx)

Admissibility checks an invariant. The invariant should already be typechecked.

Parameters:

expr - The invariant to check

ectx - its context

Returns:

whether the invariant is admissible

checkRepresentsClause

public static boolean checkRepresentsClause(JmlRepresentsDecl decl,
                                            JmlExpressionContext ectx)

Admissibility checks a represents clause. Both, functional and relational clauses are supported. The represents clause should already be typechecked.

Parameters:

decl - The represents clause to check

ectx - its context

Returns:

whether the represents clause is admissible

isAdmissibilityCheckEnabled

public static boolean isAdmissibilityCheckEnabled()

Are the admissibility checks enabled ?

Returns:

true if some admissibility check is enabled

isAdmissibilityOwnershipEnabled

public static boolean isAdmissibilityOwnershipEnabled()

Is the ownership admissibility check enabled ?

Returns:

true if the ownership admissibility check is enabled

checkAdmissibility

protected static boolean checkAdmissibility(JExpression expr,
                                            JmlExpressionContext ectx,
                                            CFieldAccessor modelField)

Admissibility checks a JExpression.

Parameters:

expr - the predicate to check

ectx - its context

modelField - the modelfield to check in case of a represents clause or null in case of an invariant.

Returns:

whether errors or warnings occured during checking

removeParentheses

protected static JExpression removeParentheses(JExpression expr)

If expr is of type JParenthesedExpression, this method returns the first child of expr which is not a JPatenthesedExpression.

Parameters:

expr - the expression to remove its parentheses.

Returns:

the first child of expr not a parentheses.

isThisAfterCasts

protected static boolean isThisAfterCasts(JExpression expr)

Whether the expr, after removing casts (JCastExpression, JUnaryPromote) is of type JThisExpression.

Parameters:

expr - to check for a this in casts

Returns:

whether it is a this after casts.

getAdmissibility

private static String getAdmissibility()

This method takes the command line admissibility string and returns the appropriate canonical admissibility option string.

Returns:

the canonical admissibility option string corresponding to the command line option, i.e. ownership, classical or none.

See Also:

ADMISSIBILITY_CLASSICAL, ADMISSIBILITY_OWNERSHIP, ADMISSIBILITY_NONE

getVisitor

private static JmlAdmissibilityVisitor getVisitor()

Returns a new instance of the appropriate subclass of JmlAdmissibilityVisitor or null according to the chosen command line option "ownership", "classical" or "none."

Returns:

a new instance of a subclass of JmlAdmissibilityVisitor for the options "ownership" and "classical", or null for "none".

warn

protected void warn(JExpression expr,
                    MessageDescription desc)
             throws JmlAdmissibilityVisitor.NotAdmissibleException

Emits a warning. Currently all admissibility errors are emitted as warnings.

Parameters:

expr - the expression the warning occured in.

desc - the warning message.

Throws:

JmlAdmissibilityVisitor.NotAdmissibleException

visit

protected void visit(JExpression expr)

This method calls the JExpression.accept(MjcVisitor) method of expr. It enables subclasses overridding this method to introduce custom initialization and termination control.

Parameters:

expr - The expr to be visited by this.