JML

org.jmlspecs.jmlrac.qexpr
Class AbstractExpressionVisitor

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.checker.JmlAbstractVisitor
          extended byorg.jmlspecs.jmlrac.RacAbstractVisitor
              extended byorg.jmlspecs.jmlrac.qexpr.AbstractExpressionVisitor
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor, RacConstants, RacVisitor
Direct Known Subclasses:
JmlAdmissibilityVisitor, QInterval.CheckRecursion, TransPostcondition.QVarChecker, TransPostExpression2.QVarChecker

public abstract class AbstractExpressionVisitor
extends RacAbstractVisitor

An abstract visitor class that visits all subexpressions of a given expression recursively. This abstract visitor class facilitates writing concrete expression visitor classes.

Version:
$Revision: 1.13 $
Author:
Yoonsik Cheon

Field Summary
 
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
AbstractExpressionVisitor()
           
 
Method Summary
 void visitAddExpression(JAddExpression self)
          Visits the given addition expression, self.
 void visitArrayAccessExpression(JArrayAccessExpression self)
          Visits the given array access expression, self.
 void visitArrayDimsAndInit(JArrayDimsAndInits self)
          Visits the given array dimension and initializer, self.
 void visitArrayInitializer(JArrayInitializer self)
          Visits the given array initializer, self.
 void visitArrayLengthExpression(JArrayLengthExpression self)
          Visits the given array lenth expression, self.
 void visitAssignmentExpression(JAssignmentExpression self)
          Visits the given assignment expression, self.
protected  void visitBinaryExpression(JBinaryExpression self)
          Visits the binary expressions, exprs.
 void visitBitwiseExpression(JBitwiseExpression self)
          Visits the given bitwise expression, self.
 void visitCastExpression(JCastExpression self)
          Visits the given cast expression, self.
 void visitClassExpression(JClassExpression self)
          Visits the given class expression, self.
 void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
          Visits the given compound assignment expression, self.
 void visitConditionalAndExpression(JConditionalAndExpression self)
          Visits the given conditional and expression, self.
 void visitConditionalExpression(JConditionalExpression self)
          Visits the given conditional expression, self.
 void visitConditionalOrExpression(JConditionalOrExpression self)
          Visits the given condition or expression, self.
 void visitDivideExpression(JDivideExpression self)
          Visits the given division expression, self.
 void visitEqualityExpression(JEqualityExpression self)
          Visits the given equality expression, self.
 void visitExplicitConstructorInvocation(JExplicitConstructorInvocation self)
          Visits the given explicit constructor invocation, self.
