Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.checker
Class JmlAccumSubclassingInfo

java.lang.Object
  extended byorg.jmlspecs.checker.JmlVisitorNI
      extended byorg.jmlspecs.checker.JmlAccumSubclassingInfo
All Implemented Interfaces:
Constants, Constants, Constants, JmlVisitor, MjcVisitor
public class JmlAccumSubclassingInfo
extends JmlVisitorNI
implements Constants

Version:
$Revision: 1.12 $
Author:
not attributable

Field Summary
protected  ArrayList accessedFields
           
protected  ArrayList assignedFields
           
protected  ArrayList calledMethods
           
 
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
JmlAccumSubclassingInfo()
           
 
Method Summary
protected  void acceptAll(ArrayList all)
           
protected  void acceptAll(JPhylum[] all)
           
 JExpression[] getAccessedFields()
           
 JExpression[] getAssignedFields()
           
 JExpression[] getCalledMethods()
           
 void visitAddExpression(JAddExpression self)
          visits an add expression
protected  void visitArgs(JExpression[] args)
           
 void visitArrayAccessExpression(JArrayAccessExpression self)
          visits an array access expression
 void visitArrayDimsAndInit(JArrayDimsAndInits self)
          visits an array dimension and initialization expression
 void visitArrayInitializer(JArrayInitializer self)
          visits an array initializer expression
 void visitArrayLengthExpression(JArrayLengthExpression self)
          visits an array length expression
 void visitAssertStatement(JAssertStatement self)
          Visits the given assert statement.
 void visitAssignmentExpression(JAssignmentExpression self)
          visits an assignment expression
protected  void visitBinaryExpression(JBinaryExpression self, String oper)
           
 void visitBitwiseExpression(JBitwiseExpression self)
          visits a compound assignment expression
 void visitBlockStatement(JBlock self)
          visits an expression statement
 void visitBooleanLiteral(JBooleanLiteral self)
          visits a boolean literal
 void visitBreakStatement(JBreakStatement self)
          visits a break statement
 void visitCastExpression(JCastExpression self)
          visits a cast expression
 void visitCatchClause(JCatchClause self)
          visits a catch clause
 void visitCharLiteral(JCharLiteral self)
          visits a character literal
 void visitClassBlock(JClassBlock self)
          visits a class block (initializer)
