JML

org.jmlspecs.racwrap
Class OrigPrettyPrinter

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.mjc.MjcPrettyPrinter
          extended byorg.jmlspecs.jmlrac.RacPrettyPrinter
              extended byorg.jmlspecs.racwrap.OrigPrettyPrinter
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor, RacConstants, RacVisitor

class OrigPrettyPrinter
extends RacPrettyPrinter


Field Summary
private  int classScopeLevel
           
 
Fields inherited from class org.jmlspecs.jmlrac.RacPrettyPrinter
NEW_LINE, offset
 
Fields inherited from class org.multijava.mjc.MjcPrettyPrinter
forInit, modUtil, nl, p, pos, TAB_SIZE, WIDTH
 
Fields inherited from class org.multijava.util.Utils
DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO
 
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
 
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
OrigPrettyPrinter(Writer wr, JmlModifier modUtil)
           
 
Method Summary
 void visitCompilationUnit(JCompilationUnit self)
          Same as MjcPrettyPrinter's visitCompilationUnit method, except it adds the imported runner package.
 void visitJmlClassDeclaration(JmlClassDeclaration self)
          Prints the modified class declaration of the orig file.
 void visitJmlConstructorDeclaration(JmlConstructorDeclaration self)
          Prints a JML constructor declaration.
 void visitJmlFieldDeclaration(JmlFieldDeclaration self)
          Prints the given JML field declaration.
 void visitJmlMethodDeclaration(JmlMethodDeclaration self)
          Prints a JML method declaration.
 
Methods inherited from class org.jmlspecs.jmlrac.RacPrettyPrinter
acceptAll, applyBinaryExpression, close, mayEndAnnotation, mayEndAnnotation, mayStartAnnotation, mayStartAnnotation, newLine, newLineOffset, print, print, printJml, println, toString, visitArrayAccessExpression, visitBigintLiteral, visitBinaryExpression, visitBitwiseExpression, visitCastExpression, visitCharLiteral, visitClassBody, visitCompoundAssignmentExpression, visitDoubleLiteral, visitEqualityExpression, visitExample, visitFieldExpression, visitFloatLiteral, visitFormalParameters, visitGeneralSpecCase, visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBehaviorSpec, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlElemTypeExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalBehaviorSpec, visitJmlExceptionalExample, visitJmlExceptionalSpecBody, visitJmlExceptionalSpecCase, visitJmlExpression, visitJmlExtendingSpecification, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlFreshExpression, visitJmlGeneralSpecCase, visitJmlGenericSpecBody, visitJmlGenericSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalExpression, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantForExpression, visitJmlInvariantStatement, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLetVarDecl, visitJmlLockSetExpression, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMaxExpression, visitJmlMeasuredClause, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNonNullElementsExpression, visitJmlNormalBehaviorSpec, visitJmlNormalExample, visitJmlNormalSpecBody, visitJmlNormalSpecCase, visitJmlNotAssignedExpression, visitJmlNotModifiedExpression, visitJmlOldExpression, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicate, visitJmlPredicateKeyword, visitJmlPreExpression, visitJmlReachExpression, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRelationalExpression, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlResultExpression, visitJmlReturnsClause, visitJmlSetComprehension, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecExpression, visitJmlSpecification, visitJmlSpecQuantifiedExpression, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlStoreRefListWrapper, visitJmlTypeExpression, visitJmlTypeOfExpression, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion, visitNewArrayExpression, visitNewObjectExpression, visitOrdinalLiteral, visitPostfixExpression, visitPrefixExpression, visitRacJmlMethodDeclaration, visitRacNode, visitRacPredicate, visitShiftExpression, visitSpecBody, visitSpecBodyClause, visitSpecCases, visitUnaryExpression, visitUnaryPromoteExpression, visitVariableDeclarationStatement
 
Methods inherited from class org.multijava.mjc.MjcPrettyPrinter
acceptAll, print, print, print, print, print, printClassModifiers, printInterfaceModifiers, setPos, visitAddExpression, visitArgs, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssertStatement, visitAssignmentExpression, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitByteLiteral, visitCatchClause, visitClassBlock, visitClassBody, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitComment, visitComments, visitCompoundStatement, visitCompoundStatement, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDivideExpression, visitDoStatement, visitEmptyStatement, visitExplicitConstructorInvocation, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceBody, visitInterfaceDeclaration, visitIntLiteral, visitJavadoc, visitLabeledStatement, visitLocalVariableExpression, visitLongLiteral, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNullLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitRealLiteral, visitRelationalExpression, visitReturnStatement, visitShortLiteral, visitStringLiteral, visitSuperExpression, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThisExpression, visitThrowStatement, visitTLMethodBody, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitTypeNameExpression, 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.multijava.mjc.MjcVisitor
visitAddExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssertStatement, visitAssignmentExpression, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitCatchClause, visitClassBlock, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitCompoundStatement, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDivideExpression, visitDoStatement, visitEmptyStatement, visitExplicitConstructorInvocation, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceDeclaration, visitLabeledStatement, visitLocalVariableExpression, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNullLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitRealLiteral, visitRelationalExpression, visitReturnStatement, visitStringLiteral, visitSuperExpression, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThisExpression, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitTypeNameExpression, visitVariableDefinition, visitWarnExpression, visitWhileStatement
 

Field Detail

classScopeLevel

private int classScopeLevel
Constructor Detail

OrigPrettyPrinter

public OrigPrettyPrinter(Writer wr,
                         JmlModifier modUtil)
Method Detail

visitCompilationUnit

public void visitCompilationUnit(JCompilationUnit self)
Same as MjcPrettyPrinter's visitCompilationUnit method, except it adds the imported runner package.

Specified by:
visitCompilationUnit in interface MjcVisitor
Overrides:
visitCompilationUnit in class RacPrettyPrinter

visitJmlClassDeclaration

public void visitJmlClassDeclaration(JmlClassDeclaration self)
Prints the modified class declaration of the orig file. This method prints $chx_Orig_Foo, instead of Foo as the class name. It will also extend $chx_Orig_Bar, instead of just Bar, except when the parent is Object, in which case it will extend org.jmlspecs.racwrap.runner.Wrapped instead.

Specified by:
visitJmlClassDeclaration in interface JmlVisitor
Overrides:
visitJmlClassDeclaration in class RacPrettyPrinter

visitJmlConstructorDeclaration

public void visitJmlConstructorDeclaration(JmlConstructorDeclaration self)
Description copied from class: RacPrettyPrinter
Prints a JML constructor declaration.

Specified by:
visitJmlConstructorDeclaration in interface JmlVisitor
Overrides:
visitJmlConstructorDeclaration in class RacPrettyPrinter

visitJmlMethodDeclaration

public void visitJmlMethodDeclaration(JmlMethodDeclaration self)
Description copied from class: RacPrettyPrinter
Prints a JML method declaration.

Specified by:
visitJmlMethodDeclaration in interface JmlVisitor
Overrides:
visitJmlMethodDeclaration in class RacPrettyPrinter

visitJmlFieldDeclaration

public void visitJmlFieldDeclaration(JmlFieldDeclaration self)
Description copied from class: RacPrettyPrinter
Prints the given JML field declaration. If this field declaration has a generated initialzer block (e.g., one for a ghost field), it is also printed.

Specified by:
visitJmlFieldDeclaration in interface JmlVisitor
Overrides:
visitJmlFieldDeclaration in class RacPrettyPrinter

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.