protected  void visitExpressions(JExpression[] exprs)
          Visits the given expressions, exprs.
 void visitFieldExpression(JClassFieldExpression self)
          Visits the given class field expression, self.
 void visitInstanceofExpression(JInstanceofExpression self)
          Visits the given instanceof expression, self.
 void visitJmlDurationExpression(JmlDurationExpression self)
          Visits the given \duration expression, self.
 void visitJmlElemTypeExpression(JmlElemTypeExpression self)
          Visits the given elem type expression, self.
 void visitJmlFreshExpression(JmlFreshExpression self)
          Visits the given fresh expression, self.
 void visitJmlInformalExpression(JmlInformalExpression self)
          Visits the given informal description expression, self.
 void visitJmlInvariantForExpression(JmlInvariantForExpression self)
          Visits the given \invariant_for expression, self.
 void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
          Visits the given \is_initialized expression, self.
 void visitJmlLabelExpression(JmlLabelExpression self)
          Visits the given label expression, self.
 void visitJmlLockSetExpression(JmlLockSetExpression self)
          Visits the given \lockset expression, self.
 void visitJmlMaxExpression(JmlMaxExpression self)
          Visits the given \max expression, self.
 void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
          Visits the given non-null element expression, self.
 void visitJmlOldExpression(JmlOldExpression self)
          Visits the given \old expression, self.
 void visitJmlPredicate(JmlPredicate self)
          Visits the given RAC predicate, self.
 void visitJmlPreExpression(JmlPreExpression self)
          Visits the given \pre expression, self.
 void visitJmlReachExpression(JmlReachExpression self)
          Visits the given \reach expression, self.
 void visitJmlRelationalExpression(JmlRelationalExpression self)
          Visits the given JML relational expression, self.
 void visitJmlResultExpression(JmlResultExpression self)
          Visits the given \result expression, self.
 void visitJmlSetComprehension(JmlSetComprehension self)
          Visits the given set comprehension expression, self.
 void visitJmlSpaceExpression(JmlSpaceExpression self)
          Visits the given \space expression, self.
 void visitJmlSpecExpression(JmlSpecExpression self)
          Visits the given JML spec expression, self.
 void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
          Visits the given spec quantified expression, self.
 void visitJmlTypeExpression(JmlTypeExpression self)
          Visits the given \type expression, self.
 void visitJmlTypeOfExpression(JmlTypeOfExpression self)
          Visits the given \typeof expression, self.
 void visitJmlWorkingSpaceExpression(JmlWorkingSpaceExpression self)
          Visits the given \working_space expression, self.
 void visitLocalVariableExpression(JLocalVariableExpression self)
          Visits the given local variable expression, self.
 void visitMethodCallExpression(JMethodCallExpression self)
          Visits the given method expression, self.
 void visitMinusExpression(JMinusExpression self)
          Visits the given minus expression, self.
 void visitModuloExpression(JModuloExpression self)
          Visits the given module expression, self.
 void visitMultExpression(JMultExpression self)
          Visits the given multiplication expression, self.
 void visitNameExpression(JNameExpression self)
          Visits the given local variable expression, self.
 void visitNewAnonymousClassExpression(JNewAnonymousClassExpression self)
          Visits the given new anonymous class expression, self.
 void visitNewArrayExpression(JNewArrayExpression self)
          Visits the given new array expression, self.
 void visitNewObjectExpression(JNewObjectExpression self)
          Visits the given new object expression, self.
 void visitParenthesedExpression(JParenthesedExpression self)
          Visits the given parenthesed expression, self.
 void visitPostfixExpression(JPostfixExpression self)
          Visits the given postfix expression, self.
 void visitPrefixExpression(JPrefixExpression self)
          Visits the given prefix expression, self.
 void visitRelationalExpression(JRelationalExpression self)
          Visits the given relational expression, self.
 void visitShiftExpression(JShiftExpression self)
          Visits the given shift expression, self.
 void visitSuperExpression(JSuperExpression self)
          Visits the given super expression, self.
 void visitThisExpression(JThisExpression self)
          Visits the given this expression, self.
 void visitTypeNameExpression(JTypeNameExpression self)
          Visits the given type name expression, self.
 void visitUnaryExpression(JUnaryExpression self)
          Visits the given unary expression, self.
 void visitUnaryPromoteExpression(JUnaryPromote self)
          Visits the given unary promition expression, self.
 
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
 

Constructor Detail

AbstractExpressionVisitor

public AbstractExpressionVisitor()
Method Detail

visitJmlPredicate

public void visitJmlPredicate(JmlPredicate self)
Visits the given RAC predicate, self. By default, this method visits the spec expression of self.

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

visitJmlSpecExpression

public void visitJmlSpecExpression(JmlSpecExpression self)
Visits the given JML spec expression, self. By default, this method visits the expression of self.

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

visitJmlNonNullElementsExpression

public void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
Visits the given non-null element expression, self. By default, this method visits the spec expression of self.

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

visitJmlDurationExpression

public void visitJmlDurationExpression(JmlDurationExpression self)
Visits the given \duration expression, self. By default, this method visits the spec expression of self.

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

visitJmlWorkingSpaceExpression

public void visitJmlWorkingSpaceExpression(JmlWorkingSpaceExpression self)
Visits the given \working_space expression, self. By default, this method visits the spec expression of self.

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

visitJmlSpaceExpression

public void visitJmlSpaceExpression(JmlSpaceExpression self)
Visits the given \space expression, self. By default, this method visits the spec expression of self.

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

visitJmlMaxExpression

public void visitJmlMaxExpression(JmlMaxExpression self)
Visits the given \max expression, self. By default, this method visits the spec expression of self.

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

visitJmlElemTypeExpression

public void visitJmlElemTypeExpression(JmlElemTypeExpression self)
Visits the given elem type expression, self. By default, this method visits the spec expression of self.

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