protected  void visitClassBody(JmlTypeDeclaration self)
           
 void visitClassExpression(JClassExpression self)
          visits a class expression
 void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
          visits a compound expression
 void visitCompoundStatement(JCompoundStatement self)
          visits a compound statement
 void visitCompoundStatement(JStatement[] body)
           
 void visitConditionalAndExpression(JConditionalAndExpression self)
          visits a boolean AND expression
 void visitConditionalExpression(JConditionalExpression self)
          visits a conditional expression
 void visitConditionalOrExpression(JConditionalOrExpression self)
          visits a boolean OR expression
 void visitConstructorBlock(JConstructorBlock self)
          visits a constructor block
 void visitConstructorDeclaration(JConstructorDeclaration self)
          visits a constructor declaration
 void visitContinueStatement(JContinueStatement self)
          visits a continue statement
 void visitDivideExpression(JDivideExpression self)
          visits a divide expression
 void visitDoStatement(JDoStatement self)
          visits a do statement
 void visitEmptyStatement(JEmptyStatement self)
          visits a empty statement
 void visitEqualityExpression(JEqualityExpression self)
          visits an equality expression
 void visitExplicitConstructorInvocation(JExplicitConstructorInvocation self)
          visits an explicit constructor invocation
 void visitExpressionListStatement(JExpressionListStatement self)
          visits an expression list statement
 void visitExpressionStatement(JExpressionStatement self)
          visits an expression statement
 void visitFieldExpression(JClassFieldExpression self)
          visits a field expression
 void visitFormalParameters(JFormalParameter parm1)
          visits a formal parameter
 void visitForStatement(JForStatement self)
          visits a for statement
 void visitIfStatement(JIfStatement self)
          visits a if statement
 void visitInstanceofExpression(JInstanceofExpression self)
          visits an instanceof expression
 void visitJmlAbruptSpecBody(JmlAbruptSpecBody self)
           
 void visitJmlAbruptSpecCase(JmlAbruptSpecCase self)
           
 void visitJmlAssertStatement(JmlAssertStatement self)
           
 void visitJmlAssignableClause(JmlAssignableClause self)
           
 void visitJmlAssignmentStatement(JmlAssignmentStatement self)
           
 void visitJmlAssumeStatement(JmlAssumeStatement self)
           
 void visitJmlClassDeclaration(JmlClassDeclaration self)
           
 void visitJmlDebugStatement(JmlDebugStatement self)
           
 void visitJmlElemTypeExpression(JmlElemTypeExpression self)
           
 void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)
           
 void visitJmlExceptionalSpecCase(JmlExceptionalSpecCase self)
           
 void visitJmlFieldDeclaration(JmlFieldDeclaration self)
           
 void visitJmlGeneralSpecCase(JmlGeneralSpecCase self)
           
 void visitJmlGenericSpecBody(JmlGenericSpecBody self)
           
 void visitJmlGenericSpecCase(JmlGenericSpecCase self)
           
 void visitJmlGuardedStatement(JmlGuardedStatement self)
           
 void visitJmlHenceByStatement(JmlHenceByStatement self)
           
 void visitJmlLoopStatement(JmlLoopStatement self)
           
 void visitJmlMethodDeclaration(JmlMethodDeclaration self)
           
 void visitJmlNondetChoiceStatement(JmlNondetChoiceStatement self)
           
 void visitJmlNondetIfStatement(JmlNondetIfStatement self)
           
 void visitJmlNormalSpecBody(JmlNormalSpecBody self)
           
 void visitJmlNormalSpecCase(JmlNormalSpecCase self)
           
 void visitJmlPredicate(JmlPredicate self)
           
 void visitJmlPredicateKeyword(JmlPredicateKeyword self)
           
 void visitJmlRelationalExpression(JmlRelationalExpression self)
           
 void visitJmlSetStatement(JmlSetStatement self)
           
 void visitJmlSpecBody(JmlSpecBody self)
           
 void visitJmlSpecExpression(JmlSpecExpression self)
           
 void visitJmlSpecStatement(JmlSpecStatement self)
           
 void visitJmlTypeExpression(JmlTypeExpression self)
           
 void visitJmlTypeOfExpression(JmlTypeOfExpression self)
           
 void visitJmlUnreachableStatement(JmlUnreachableStatement self)
           
 void visitJmlVariableDefinition(JmlVariableDefinition self)
           
 void visitLabeledStatement(JLabeledStatement self)
          visits a labeled statement
 void visitLocalVariableExpression(JLocalVariableExpression self)
          visits a local variable expression
 void visitMathModeExpression(MJMathModeExpression self)
          visits a math mode expression
 void visitMethodCallExpression(JMethodCallExpression self)
          visits a method call expression
 void visitMethodDeclaration(JMethodDeclaration self)
          visits a method declaration
 void visitMinusExpression(JMinusExpression self)
          visits a minus expression
 void visitModuloExpression(JModuloExpression self)
          visits a modulo division expression
 void visitMultExpression(JMultExpression self)
          visits a multiplication expression
 void visitNameExpression(JNameExpression self)
          visits a name expression
 void visitNewAnonymousClassExpression(JNewAnonymousClassExpression self)
          visits an object allocator expression for an anonymous class
 void visitNewArrayExpression(JNewArrayExpression self)
          visits an array allocator expression
 void visitNewObjectExpression(JNewObjectExpression self)
          visits an object allocator expression
 void visitNullLiteral(JNullLiteral self)
          visits a null literal
 void visitOrdinalLiteral(JOrdinalLiteral self)
          prints an ordinal literal
 void visitParenthesedExpression(JParenthesedExpression self)
          visits a parenthesed expression
 void visitPostfixExpression(JPostfixExpression self)
          visits a postfix expression
 void visitPrefixExpression(JPrefixExpression self)
          visits a prefix expression
 void visitRealLiteral(JRealLiteral self)
          prints a real literal
 void visitRelationalExpression(JRelationalExpression self)
          visits a shift expressiona
 void visitReturnStatement(JReturnStatement self)
          visits a return statement
 void visitShiftExpression(JShiftExpression self)
          visits a shift expression
 void visitStringLiteral(JStringLiteral self)
          visits a string literal
 void visitSuperExpression(JSuperExpression self)
          visits a super expression
 void visitSwitchGroup(JSwitchGroup self)
          visits a switch group
 void visitSwitchLabel(JSwitchLabel self)
          visits a switch label
 void visitSwitchStatement(JSwitchStatement self)
          visits a switch statement
 void visitSynchronizedStatement(JSynchronizedStatement self)
          visits a synchronized statement
 void visitThisExpression(JThisExpression self)
          visits a this expression
 void visitThrowStatement(JThrowStatement self)
          visits a throw statement
 void visitTLMethodBody(JBlock body)
           
 void visitTopLevelMethodDeclaration(MJTopLevelMethodDeclaration self)
          visits an external method declaration
 void visitTryCatchStatement(JTryCatchStatement self)
          visits a try-catch statement
 void visitTryFinallyStatement(JTryFinallyStatement self)
          visits a try-finally statement
 void visitTypeDeclarationStatement(JTypeDeclarationStatement self)
          visits a type declaration statement
 void visitTypeNameExpression(JTypeNameExpression self)
          visits a type name expression
 void visitUnaryExpression(JUnaryExpression self)
          visits an unary expression
 void visitUnaryPromoteExpression(JUnaryPromote self)
          visits a cast expression
 void visitVariableDeclarationStatement(JVariableDeclarationStatement self)
          visits a variable declaration statement
 void visitVariableDefinition(JVariableDefinition self)
          visits a variable declaration statement
 void visitWhileStatement(JWhileStatement self)
          visits a while statement
 
