JML

org.jmlspecs.checker
Class JmlExpressionChecker

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.checker.JmlAbstractVisitor
          extended byorg.jmlspecs.checker.JmlExpressionChecker
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor

public class JmlExpressionChecker
extends JmlAbstractVisitor

A visitor class to check privacy (and purity) of JML expressions.

Version:
$Revision: 1.31 $
Author:
Yoonsik Cheon

Field Summary
private  boolean checkPurity
          Indicates whether to check purity or not.
private  CContextType context
          The context with which to report error if an error is found while checking visibility and purity.
private  long privacy
          The visibility of specification context against which JML expressions are checked for visibility.
private  boolean sideEffectOk
          Indicates if side effects are ok.
 
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
 
Constructor Summary
private JmlExpressionChecker(CContextType ctx, long privacy)
          Constructs a new instance.
private JmlExpressionChecker(CContextType ctx, long privacy, boolean checkPurity)
          Constructs a new instance.
private JmlExpressionChecker(CContextType ctx, long privacy, boolean checkPurity, boolean sideEffectOk)
           
 
Method Summary
private  void check(boolean cond, TokenReference tref, MessageDescription msg)
          Checks if the condition, cond is true.
private  void check(boolean cond, TokenReference tref, MessageDescription msg, Object obj1)
          Checks if the condition, cond is true.
private  void check(boolean cond, TokenReference tref, MessageDescription msg, Object obj1, Object obj2)
          Checks if the condition, cond is true.
private  void check(boolean cond, TokenReference tref, MessageDescription msg, Object[] obj)
           
private  void checkType(CType type, TokenReference ref)
          Checks the visibility of the given type, type.
private  void checkTypeHelper(CClass clazz, TokenReference ref)
          Checks the visibility of the given class, clazz.
private  CType getBaseType(CType type)
          Returns the ultimate base type if the given type, type, is an array type.
private static boolean isModelFieldReference(JExpression expr)
          Returns true if the given expression, expr is a reference to a model field.
static boolean isVisibilityOk(long privacy, long modifiers)
          Returns true if a member (field or method) with the given modifiers, modifiers, can be used in a specification context of the visibility, privacy.
private  int methodPureness(CMethod meth, JExpression prefix)
          Returns 1 if the given method, meth, is a pure method.
static void perform(CContextType ctx, long privacy, JExpression expr)
          Checks visibility (and purity) of the given expression, expr, in the specification context of visibility, privacy.
static void perform(CContextType ctx, long privacy, JExpression expr, boolean checkPurity)
          Checks visibility (and purity) of the given expression, expr, in the specification context of visibility, privacy.
static void perform(CContextType ctx, JExpression expr)
          Checks purity of the given expression, expr.
