org.jmlspecs.checker
Class JmlExpressionChecker

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.checker.JmlAbstractVisitor
          org.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.

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)

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;