Methods inherited from class org.jmlspecs.checker.JmlVisitorNI
imp, visitClassDeclaration, visitClassOrGFImport, visitCompilationUnit, visitFieldDeclaration, visitGenericFunctionDecl, visitInitializerDeclaration, visitInterfaceDeclaration, visitJmlAccessibleClause, visitJmlAxiom, visitJmlBehaviorSpec, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalBehaviorSpec, visitJmlExceptionalExample, visitJmlExpression, visitJmlExtendingSpecification, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlFreshExpression, visitJmlInformalExpression, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantForExpression, visitJmlInvariantStatement, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLetVarDecl, visitJmlLockSetExpression, visitJmlLoopInvariant, visitJmlMapsIntoClause, visitJmlMaxExpression, visitJmlMeasuredClause, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNonNullElementsExpression, visitJmlNormalBehaviorSpec, visitJmlNormalExample, visitJmlNotAssignedExpression, visitJmlNotModifiedExpression, visitJmlOldExpression, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPreExpression, visitJmlReachExpression, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlResultExpression, visitJmlReturnsClause, visitJmlSetComprehension, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecification, visitJmlSpecQuantifiedExpression, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion, visitPackageImport, visitPackageName, visitWarnExpression
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

assignedFields

protected ArrayList assignedFields

accessedFields

protected ArrayList accessedFields

calledMethods

protected ArrayList calledMethods
Constructor Detail

JmlAccumSubclassingInfo

public JmlAccumSubclassingInfo()
Method Detail

getAssignedFields

public JExpression[] getAssignedFields()

getAccessedFields

public JExpression[] getAccessedFields()

getCalledMethods

public JExpression[] getCalledMethods()

visitMethodDeclaration

public void visitMethodDeclaration(JMethodDeclaration self)
Description copied from class: JmlVisitorNI
visits a method declaration

Specified by:
visitMethodDeclaration in interface MjcVisitor
Overrides:
visitMethodDeclaration in class JmlVisitorNI

visitConstructorDeclaration

public void visitConstructorDeclaration(JConstructorDeclaration self)
Description copied from class: JmlVisitorNI
visits a constructor declaration

Specified by:
visitConstructorDeclaration in interface MjcVisitor
Overrides:
visitConstructorDeclaration in class JmlVisitorNI

visitBlockStatement

public void visitBlockStatement(JBlock self)
Description copied from class: JmlVisitorNI
visits an expression statement

Specified by:
visitBlockStatement in interface MjcVisitor
Overrides:
visitBlockStatement in class JmlVisitorNI

visitConstructorBlock

public void visitConstructorBlock(JConstructorBlock self)
Description copied from class: JmlVisitorNI
visits a constructor block

Specified by:
visitConstructorBlock in interface MjcVisitor
Overrides:
visitConstructorBlock in class JmlVisitorNI

visitCompoundStatement

public void visitCompoundStatement(JStatement[] body)

visitCompoundStatement

public void visitCompoundStatement(JCompoundStatement self)
Description copied from class: JmlVisitorNI
visits a compound statement

Specified by:
visitCompoundStatement in interface MjcVisitor
Overrides:
visitCompoundStatement in class JmlVisitorNI

visitVariableDeclarationStatement

public void visitVariableDeclarationStatement(JVariableDeclarationStatement self)
Description copied from class: JmlVisitorNI
visits a variable declaration statement

Specified by:
visitVariableDeclarationStatement in interface MjcVisitor
Overrides:
visitVariableDeclarationStatement in class JmlVisitorNI

visitVariableDefinition

public void visitVariableDefinition(JVariableDefinition self)
Description copied from class: JmlVisitorNI
visits a variable declaration statement

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

visitJmlVariableDefinition