static void performSideEffectOk(CContextType ctx, JExpression expr)
          Checks the given expression allowing side effects.
 void visitAddExpression(JAddExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitArrayAccessExpression(JArrayAccessExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitArrayDimsAndInit(JArrayDimsAndInits self)
          Checks visibility (and purity) of the given expression, self.
 void visitArrayInitializer(JArrayInitializer self)
          Checks visibility (and purity) of the given expression, self.
 void visitArrayLengthExpression(JArrayLengthExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitAssignmentExpression(JAssignmentExpression self)
          Checks visibility (and purity) of the given expression, self.
protected  void visitBinaryExpression(JBinaryExpression expr)
          Checks visibility (and purity) of the given binary expression, expr.
 void visitBitwiseExpression(JBitwiseExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitCastExpression(JCastExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitClassExpression(JClassExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitConditionalAndExpression(JConditionalAndExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitConditionalExpression(JConditionalExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitConditionalOrExpression(JConditionalOrExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitDivideExpression(JDivideExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitEqualityExpression(JEqualityExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitExplicitConstructorInvocation(JExplicitConstructorInvocation self)
          Checks visibility (and purity) of the given expression, self.
protected  void visitExpressions(JExpression[] exprs)
          Checks visibility (and purity) of the given expressions, expr.
 void visitFieldExpression(JClassFieldExpression self)
          Checks the given class field expression for visibility and purity violations.
 void visitInstanceofExpression(JInstanceofExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlCodeContract(JmlCodeContract self)
           
 void visitJmlDurationExpression(JmlDurationExpression self)
          Checks visibility of the given expression, self.
 void visitJmlElemTypeExpression(JmlElemTypeExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlFreshExpression(JmlFreshExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlInformalExpression(JmlInformalExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlInGroupClause(JmlInGroupClause self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlInvariantForExpression(JmlInvariantForExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlLabelExpression(JmlLabelExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlLockSetExpression(JmlLockSetExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlMapsIntoClause(JmlMapsIntoClause self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlOldExpression(JmlOldExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlPredicate(JmlPredicate self)
           
 void visitJmlPreExpression(JmlPreExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlReachExpression(JmlReachExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlRelationalExpression(JmlRelationalExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlResultExpression(JmlResultExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlSetComprehension(JmlSetComprehension self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlSpaceExpression(JmlSpaceExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlSpecExpression(JmlSpecExpression self)
           
 void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlTypeExpression(JmlTypeExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlTypeOfExpression(JmlTypeOfExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlVariableDefinition(JmlVariableDefinition self)
          Checks visibility (and purity) of the given expression, self.
 void visitJmlWorkingSpaceExpression(JmlWorkingSpaceExpression self)
          Checks visibility of the given expression, self.
 void visitLocalVariableExpression(JLocalVariableExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitMathModeExpression(MJMathModeExpression self)
          Checks visibility (and purity) of the given expression.
 void visitMethodCallExpression(JMethodCallExpression self)
          Checks the given method call expression for visibility and purity violations.
 void visitMinusExpression(JMinusExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitModuloExpression(JModuloExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitMultExpression(JMultExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitNameExpression(JNameExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitNewAnonymousClassExpression(JNewAnonymousClassExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitNewArrayExpression(JNewArrayExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitNewObjectExpression(JNewObjectExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitParenthesedExpression(JParenthesedExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitPostfixExpression(JPostfixExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitPrefixExpression(JPrefixExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitRelationalExpression(JRelationalExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitShiftExpression(JShiftExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitSuperExpression(JSuperExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitThisExpression(JThisExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitTypeNameExpression(JTypeNameExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitUnaryExpression(JUnaryExpression self)
          Checks visibility (and purity) of the given expression, self.
 void visitUnaryPromoteExpression(JUnaryPromote self)
          Checks visibility (and purity) of the given expression, self.
 void visitVariableDefinition(JVariableDefinition self)
          Checks visibility (and purity) of the given expression, self.
 void visitWarnExpression(MJWarnExpression self)
          Checks visibility (and purity) of the given expression.
private  void warnPureness(int cond, TokenReference tref, Object obj)
          Produce a caution message about method pureness if the argument, cond, is -1.
 
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, 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, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantStatement, visitJmlLetVarDecl, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMaxExpression, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNormalBehaviorSpec, visitJmlNormalExample, visitJmlNormalSpecBody, visitJmlNormalSpecCase, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicateKeyword, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlReturnsClause, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpecBody, visitJmlSpecification, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlUnreachableStatement, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWritableIfVarAssertion, visitLabeledStatement, visitLongLiteral, visitMethodDeclaration, visitNullLiteral, visitOrdinalLiteral, visitPackageImport, visitPackageName, visitRealLiteral, visitReturnStatement, visitShortLiteral, visitStringLiteral, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitVariableDeclarationStatement, 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
 

Field Detail

context

private CContextType context
The context with which to report error if an error is found while checking visibility and purity.


privacy

private long privacy
The visibility of specification context against which JML expressions are checked for visibility.

 private invariant privacy == ACC_PUBLIC || privacy == ACC_SPEC_PUBLIC
   || privacy == ACC_PROTECTED || privacy == ACC_SPEC_PROTECTED
   || privacy == ACC_PRIVATE 
   || privacy == 0;
 


checkPurity

private boolean checkPurity
Indicates whether to check purity or not. For a particular context such as accessible clause and callable clause, the purity check should not be performed.


sideEffectOk

private boolean sideEffectOk
Indicates if side effects are ok. E.g., in the debug statement.

Constructor Detail

JmlExpressionChecker

private JmlExpressionChecker(CContextType ctx,
                             long privacy)
Constructs a new instance.

 requires privacy == ACC_PUBLIC || privacy == ACC_SPEC_PUBLIC
   || privacy == ACC_PROTECTED || privacy == ACC_SPEC_PROTECTED
   || privacy == ACC_PRIVATE 
   || privacy == 0;
 


JmlExpressionChecker

private JmlExpressionChecker(CContextType ctx,
                             long privacy,
                             boolean checkPurity)
Constructs a new instance.

 requires privacy == ACC_PUBLIC || privacy == ACC_SPEC_PUBLIC
   || privacy == ACC_PROTECTED || privacy == ACC_SPEC_PROTECTED
   || privacy == ACC_PRIVATE 
   || privacy == 0;
 


JmlExpressionChecker

private JmlExpressionChecker(CContextType ctx,
                             long privacy,
                             boolean checkPurity,
                             boolean sideEffectOk)
Method Detail

perform

public static void perform(CContextType ctx,
                           long privacy,
                           JExpression expr,
                           boolean checkPurity)
Checks visibility (and purity) of the given expression, expr, in the specification context of visibility, privacy. If there is an error, it is reported using the given context, ctx. The purity check is performed only if the argument checkPurity is true.

 requires privacy == ACC_PUBLIC || privacy == ACC_SPEC_PUBLIC
   || privacy == ACC_PROTECTED || privacy == ACC_SPEC_PROTECTED
   || privacy == ACC_PRIVATE 
   || privacy == 0;
 


perform

public static void perform(CContextType ctx,
                           long privacy,
                           JExpression expr)
Checks visibility (and purity) of the given expression, expr, in the specification context of visibility, privacy. If there is an error, it is reported using the given context, ctx.

 requires privacy == ACC_PUBLIC || privacy == ACC_SPEC_PUBLIC
   || privacy == ACC_PROTECTED || privacy == ACC_SPEC_PROTECTED
   || privacy == ACC_PRIVATE 
   || privacy == 0;
 


perform

public static void perform(CContextType ctx,
                           JExpression expr)
Checks purity of the given expression, expr. If there is an error, it is reported using the given context, ctx.


performSideEffectOk

public static void performSideEffectOk(CContextType ctx,
                                       JExpression expr)
Checks the given expression allowing side effects.


visitJmlCodeContract

public void visitJmlCodeContract(JmlCodeContract self)
Specified by:
visitJmlCodeContract in interface JmlVisitor
Overrides:
visitJmlCodeContract in class JmlAbstractVisitor

visitJmlDurationExpression

public void visitJmlDurationExpression(JmlDurationExpression self)
Checks visibility of the given expression, self.

Specified by:
visitJmlDurationExpression in interface JmlVisitor
Overrides:
visitJmlDurationExpression in class JmlAbstractVisitor

visitJmlPredicate

public void visitJmlPredicate(JmlPredicate self)
Specified by:
visitJmlPredicate in interface JmlVisitor
Overrides:
visitJmlPredicate in class JmlAbstractVisitor

visitJmlSpecExpression

public void visitJmlSpecExpression(JmlSpecExpression self)
Specified by:
visitJmlSpecExpression in interface JmlVisitor
Overrides:
visitJmlSpecExpression in class JmlAbstractVisitor

visitJmlNotModifiedExpression

public void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlNotModifiedExpression in interface JmlVisitor
Overrides:
visitJmlNotModifiedExpression in class JmlAbstractVisitor

visitJmlNotAssignedExpression

public void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlNotAssignedExpression in interface JmlVisitor
Overrides:
visitJmlNotAssignedExpression in class JmlAbstractVisitor

visitJmlNonNullElementsExpression

public void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlNonNullElementsExpression in interface JmlVisitor
Overrides:
visitJmlNonNullElementsExpression in class JmlAbstractVisitor

visitJmlElemTypeExpression

public void visitJmlElemTypeExpression(JmlElemTypeExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlElemTypeExpression in interface JmlVisitor
Overrides:
visitJmlElemTypeExpression in class JmlAbstractVisitor

visitJmlFreshExpression

public void visitJmlFreshExpression(JmlFreshExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlFreshExpression in interface JmlVisitor
Overrides:
visitJmlFreshExpression in class JmlAbstractVisitor

visitJmlInGroupClause

public void visitJmlInGroupClause(JmlInGroupClause self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlInGroupClause in interface JmlVisitor
Overrides:
visitJmlInGroupClause in class JmlAbstractVisitor

visitJmlInformalExpression

public void visitJmlInformalExpression(JmlInformalExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlInformalExpression in interface JmlVisitor
Overrides:
visitJmlInformalExpression in class JmlAbstractVisitor

visitJmlInvariantForExpression

public void visitJmlInvariantForExpression(JmlInvariantForExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlInvariantForExpression in interface JmlVisitor
Overrides:
visitJmlInvariantForExpression in class JmlAbstractVisitor

visitJmlIsInitializedExpression

public void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlIsInitializedExpression in interface JmlVisitor
Overrides:
visitJmlIsInitializedExpression in class JmlAbstractVisitor

visitJmlLabelExpression

public void visitJmlLabelExpression(JmlLabelExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlLabelExpression in interface JmlVisitor
Overrides:
visitJmlLabelExpression in class JmlAbstractVisitor

visitJmlLockSetExpression

public void visitJmlLockSetExpression(JmlLockSetExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlLockSetExpression in interface JmlVisitor
Overrides:
visitJmlLockSetExpression in class JmlAbstractVisitor

visitJmlMapsIntoClause

public void visitJmlMapsIntoClause(JmlMapsIntoClause self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlMapsIntoClause in interface JmlVisitor
Overrides:
visitJmlMapsIntoClause in class JmlAbstractVisitor

visitJmlOldExpression

public void visitJmlOldExpression(JmlOldExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlOldExpression in interface JmlVisitor
Overrides:
visitJmlOldExpression in class JmlAbstractVisitor

visitJmlPreExpression

public void visitJmlPreExpression(JmlPreExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlPreExpression in interface JmlVisitor
Overrides:
visitJmlPreExpression in class JmlAbstractVisitor

visitJmlReachExpression

public void visitJmlReachExpression(JmlReachExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlReachExpression in interface JmlVisitor
Overrides:
visitJmlReachExpression in class JmlAbstractVisitor

visitJmlResultExpression

public void visitJmlResultExpression(JmlResultExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlResultExpression in interface JmlVisitor
Overrides:
visitJmlResultExpression in class JmlAbstractVisitor

visitJmlSetComprehension

public void visitJmlSetComprehension(JmlSetComprehension self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlSetComprehension in interface JmlVisitor
Overrides:
visitJmlSetComprehension in class JmlAbstractVisitor

visitJmlSpaceExpression

public void visitJmlSpaceExpression(JmlSpaceExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlSpaceExpression in interface JmlVisitor
Overrides:
visitJmlSpaceExpression in class JmlAbstractVisitor

visitJmlSpecQuantifiedExpression

public void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlSpecQuantifiedExpression in interface JmlVisitor
Overrides:
visitJmlSpecQuantifiedExpression in class JmlAbstractVisitor

visitJmlVariableDefinition

public void visitJmlVariableDefinition(JmlVariableDefinition self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlVariableDefinition in interface JmlVisitor
Overrides:
visitJmlVariableDefinition in class JmlAbstractVisitor

visitVariableDefinition

public void visitVariableDefinition(JVariableDefinition self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitVariableDefinition in interface MjcVisitor
Overrides:
visitVariableDefinition in class JmlAbstractVisitor

visitJmlTypeExpression

public void visitJmlTypeExpression(JmlTypeExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlTypeExpression in interface JmlVisitor
Overrides:
visitJmlTypeExpression in class JmlAbstractVisitor

visitJmlTypeOfExpression

public void visitJmlTypeOfExpression(JmlTypeOfExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlTypeOfExpression in interface JmlVisitor
Overrides:
visitJmlTypeOfExpression in class JmlAbstractVisitor

visitJmlWorkingSpaceExpression

public void visitJmlWorkingSpaceExpression(JmlWorkingSpaceExpression self)
Checks visibility of the given expression, self.

Specified by:
visitJmlWorkingSpaceExpression in interface JmlVisitor
Overrides:
visitJmlWorkingSpaceExpression in class JmlAbstractVisitor

visitAssignmentExpression

public void visitAssignmentExpression(JAssignmentExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitAssignmentExpression in interface MjcVisitor
Overrides:
visitAssignmentExpression in class JmlAbstractVisitor

visitCompoundAssignmentExpression

public void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitCompoundAssignmentExpression in interface MjcVisitor
Overrides:
visitCompoundAssignmentExpression in class JmlAbstractVisitor

visitConditionalExpression

public void visitConditionalExpression(JConditionalExpression self)
Checks visibility (and purity) of the given expression, self.

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

visitJmlRelationalExpression

public void visitJmlRelationalExpression(JmlRelationalExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitJmlRelationalExpression in interface JmlVisitor
Overrides:
visitJmlRelationalExpression in class JmlAbstractVisitor

visitConditionalAndExpression

public void visitConditionalAndExpression(JConditionalAndExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitConditionalAndExpression in interface MjcVisitor
Overrides:
visitConditionalAndExpression in class JmlAbstractVisitor

visitConditionalOrExpression

public void visitConditionalOrExpression(JConditionalOrExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitConditionalOrExpression in interface MjcVisitor
Overrides:
visitConditionalOrExpression in class JmlAbstractVisitor

visitBitwiseExpression

public void visitBitwiseExpression(JBitwiseExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitBitwiseExpression in interface MjcVisitor
Overrides:
visitBitwiseExpression in class JmlAbstractVisitor

visitEqualityExpression

public void visitEqualityExpression(JEqualityExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitEqualityExpression in interface MjcVisitor
Overrides:
visitEqualityExpression in class JmlAbstractVisitor

visitRelationalExpression

public void visitRelationalExpression(JRelationalExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitRelationalExpression in interface MjcVisitor
Overrides:
visitRelationalExpression in class JmlAbstractVisitor

visitInstanceofExpression

public void visitInstanceofExpression(JInstanceofExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitInstanceofExpression in interface MjcVisitor
Overrides:
visitInstanceofExpression in class JmlAbstractVisitor

visitAddExpression

public void visitAddExpression(JAddExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitAddExpression in interface MjcVisitor
Overrides:
visitAddExpression in class JmlAbstractVisitor

visitMinusExpression

public void visitMinusExpression(JMinusExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitMinusExpression in interface MjcVisitor
Overrides:
visitMinusExpression in class JmlAbstractVisitor

visitMultExpression

public void visitMultExpression(JMultExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitMultExpression in interface MjcVisitor
Overrides:
visitMultExpression in class JmlAbstractVisitor

visitDivideExpression

public void visitDivideExpression(JDivideExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitDivideExpression in interface MjcVisitor
Overrides:
visitDivideExpression in class JmlAbstractVisitor

visitModuloExpression

public void visitModuloExpression(JModuloExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitModuloExpression in interface MjcVisitor
Overrides:
visitModuloExpression in class JmlAbstractVisitor

visitShiftExpression

public void visitShiftExpression(JShiftExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitShiftExpression in interface MjcVisitor
Overrides:
visitShiftExpression in class JmlAbstractVisitor

visitPrefixExpression

public void visitPrefixExpression(JPrefixExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitPrefixExpression in interface MjcVisitor
Overrides:
visitPrefixExpression in class JmlAbstractVisitor

visitPostfixExpression

public void visitPostfixExpression(JPostfixExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitPostfixExpression in interface MjcVisitor
Overrides:
visitPostfixExpression in class JmlAbstractVisitor

visitUnaryExpression

public void visitUnaryExpression(JUnaryExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitUnaryExpression in interface MjcVisitor
Overrides:
visitUnaryExpression in class JmlAbstractVisitor

visitCastExpression

public void visitCastExpression(JCastExpression self)
Checks visibility (and purity) of the given expression, self.

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

visitUnaryPromoteExpression

public void visitUnaryPromoteExpression(JUnaryPromote self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitUnaryPromoteExpression in interface MjcVisitor
Overrides:
visitUnaryPromoteExpression in class JmlAbstractVisitor

visitMethodCallExpression

public void visitMethodCallExpression(JMethodCallExpression self)
Checks the given method call expression for visibility and purity violations.

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

visitTypeNameExpression

public void visitTypeNameExpression(JTypeNameExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitTypeNameExpression in interface MjcVisitor
Overrides:
visitTypeNameExpression in class JmlAbstractVisitor

visitThisExpression

public void visitThisExpression(JThisExpression self)
Checks visibility (and purity) of the given expression, self.

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

visitSuperExpression

public void visitSuperExpression(JSuperExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitSuperExpression in interface MjcVisitor
Overrides:
visitSuperExpression in class JmlAbstractVisitor

visitClassExpression

public void visitClassExpression(JClassExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitClassExpression in interface MjcVisitor
Overrides:
visitClassExpression in class JmlAbstractVisitor

visitExplicitConstructorInvocation

public void visitExplicitConstructorInvocation(JExplicitConstructorInvocation self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitExplicitConstructorInvocation in interface MjcVisitor
Overrides:
visitExplicitConstructorInvocation in class JmlAbstractVisitor

visitArrayLengthExpression

public void visitArrayLengthExpression(JArrayLengthExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitArrayLengthExpression in interface MjcVisitor
Overrides:
visitArrayLengthExpression in class JmlAbstractVisitor

visitArrayAccessExpression

public void visitArrayAccessExpression(JArrayAccessExpression self)
Checks visibility (and purity) of the given expression, self.

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

visitNameExpression

public void visitNameExpression(JNameExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitNameExpression in interface MjcVisitor
Overrides:
visitNameExpression in class JmlAbstractVisitor

visitLocalVariableExpression

public void visitLocalVariableExpression(JLocalVariableExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitLocalVariableExpression in interface MjcVisitor
Overrides:
visitLocalVariableExpression in class JmlAbstractVisitor

visitParenthesedExpression

public void visitParenthesedExpression(JParenthesedExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitParenthesedExpression in interface MjcVisitor
Overrides:
visitParenthesedExpression in class JmlAbstractVisitor

visitNewObjectExpression

public void visitNewObjectExpression(JNewObjectExpression self)
Checks visibility (and purity) of the given expression, self.

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

visitNewAnonymousClassExpression

public void visitNewAnonymousClassExpression(JNewAnonymousClassExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitNewAnonymousClassExpression in interface MjcVisitor
Overrides:
visitNewAnonymousClassExpression in class JmlAbstractVisitor

visitNewArrayExpression

public void visitNewArrayExpression(JNewArrayExpression self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitNewArrayExpression in interface MjcVisitor
Overrides:
visitNewArrayExpression in class JmlAbstractVisitor

visitArrayDimsAndInit

public void visitArrayDimsAndInit(JArrayDimsAndInits self)
Checks visibility (and purity) of the given expression, self.

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

visitArrayInitializer

public void visitArrayInitializer(JArrayInitializer self)
Checks visibility (and purity) of the given expression, self.

Specified by:
visitArrayInitializer in interface MjcVisitor
Overrides:
visitArrayInitializer in class JmlAbstractVisitor

visitFieldExpression

public void visitFieldExpression(JClassFieldExpression self)
Checks the given class field expression for visibility and purity violations.

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

visitWarnExpression

public void visitWarnExpression(MJWarnExpression self)
Checks visibility (and purity) of the given expression.

Specified by:
visitWarnExpression in interface MjcVisitor
Overrides:
visitWarnExpression in class JmlAbstractVisitor

visitMathModeExpression

public void visitMathModeExpression(MJMathModeExpression self)
Checks visibility (and purity) of the given expression.

Specified by:
visitMathModeExpression in interface MjcVisitor
Overrides:
visitMathModeExpression in class JmlAbstractVisitor

visitExpressions

protected void visitExpressions(JExpression[] exprs)
Checks visibility (and purity) of the given expressions, expr.


visitBinaryExpression

protected void visitBinaryExpression(JBinaryExpression expr)
Checks visibility (and purity) of the given binary expression, expr.


check

private void check(boolean cond,
                   TokenReference tref,
                   MessageDescription msg,
                   Object obj1,
                   Object obj2)
Checks if the condition, cond is true. If not, reports a positioned error.


check

private void check(boolean cond,
                   TokenReference tref,
                   MessageDescription msg,
                   Object[] obj)

check

private void check(boolean cond,
                   TokenReference tref,
                   MessageDescription msg,
                   Object obj1)
Checks if the condition, cond is true. If not, reports a positioned error.


check

private void check(boolean cond,
                   TokenReference tref,
                   MessageDescription msg)
Checks if the condition, cond is true. If not, reports a positioned error.


warnPureness

private void warnPureness(int cond,
                          TokenReference tref,
                          Object obj)
Produce a caution message about method pureness if the argument, cond, is -1. If cond is 0, produce a warning message instead; otherwise, do nothing.


isVisibilityOk

public static boolean isVisibilityOk(long privacy,
                                     long modifiers)
Returns true if a member (field or method) with the given modifiers, modifiers, can be used in a specification context of the visibility, privacy.

 requires privacy == ACC_PUBLIC || privacy == ACC_SPEC_PUBLIC
   || privacy == ACC_PROTECTED || privacy == ACC_SPEC_PROTECTED
   || privacy == ACC_PRIVATE 
   || privacy == 0;
 


checkType

private void checkType(CType type,
                       TokenReference ref)
Checks the visibility of the given type, type. If the given type is an array type, the visibility of its base type is checked. For a nested type, also checks the owner type's visibility. If there is a visibility violation, throw an error message composed using the given token reference, ref.


checkTypeHelper

private void checkTypeHelper(CClass clazz,
                             TokenReference ref)
Checks the visibility of the given class, clazz. For a nested class, also checks the owner class's visibility. If there is a visibility violation, throw an error message composed using the given token reference, ref.


getBaseType

private CType getBaseType(CType type)
Returns the ultimate base type if the given type, type, is an array type. Otherwise, returns the type itself.


methodPureness

private int methodPureness(CMethod meth,
                           JExpression prefix)
Returns 1 if the given method, meth, is a pure method. A method is pure if it is annoted with the JML pure modifier or its owner (a class or an interface) is declared as pure. Returns -1 if the given method is not pure; returns 0 if it can not be determined, e.g., no source code is available.


isModelFieldReference

private static boolean isModelFieldReference(JExpression expr)
Returns true if the given expression, expr is a reference to a model field.


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.