visitJmlFreshExpression

public void visitJmlFreshExpression(JmlFreshExpression self)
Visits the given fresh expression, self. By default, this method visits each spec expression contained in the expression self.

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

visitJmlInformalExpression

public void visitJmlInformalExpression(JmlInformalExpression self)
Visits the given informal description expression, self. By default, this method does no action at all.

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

visitJmlInvariantForExpression

public void visitJmlInvariantForExpression(JmlInvariantForExpression self)
Visits the given \invariant_for expression, self. By default, this method visits the spec expression of self.

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

visitJmlIsInitializedExpression

public void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
Visits the given \is_initialized expression, self. By default, this method does nothing.

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

visitJmlLabelExpression

public void visitJmlLabelExpression(JmlLabelExpression self)
Visits the given label expression, self. By default, this method visits the spec expression of self.

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

visitJmlLockSetExpression

public void visitJmlLockSetExpression(JmlLockSetExpression self)
Visits the given \lockset expression, self. By default, this method does nothing.

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

visitJmlPreExpression

public void visitJmlPreExpression(JmlPreExpression self)
Visits the given \pre expression, self. By default, this method visits the spec expression of self.

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

visitJmlOldExpression

public void visitJmlOldExpression(JmlOldExpression self)
Visits the given \old expression, self. By default, this method visits the spec expression of self.

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

visitJmlReachExpression

public void visitJmlReachExpression(JmlReachExpression self)
Visits the given \reach expression, self. By default, this method visits the store reference expression of self.

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

visitJmlResultExpression

public void visitJmlResultExpression(JmlResultExpression self)
Visits the given \result expression, self. By default, this method does nothing.

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

visitJmlSetComprehension

public void visitJmlSetComprehension(JmlSetComprehension self)
Visits the given set comprehension expression, self. By default, this method visits boeth predicate and superset predicate of self.

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

visitJmlSpecQuantifiedExpression

public void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
Visits the given spec quantified expression, self. By default, this method visits both predicate and spec expression of self.

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

visitJmlTypeExpression

public void visitJmlTypeExpression(JmlTypeExpression self)
Visits the given \type expression, self. By default, this method does nothing.

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

visitJmlTypeOfExpression

public void visitJmlTypeOfExpression(JmlTypeOfExpression self)
Visits the given \typeof expression, self. By default, this method visits the spec expression of self.

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

visitAssignmentExpression

public void visitAssignmentExpression(JAssignmentExpression self)
Visits the given assignment expression, self. By default, this method visits both the left and right side expression of self.

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

visitCompoundAssignmentExpression

public void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
Visits the given compound assignment expression, self. By default, this method visits both the left and right side expression of self.

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

visitConditionalExpression

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

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

visitJmlRelationalExpression

public void visitJmlRelationalExpression(JmlRelationalExpression self)
Visits the given JML relational expression, self. By default, this method visits both the left and right expressions of self.

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

visitConditionalAndExpression

public void visitConditionalAndExpression(JConditionalAndExpression self)
Visits the given conditional and expression, self. By default, this method visits both the left and right expressions of self.

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

visitConditionalOrExpression

public void visitConditionalOrExpression(JConditionalOrExpression self)
Visits the given condition or expression, self. By default, this method visits both the left and right expressions of self.

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

visitBitwiseExpression

public void visitBitwiseExpression(JBitwiseExpression self)
Visits the given bitwise expression, self. By default, this method visits both the left and right expressions of self.

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

visitEqualityExpression

public void visitEqualityExpression(JEqualityExpression self)
Visits the given equality expression, self. By default, this method visits both the left and right expressions of self.

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

visitRelationalExpression

public void visitRelationalExpression(JRelationalExpression self)
Visits the given relational expression, self. By default, this method visits both the left and right expressions of self.

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

visitInstanceofExpression

public void visitInstanceofExpression(JInstanceofExpression self)
Visits the given instanceof expression, self. By default, this method visits the expression of self.

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

visitAddExpression

public void visitAddExpression(JAddExpression self)
Visits the given addition expression, self. By default, this method visits both the left and right expressions of self.

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

visitMinusExpression