public void visitJmlVariableDefinition(JmlVariableDefinition self)
Specified by:
visitJmlVariableDefinition in interface JmlVisitor
Overrides:
visitJmlVariableDefinition in class JmlVisitorNI

visitAssertStatement

public void visitAssertStatement(JAssertStatement self)
Description copied from class: JmlVisitorNI
Visits the given assert statement.

Specified by:
visitAssertStatement in interface MjcVisitor
Overrides:
visitAssertStatement in class JmlVisitorNI

visitBreakStatement

public void visitBreakStatement(JBreakStatement self)
Description copied from class: JmlVisitorNI
visits a break statement

Specified by:
visitBreakStatement in interface MjcVisitor
Overrides:
visitBreakStatement in class JmlVisitorNI

visitContinueStatement

public void visitContinueStatement(JContinueStatement self)
Description copied from class: JmlVisitorNI
visits a continue statement

Specified by:
visitContinueStatement in interface MjcVisitor
Overrides:
visitContinueStatement in class JmlVisitorNI

visitEmptyStatement

public void visitEmptyStatement(JEmptyStatement self)
Description copied from class: JmlVisitorNI
visits a empty statement

Specified by:
visitEmptyStatement in interface MjcVisitor
Overrides:
visitEmptyStatement in class JmlVisitorNI

visitExpressionListStatement

public void visitExpressionListStatement(JExpressionListStatement self)
Description copied from class: JmlVisitorNI
visits an expression list statement

Specified by:
visitExpressionListStatement in interface MjcVisitor
Overrides:
visitExpressionListStatement in class JmlVisitorNI

visitExpressionStatement

public void visitExpressionStatement(JExpressionStatement self)
Description copied from class: JmlVisitorNI
visits an expression statement

Specified by:
visitExpressionStatement in interface MjcVisitor
Overrides:
visitExpressionStatement in class JmlVisitorNI

visitIfStatement

public void visitIfStatement(JIfStatement self)
Description copied from class: JmlVisitorNI
visits a if statement

Specified by:
visitIfStatement in interface MjcVisitor
Overrides:
visitIfStatement in class JmlVisitorNI

visitDoStatement

public void visitDoStatement(JDoStatement self)
Description copied from class: JmlVisitorNI
visits a do statement

Specified by:
visitDoStatement in interface MjcVisitor
Overrides:
visitDoStatement in class JmlVisitorNI

visitWhileStatement

public void visitWhileStatement(JWhileStatement self)
Description copied from class: JmlVisitorNI
visits a while statement

Specified by:
visitWhileStatement in interface MjcVisitor
Overrides:
visitWhileStatement in class JmlVisitorNI

visitForStatement

public void visitForStatement(JForStatement self)
Description copied from class: JmlVisitorNI
visits a for statement

Specified by:
visitForStatement in interface MjcVisitor
Overrides:
visitForStatement in class JmlVisitorNI

visitSwitchStatement

public void visitSwitchStatement(JSwitchStatement self)
Description copied from class: JmlVisitorNI
visits a switch statement

Specified by:
visitSwitchStatement in interface MjcVisitor
Overrides:
visitSwitchStatement in class JmlVisitorNI

visitSwitchGroup

public void visitSwitchGroup(JSwitchGroup self)
Description copied from class: JmlVisitorNI
visits a switch group

Specified by:
visitSwitchGroup in interface MjcVisitor
Overrides:
visitSwitchGroup in class JmlVisitorNI

visitSwitchLabel

public void visitSwitchLabel(JSwitchLabel self)
Description copied from class: JmlVisitorNI
visits a switch label

Specified by:
visitSwitchLabel in interface MjcVisitor
Overrides:
visitSwitchLabel in class JmlVisitorNI

visitTryCatchStatement

public void visitTryCatchStatement(JTryCatchStatement self)
Description copied from class: JmlVisitorNI
visits a try-catch statement

Specified by:
visitTryCatchStatement in interface MjcVisitor
Overrides:
visitTryCatchStatement in class JmlVisitorNI

visitTryFinallyStatement

public void visitTryFinallyStatement(JTryFinallyStatement self)
Description copied from class: JmlVisitorNI
visits a try-finally statement

Specified by:
visitTryFinallyStatement in interface MjcVisitor
Overrides:
visitTryFinallyStatement in class JmlVisitorNI

visitSynchronizedStatement

public void visitSynchronizedStatement(JSynchronizedStatement self)
Description copied from class: JmlVisitorNI
visits a synchronized statement

Specified by:
visitSynchronizedStatement in interface MjcVisitor
Overrides:
visitSynchronizedStatement in class JmlVisitorNI

visitReturnStatement

public void visitReturnStatement(JReturnStatement self)
Description copied from class: JmlVisitorNI
visits a return statement

Specified by:
visitReturnStatement in interface MjcVisitor
Overrides:
visitReturnStatement in class JmlVisitorNI

visitThrowStatement

public void visitThrowStatement(JThrowStatement self)
Description copied from class: JmlVisitorNI
visits a throw statement

Specified by:
visitThrowStatement in interface MjcVisitor
Overrides:
visitThrowStatement in class JmlVisitorNI

visitLabeledStatement

public void visitLabeledStatement(JLabeledStatement self)
Description copied from class: JmlVisitorNI
visits a labeled statement

Specified by:
visitLabeledStatement in interface MjcVisitor
Overrides:
visitLabeledStatement in class JmlVisitorNI

visitExplicitConstructorInvocation

public void visitExplicitConstructorInvocation(JExplicitConstructorInvocation self)
Description copied from class: JmlVisitorNI
visits an explicit constructor invocation

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

visitMethodCallExpression

public void visitMethodCallExpression(JMethodCallExpression self)
Description copied from class: JmlVisitorNI
visits a method call expression

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

visitAddExpression

public void visitAddExpression(JAddExpression self)
Description copied from class: JmlVisitorNI
visits an add expression

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

visitConditionalAndExpression

public void visitConditionalAndExpression(JConditionalAndExpression self)
Description copied from class: JmlVisitorNI
visits a boolean AND expression

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

visitConditionalOrExpression

public void visitConditionalOrExpression(JConditionalOrExpression self)
Description copied from class: JmlVisitorNI
visits a boolean OR expression

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

visitDivideExpression

public void visitDivideExpression(JDivideExpression self)
Description copied from class: JmlVisitorNI
visits a divide expression

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

visitMinusExpression

public void visitMinusExpression(JMinusExpression self)
Description copied from class: JmlVisitorNI
visits a minus expression

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

visitModuloExpression

public void visitModuloExpression(JModuloExpression self)
Description copied from class: JmlVisitorNI
visits a modulo division expression

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

visitMultExpression

public void visitMultExpression(JMultExpression self)
Description copied from class: JmlVisitorNI
visits a multiplication expression

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

visitBinaryExpression

protected void visitBinaryExpression(JBinaryExpression self,
                                     String oper)

visitBitwiseExpression

public void visitBitwiseExpression(JBitwiseExpression self)
Description copied from class: JmlVisitorNI
visits a compound assignment expression

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

visitShiftExpression

public void visitShiftExpression(JShiftExpression self)
Description copied from class: JmlVisitorNI
visits a shift expression

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

visitAssignmentExpression

public void visitAssignmentExpression(JAssignmentExpression self)
Description copied from class: JmlVisitorNI
visits an assignment expression

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

visitCompoundAssignmentExpression

public void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
Description copied from class: JmlVisitorNI
visits a compound expression

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

visitPostfixExpression

public void visitPostfixExpression(JPostfixExpression self)
Description copied from class: JmlVisitorNI
visits a postfix expression

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

visitPrefixExpression

public void visitPrefixExpression(JPrefixExpression self)
Description copied from class: JmlVisitorNI
visits a prefix expression

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

visitLocalVariableExpression

public void visitLocalVariableExpression(JLocalVariableExpression self)
Description copied from class: JmlVisitorNI
visits a local variable expression

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

visitEqualityExpression

public void visitEqualityExpression(JEqualityExpression self)
Description copied from class: JmlVisitorNI
visits an equality expression

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

visitRelationalExpression

public void visitRelationalExpression(JRelationalExpression self)
Description copied from class: JmlVisitorNI
visits a shift expressiona

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

visitNameExpression

public void visitNameExpression(JNameExpression self)
Description copied from class: JmlVisitorNI
visits a name expression

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

visitParenthesedExpression

public void visitParenthesedExpression(JParenthesedExpression self)
Description copied from class: JmlVisitorNI
visits a parenthesed expression

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

visitCastExpression

public void visitCastExpression(JCastExpression self)
Description copied from class: JmlVisitorNI
visits a cast expression

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

visitNewObjectExpression

public void visitNewObjectExpression(JNewObjectExpression self)
Description copied from class: JmlVisitorNI
visits an object allocator expression

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

visitNewAnonymousClassExpression

public void visitNewAnonymousClassExpression(JNewAnonymousClassExpression self)
Description copied from class: JmlVisitorNI
visits an object allocator expression for an anonymous class

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

visitNewArrayExpression