public void visitMinusExpression(JMinusExpression self)
Visits the given minus expression, self. By default, this method visits both the left and right expressions of self.

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

visitMultExpression

public void visitMultExpression(JMultExpression self)
Visits the given multiplication expression, self. By default, this method visits both the left and right expressions of self.

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

visitDivideExpression

public void visitDivideExpression(JDivideExpression self)
Visits the given division expression, self. By default, this method visits both the left and right expressions of self.

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

visitModuloExpression

public void visitModuloExpression(JModuloExpression self)
Visits the given module expression, self. By default, this method visits both the left and right expressions of self.

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

visitShiftExpression

public void visitShiftExpression(JShiftExpression self)
Visits the given shift expression, self. By default, this method visits both the left and right expressions of self.

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

visitPrefixExpression

public void visitPrefixExpression(JPrefixExpression self)
Visits the given prefix expression, self. By default, this method visits the expression of self.

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

visitPostfixExpression

public void visitPostfixExpression(JPostfixExpression self)
Visits the given postfix expression, self. By default, this method visits the expression of self.

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

visitUnaryExpression

public void visitUnaryExpression(JUnaryExpression self)
Visits the given unary expression, self. By default, this method visits the expression of self.

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

visitCastExpression

public void visitCastExpression(JCastExpression self)
Visits the given cast expression, self. By default, this method visits the expression of self.

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

visitUnaryPromoteExpression

public void visitUnaryPromoteExpression(JUnaryPromote self)
Visits the given unary promition expression, self. By default, this method visits the expression of of self.

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

visitMethodCallExpression

public void visitMethodCallExpression(JMethodCallExpression self)
Visits the given method expression, self. By default, this method visits both prefix and arguments of self.

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

visitTypeNameExpression

public void visitTypeNameExpression(JTypeNameExpression self)
Visits the given type name expression, self. By default, this method does nothing.

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

visitThisExpression

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

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

visitSuperExpression

public void visitSuperExpression(JSuperExpression self)
Visits the given super expression, self. By default, this method does nothing.

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

visitClassExpression

public void visitClassExpression(JClassExpression self)
Visits the given class expression, self. By default, this method does nothing.

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

visitExplicitConstructorInvocation

public void visitExplicitConstructorInvocation(JExplicitConstructorInvocation self)
Visits the given explicit constructor invocation, self. By default, this method visits bothe prefix and parameters of self.

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

visitArrayLengthExpression

public void visitArrayLengthExpression(JArrayLengthExpression self)
Visits the given array lenth expression, self. By default, this method visits the prefix of self.

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

visitArrayAccessExpression

public void visitArrayAccessExpression(JArrayAccessExpression self)
Visits the given array access expression, self. By default, this method visits bith prefix and accessor of self.

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

visitNameExpression

public void visitNameExpression(JNameExpression self)
Visits the given local variable expression, self. By default, this method does nothing.

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

visitLocalVariableExpression

public void visitLocalVariableExpression(JLocalVariableExpression self)
Visits the given local variable expression, self. By default, this method does nothing.

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

visitParenthesedExpression

public void visitParenthesedExpression(JParenthesedExpression self)
Visits the given parenthesed expression, self. By default, this method visits the expression of self.

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

visitNewObjectExpression

public void visitNewObjectExpression(JNewObjectExpression self)
Visits the given new object expression, self. By default, this method visits both the this expression and parameters of self.

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

visitNewAnonymousClassExpression

public void visitNewAnonymousClassExpression(JNewAnonymousClassExpression self)
Visits the given new anonymous class expression, self. By default, this method visits the declaration of self.

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

visitNewArrayExpression

public void visitNewArrayExpression(JNewArrayExpression self)
Visits the given new array expression, self. By default, this method visits both the dimension expression of self.

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

visitArrayDimsAndInit

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

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

visitArrayInitializer

public void visitArrayInitializer(JArrayInitializer self)
Visits the given array initializer, self. By default, this method visits each elements of self.

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

visitFieldExpression

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

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

visitExpressions

protected void visitExpressions(JExpression[] exprs)
Visits the given expressions, exprs.


visitBinaryExpression

protected void visitBinaryExpression(JBinaryExpression self)
Visits the binary expressions, exprs.


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.