public void visitNewArrayExpression(JNewArrayExpression self)
Description copied from class: JmlVisitorNI
visits an array allocator expression

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

visitArrayDimsAndInit

public void visitArrayDimsAndInit(JArrayDimsAndInits self)
Description copied from class: JmlVisitorNI
visits an array dimension and initialization expression

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

visitArrayInitializer

public void visitArrayInitializer(JArrayInitializer self)
Description copied from class: JmlVisitorNI
visits an array initializer expression

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

visitArrayAccessExpression

public void visitArrayAccessExpression(JArrayAccessExpression self)
Description copied from class: JmlVisitorNI
visits an array access expression

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

visitArrayLengthExpression

public void visitArrayLengthExpression(JArrayLengthExpression self)
Description copied from class: JmlVisitorNI
visits an array length expression

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

visitUnaryExpression

public void visitUnaryExpression(JUnaryExpression self)
Description copied from class: JmlVisitorNI
visits an unary expression

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

visitUnaryPromoteExpression

public void visitUnaryPromoteExpression(JUnaryPromote self)
Description copied from class: JmlVisitorNI
visits a cast expression

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

visitConditionalExpression

public void visitConditionalExpression(JConditionalExpression self)
Description copied from class: JmlVisitorNI
visits a conditional expression

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

visitInstanceofExpression

public void visitInstanceofExpression(JInstanceofExpression self)
Description copied from class: JmlVisitorNI
visits an instanceof expression

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

visitThisExpression

public void visitThisExpression(JThisExpression self)
Description copied from class: JmlVisitorNI
visits a this expression

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

visitSuperExpression

public void visitSuperExpression(JSuperExpression self)
Description copied from class: JmlVisitorNI
visits a super expression

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

visitTypeNameExpression

public void visitTypeNameExpression(JTypeNameExpression self)
Description copied from class: JmlVisitorNI
visits a type name expression

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

visitCatchClause

public void visitCatchClause(JCatchClause self)
Description copied from class: JmlVisitorNI
visits a catch clause

Specified by:
visitCatchClause in interface MjcVisitor
Overrides:
visitCatchClause in class JmlVisitorNI

visitStringLiteral

public void visitStringLiteral(JStringLiteral self)
Description copied from class: JmlVisitorNI
visits a string literal

Specified by:
visitStringLiteral in interface MjcVisitor
Overrides:
visitStringLiteral in class JmlVisitorNI

visitOrdinalLiteral

public void visitOrdinalLiteral(JOrdinalLiteral self)
Description copied from class: JmlVisitorNI
prints an ordinal literal

Specified by:
visitOrdinalLiteral in interface MjcVisitor
Overrides:
visitOrdinalLiteral in class JmlVisitorNI

visitNullLiteral

public void visitNullLiteral(JNullLiteral self)
Description copied from class: JmlVisitorNI
visits a null literal

Specified by:
visitNullLiteral in interface MjcVisitor
Overrides:
visitNullLiteral in class JmlVisitorNI

visitBooleanLiteral

public void visitBooleanLiteral(JBooleanLiteral self)
Description copied from class: JmlVisitorNI
visits a boolean literal

Specified by:
visitBooleanLiteral in interface MjcVisitor
Overrides:
visitBooleanLiteral in class JmlVisitorNI

visitCharLiteral

public void visitCharLiteral(JCharLiteral self)
Description copied from class: JmlVisitorNI
visits a character literal

Specified by:
visitCharLiteral in interface MjcVisitor
Overrides:
visitCharLiteral in class JmlVisitorNI

visitRealLiteral

public void visitRealLiteral(JRealLiteral self)
Description copied from class: JmlVisitorNI
prints a real literal

Specified by:
visitRealLiteral in interface MjcVisitor
Overrides:
visitRealLiteral in class JmlVisitorNI

visitTopLevelMethodDeclaration

public void visitTopLevelMethodDeclaration(MJTopLevelMethodDeclaration self)
Description copied from class: JmlVisitorNI
visits an external method declaration

Specified by:
visitTopLevelMethodDeclaration in interface MjcVisitor
Overrides:
visitTopLevelMethodDeclaration in class JmlVisitorNI

visitTLMethodBody

public void visitTLMethodBody(JBlock body)

visitClassBlock

public void visitClassBlock(JClassBlock self)
Description copied from class: JmlVisitorNI
visits a class block (initializer)

Specified by:
visitClassBlock in interface MjcVisitor
Overrides:
visitClassBlock in class JmlVisitorNI

visitTypeDeclarationStatement

public void visitTypeDeclarationStatement(JTypeDeclarationStatement self)
Description copied from class: JmlVisitorNI
visits a type declaration statement

Specified by:
visitTypeDeclarationStatement in interface MjcVisitor
Overrides:
visitTypeDeclarationStatement in class JmlVisitorNI

visitFieldExpression

public void visitFieldExpression(JClassFieldExpression self)
Description copied from class: JmlVisitorNI
visits a field expression

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

visitFormalParameters

public void visitFormalParameters(JFormalParameter parm1)
Description copied from class: JmlVisitorNI
visits a formal parameter

Specified by:
visitFormalParameters in interface MjcVisitor
Overrides:
visitFormalParameters in class JmlVisitorNI

visitClassExpression

public void visitClassExpression(JClassExpression self)
Description copied from class: JmlVisitorNI
visits a class expression

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

acceptAll

protected void acceptAll(ArrayList all)

visitArgs

protected void visitArgs(JExpression[] args)

visitJmlLoopStatement

public void visitJmlLoopStatement(JmlLoopStatement self)
Specified by:
visitJmlLoopStatement in interface JmlVisitor
Overrides:
visitJmlLoopStatement in class JmlVisitorNI

visitJmlAssignmentStatement

public void visitJmlAssignmentStatement(JmlAssignmentStatement self)
Specified by:
visitJmlAssignmentStatement in interface JmlVisitor
Overrides:
visitJmlAssignmentStatement in class JmlVisitorNI

visitJmlNondetChoiceStatement

public void visitJmlNondetChoiceStatement(JmlNondetChoiceStatement self)
Specified by:
visitJmlNondetChoiceStatement in interface JmlVisitor
Overrides:
visitJmlNondetChoiceStatement in class JmlVisitorNI

visitJmlNondetIfStatement

public void visitJmlNondetIfStatement(JmlNondetIfStatement self)
Specified by:
visitJmlNondetIfStatement in interface JmlVisitor
Overrides:
visitJmlNondetIfStatement in class JmlVisitorNI

visitJmlGuardedStatement

public void visitJmlGuardedStatement(JmlGuardedStatement self)
Specified by:
visitJmlGuardedStatement in interface JmlVisitor
Overrides:
visitJmlGuardedStatement in class JmlVisitorNI

visitJmlRelationalExpression

public void visitJmlRelationalExpression(JmlRelationalExpression self)
Specified by:
visitJmlRelationalExpression in interface JmlVisitor
Overrides:
visitJmlRelationalExpression in class JmlVisitorNI

visitJmlAssumeStatement

public void visitJmlAssumeStatement(JmlAssumeStatement self)
Specified by:
visitJmlAssumeStatement in interface JmlVisitor
Overrides:
visitJmlAssumeStatement in class JmlVisitorNI

visitJmlAssertStatement

public void visitJmlAssertStatement(JmlAssertStatement self)
Specified by:
visitJmlAssertStatement in interface JmlVisitor
Overrides:
visitJmlAssertStatement in class JmlVisitorNI

visitJmlElemTypeExpression

public void visitJmlElemTypeExpression(JmlElemTypeExpression self)
Specified by:
visitJmlElemTypeExpression in interface JmlVisitor
Overrides:
visitJmlElemTypeExpression in class JmlVisitorNI

visitJmlSpecStatement

public void visitJmlSpecStatement(JmlSpecStatement self)
Specified by:
visitJmlSpecStatement in interface JmlVisitor
Overrides:
visitJmlSpecStatement in class JmlVisitorNI

visitJmlGeneralSpecCase

public void visitJmlGeneralSpecCase(JmlGeneralSpecCase self)
Specified by:
visitJmlGeneralSpecCase in interface JmlVisitor
Overrides:
visitJmlGeneralSpecCase in class JmlVisitorNI

visitJmlGenericSpecCase

public void visitJmlGenericSpecCase(JmlGenericSpecCase self)
Specified by:
visitJmlGenericSpecCase in interface JmlVisitor
Overrides:
visitJmlGenericSpecCase in class JmlVisitorNI

visitJmlNormalSpecCase

public void visitJmlNormalSpecCase(JmlNormalSpecCase self)
Specified by:
visitJmlNormalSpecCase in interface JmlVisitor
Overrides:
visitJmlNormalSpecCase in class JmlVisitorNI

visitJmlExceptionalSpecCase

public void visitJmlExceptionalSpecCase(JmlExceptionalSpecCase self)
Specified by:
visitJmlExceptionalSpecCase in interface JmlVisitor
Overrides:
visitJmlExceptionalSpecCase in class JmlVisitorNI

visitJmlAbruptSpecCase

public void visitJmlAbruptSpecCase(JmlAbruptSpecCase self)
Specified by:
visitJmlAbruptSpecCase in interface JmlVisitor
Overrides:
visitJmlAbruptSpecCase in class JmlVisitorNI

visitJmlSpecBody

public void visitJmlSpecBody(JmlSpecBody self)
Specified by:
visitJmlSpecBody in interface JmlVisitor
Overrides:
visitJmlSpecBody in class JmlVisitorNI

visitJmlGenericSpecBody

public void visitJmlGenericSpecBody(JmlGenericSpecBody self)
Specified by:
visitJmlGenericSpecBody in interface JmlVisitor
Overrides:
visitJmlGenericSpecBody in class JmlVisitorNI

visitJmlNormalSpecBody

public void visitJmlNormalSpecBody(JmlNormalSpecBody self)
Specified by:
visitJmlNormalSpecBody in interface JmlVisitor
Overrides:
visitJmlNormalSpecBody in class JmlVisitorNI

visitJmlExceptionalSpecBody

public void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)
Specified by:
visitJmlExceptionalSpecBody in interface JmlVisitor
Overrides:
visitJmlExceptionalSpecBody in class JmlVisitorNI

visitJmlAbruptSpecBody

public void visitJmlAbruptSpecBody(JmlAbruptSpecBody self)
Specified by:
visitJmlAbruptSpecBody in interface JmlVisitor
Overrides:
visitJmlAbruptSpecBody in class JmlVisitorNI

visitJmlAssignableClause

public void visitJmlAssignableClause(JmlAssignableClause self)
Specified by:
visitJmlAssignableClause in interface JmlVisitor
Overrides:
visitJmlAssignableClause in class JmlVisitorNI

visitJmlDebugStatement

public void visitJmlDebugStatement(JmlDebugStatement self)
Specified by:
visitJmlDebugStatement in interface JmlVisitor
Overrides:
visitJmlDebugStatement in class JmlVisitorNI

visitJmlSetStatement

public void visitJmlSetStatement(JmlSetStatement self)
Specified by:
visitJmlSetStatement in interface JmlVisitor
Overrides:
visitJmlSetStatement in class JmlVisitorNI

visitJmlUnreachableStatement

public void visitJmlUnreachableStatement(JmlUnreachableStatement self)
Specified by:
visitJmlUnreachableStatement in interface JmlVisitor
Overrides:
visitJmlUnreachableStatement in class JmlVisitorNI

visitJmlHenceByStatement

public void visitJmlHenceByStatement(JmlHenceByStatement self)
Specified by:
visitJmlHenceByStatement in interface JmlVisitor
Overrides:
visitJmlHenceByStatement in class JmlVisitorNI

visitJmlTypeExpression

public void visitJmlTypeExpression(JmlTypeExpression self)
Specified by:
visitJmlTypeExpression in interface JmlVisitor
Overrides:
visitJmlTypeExpression in class JmlVisitorNI

visitMathModeExpression

public void visitMathModeExpression(MJMathModeExpression self)
Description copied from class: JmlVisitorNI
visits a math mode expression

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

visitJmlClassDeclaration

public void visitJmlClassDeclaration(JmlClassDeclaration self)
Specified by:
visitJmlClassDeclaration in interface JmlVisitor
Overrides:
visitJmlClassDeclaration in class JmlVisitorNI

visitJmlTypeOfExpression

public void visitJmlTypeOfExpression(JmlTypeOfExpression self)
Specified by:
visitJmlTypeOfExpression in interface JmlVisitor
Overrides:
visitJmlTypeOfExpression in class JmlVisitorNI

visitJmlSpecExpression

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

visitJmlPredicate

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

visitJmlPredicateKeyword

public void visitJmlPredicateKeyword(JmlPredicateKeyword self)
Specified by:
visitJmlPredicateKeyword in interface JmlVisitor
Overrides:
visitJmlPredicateKeyword in class JmlVisitorNI

visitJmlMethodDeclaration

public void visitJmlMethodDeclaration(JmlMethodDeclaration self)
Specified by:
visitJmlMethodDeclaration in interface JmlVisitor
Overrides:
visitJmlMethodDeclaration in class JmlVisitorNI

visitJmlFieldDeclaration

public void visitJmlFieldDeclaration(JmlFieldDeclaration self)
Specified by:
visitJmlFieldDeclaration in interface JmlVisitor
Overrides:
visitJmlFieldDeclaration in class JmlVisitorNI

visitClassBody

protected void visitClassBody(JmlTypeDeclaration self)

acceptAll

protected void acceptAll(JPhylum[] all)
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
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.