JML

org.jmlspecs.jmlrac
Class TransMethodBody

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.checker.JmlAbstractVisitor
          extended byorg.jmlspecs.jmlrac.RacAbstractVisitor
              extended byorg.jmlspecs.jmlrac.TransMethodBody
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor, RacConstants, RacVisitor
Direct Known Subclasses:
TransConstructorBody

public class TransMethodBody
extends RacAbstractVisitor

A visitor class for translating JML specification statements in a method body into assertion check code. The translated assertion check code is stored as a RacNode in the AST of the specification statement and is expected to be pretty-printed by the class RacPrettyPrinter. Translated are such specification statements as assume, assert, and unreachable statements.

                 TransConstuctorBody  JConstructorBlock
                         |                   |
                         +                   +
                         v                   V
 TransType <>----- TransMethodBody -----> JBlock
                         |                   |
       setAssertionCode()|<<call>>           +
                         V                   V
                 JmlAssertStatement ----|> JStatement
                         ^
          assertionCode()|<<call>>
                         |
                 RacPrettyPrinter
 

Version:
$Revision: 1.52 $
Author:
Yoonsik Cheon
See Also:
translate(), visitJmlAssumeStatement(JmlAssumeStatement), visitJmlAssertStatement(JmlAssertStatement), visitCompoundStatement(JStatement[]), visitJmlUnreachableStatement(JmlUnreachableStatement)

Field Summary
protected  JBlock body
          method body to be translated
protected  JmlMethodDeclaration methodDecl
          method declaration whose body is being translated
protected  JTypeDeclarationType typeDecl
          type declaration to which the method belongs
protected  VarGenerator varGen
          variable generator to generate fresh local variables
 
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
TransMethodBody(VarGenerator varGen, JmlMethodDeclaration mdecl, JTypeDeclarationType typeDecl)
          Construct an object of TransMethodBody.
 
Method Summary
private  JExpression conjoinInvariants(JmlLoopInvariant[] invs)
          Conjoins the given loop invariants and returns the result.
static String defaultValue(CType type)
          Return the default value of the type type.
static RacNode getGhostFieldSetter(JClassFieldExpression fieldExpr, String argVar, VarGenerator varGen)
          Returns Java source code that makes a dynamic call to the setter method of the given ghost field, fieldExpr, to set the ghost value to the value of the given variable, argVar.
private  RacNode ghostFieldSetter(JClassFieldExpression fieldExpr, String argVar)
          Returns Java source code that makes a dynamic call to the setter method of the given ghost field, fieldExpr, to set the ghost value to the value of the given variable, argVar.
private  RacNode invariantCheckCode(JmlLoopInvariant[] invs)
          Returns code that checks the given loop invariants.
protected  String isActive()
          Returns a string representation of the condition that tests if the given type of assertion is active.
private static boolean isCheckable(JmlAssertOrAssumeStatement clause)
          Returns true if the given assume (or assert) statement is checkable.
private static boolean isCheckable(JmlHenceByStatement clause)
          Returns true if the given hence_by statement is checkable.
private static boolean isCheckable(JmlLoopSpecification clause)
          Returns true if the given loop invariant is checkable.
private static boolean isStatic(JClassFieldExpression expr)
          Returns true if the given field expression is a reference to a static field.
private static void needDynamicInvocationMethod()
          Records that a ghost field inheritance mechanism is needed.
static String operator(JAssignmentExpression expr)
          Returns the string representation of the assignment operator of the given assignment expression.
private  void transDoLoop(JmlLoopStatement self, RacNode checkInv, RacNode checkVar)
          Translates the given JML loop statement with the given invariant check code and variant check code.
private  void transForLoop(JmlLoopStatement self, RacNode checkInv, RacNode checkVar)
          Translates the given JML loop statement with the given invariant check code and variant check code.
 JBlock translate()
          Performs the translation of method body and returns the resulting method body, which may be modified during the translation.
private static RacNode transPrefix(VarGenerator varGen, JClassFieldExpression fieldExpr)
          Translates the prefix expression of the given field reference expression, fieldExpr.
private  void transWhileLoop(JmlLoopStatement self, RacNode checkInv, RacNode checkVar)
          Translates the given JML loop statement with the given invariant check code and variant check code.
private  RacNode variantCheckCode(JmlVariantFunction[] vars)
          Returns code that checks the given loop variants.
 void visitAssertStatement(JAssertStatement self)
          Translates the given Java assert statement.
 void visitBlockStatement(JBlock self)
          Translates the given Java block statement.
 void visitBreakStatement(JBreakStatement self)
          Translates the given Java break statement.
 void visitCompoundStatement(JCompoundStatement self)
          Translates the given Java compound statement.
 void visitCompoundStatement(JStatement[] body)
          Translates the given Java compound statement.
 void visitConstructorBlock(JConstructorBlock self)
          Translates the given Java constructor statement.
 void visitContinueStatement(JContinueStatement self)
          Translates the given Java continue statement.
 void visitDoStatement(JDoStatement self)
          Translates the given Java do statement.
 void visitEmptyStatement(JEmptyStatement self)
          Translates the given Java empty statement.
 void visitExpressionListStatement(JExpressionListStatement self)
          Translates the given Java expression list statement.
 void visitExpressionStatement(JExpressionStatement self)
          Translates the given Java expression statement.
 void visitForStatement(JForStatement self)
          Translates the given Java for statement.
 void visitIfStatement(JIfStatement self)
          Translates the given Java if statement.
 void visitJmlAssertStatement(JmlAssertStatement self)
          Translates the given JML assert statement and stores the translated assertion check code into the AST node.
 void visitJmlAssumeStatement(JmlAssumeStatement self)
          Translates the JML assume statement and stores the translated assertion check code into the AST node.
 void visitJmlDebugStatement(JmlDebugStatement self)
          Translates the given JML debug statement and stores the translated code into the AST node.
 void visitJmlGuardedStatement(JmlGuardedStatement self)
          Translates the given JML guarded statement.
 void visitJmlHenceByStatement(JmlHenceByStatement self)
          Translates the given JML hence_by and stores the translated assertion check code into the AST node.
 void visitJmlInvariantStatement(JmlInvariantStatement self)
          Translates the given JML invariant statement.
 void visitJmlLoopStatement(JmlLoopStatement self)
          Translates the given JML loop statement and stores the instrumented code into the AST node of self.
 void visitJmlNondetChoiceStatement(JmlNondetChoiceStatement self)
          Translates the given JML nondeterministic choice statement.
 void visitJmlNondetIfStatement(JmlNondetIfStatement self)
          Translates the given JML nondeterministic if statement.
 void visitJmlSetStatement(JmlSetStatement self)
          Translates the JML set statement and stores the translated assertion check code into the AST node.
 void visitJmlSpecStatement(JmlSpecStatement self)
          Translates the given JML specification statement.
 void visitJmlUnreachableStatement(JmlUnreachableStatement self)
          Translates the JML unreachable statement.
 void visitLabeledStatement(JLabeledStatement self)
          Translates the given Java labeled statement.
 void visitReturnStatement(JReturnStatement self)
          Translates the given Java return statement.
 void visitSwitchGroup(JSwitchGroup self)
          Translates the given Java switch group statement.
 void visitSwitchStatement(JSwitchStatement self)
          Translates the given Java switch statement.
 void visitSynchronizedStatement(JSynchronizedStatement self)
          Translates the given Java synchronized statement.
 void visitThrowStatement(JThrowStatement self)
          Translates the given Java throw statement.
 void visitTryCatchStatement(JTryCatchStatement self)
          Translates the given Java try/catch statement.
 void visitTryFinallyStatement(JTryFinallyStatement self)
          Translates the given Java try/finally statement.
 void visitTypeDeclarationStatement(JTypeDeclarationStatement self)
          Translates the given Java type declaration statement.
 void visitVariableDeclarationStatement(JVariableDeclarationStatement self)
          Translates the given Java variable declaration statement.
 void visitWhileStatement(JWhileStatement self)
          Translates the given Java while statement.
 
Methods inherited from class org.jmlspecs.jmlrac.RacAbstractVisitor
visitRacNode, visitRacPredicate
 
Methods inherited from class org.jmlspecs.checker.JmlAbstractVisitor
visitAddExpression, visitArrayAccessExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssignmentExpression, visitBinaryExpression, visitBitwiseExpression, visitBooleanLiteral, visitByteLiteral, visitCastExpression, visitCatchClause, visitCharLiteral, visitClassBlock, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorDeclaration, visitDivideExpression, visitDoubleLiteral, visitEqualityExpression, visitExplicitConstructorInvocation, visitFieldDeclaration, visitFieldExpression, visitFloatLiteral, visitFormalParameters, visitGenericFunctionDecl, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceDeclaration, visitIntLiteral, visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAxiom, visitJmlBehaviorSpec, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlElemTypeExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalBehaviorSpec, visitJmlExceptionalExample, visitJmlExceptionalSpecBody, visitJmlExceptionalSpecCase, visitJmlExpression, visitJmlExtendingSpecification, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlFreshExpression, visitJmlGeneralSpecCase, visitJmlGenericSpecBody, visitJmlGenericSpecCase, visitJmlInformalExpression, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantForExpression, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLetVarDecl, visitJmlLockSetExpression, visitJmlLoopInvariant, visitJmlMapsIntoClause, visitJmlMaxExpression, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, 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, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecExpression, visitJmlSpecification, visitJmlSpecQuantifiedExpression, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlTypeExpression, visitJmlTypeOfExpression, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion, visitLocalVariableExpression, visitLongLiteral, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitNewObjectExpression, visitNullLiteral, visitOrdinalLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitPostfixExpression, visitPrefixExpression, visitRealLiteral, visitRelationalExpression, visitShiftExpression, visitShortLiteral, visitStringLiteral, visitSuperExpression, visitSwitchLabel, visitThisExpression, visitTopLevelMethodDeclaration, visitTypeNameExpression, visitUnaryExpression, visitUnaryPromoteExpression, visitVariableDefinition, visitWarnExpression
 
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, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAxiom, visitJmlBehaviorSpec, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlElemTypeExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalBehaviorSpec, visitJmlExceptionalExample, visitJmlExceptionalSpecBody, visitJmlExceptionalSpecCase, visitJmlExpression, visitJmlExtendingSpecification, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlFreshExpression, visitJmlGeneralSpecCase, visitJmlGenericSpecBody, visitJmlGenericSpecCase, visitJmlInformalExpression, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantForExpression, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLetVarDecl, visitJmlLockSetExpression, visitJmlLoopInvariant, visitJmlMapsIntoClause, visitJmlMaxExpression, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, 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, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecExpression, visitJmlSpecification, visitJmlSpecQuantifiedExpression, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlTypeExpression, visitJmlTypeOfExpression, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion
 
Methods inherited from interface org.multijava.mjc.MjcVisitor
visitAddExpression, visitArrayAccessExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssignmentExpression, visitBitwiseExpression, visitBooleanLiteral, visitCastExpression, visitCatchClause, visitCharLiteral, visitClassBlock, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorDeclaration, visitDivideExpression, visitEqualityExpression, visitExplicitConstructorInvocation, visitFieldDeclaration, visitFieldExpression, visitFormalParameters, visitGenericFunctionDecl, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceDeclaration, visitLocalVariableExpression, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitNewObjectExpression, visitNullLiteral, visitOrdinalLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitPostfixExpression, visitPrefixExpression, visitRealLiteral, visitRelationalExpression, visitShiftExpression, visitStringLiteral, visitSuperExpression, visitSwitchLabel, visitThisExpression, visitTopLevelMethodDeclaration, visitTypeNameExpression, visitUnaryExpression, visitUnaryPromoteExpression, visitVariableDefinition, visitWarnExpression
 

Field Detail

varGen

protected VarGenerator varGen
variable generator to generate fresh local variables


typeDecl

protected JTypeDeclarationType typeDecl
type declaration to which the method belongs


methodDecl

protected JmlMethodDeclaration methodDecl
method declaration whose body is being translated


body

protected JBlock body
method body to be translated

Constructor Detail

TransMethodBody

public TransMethodBody(VarGenerator varGen,
                       JmlMethodDeclaration mdecl,
                       JTypeDeclarationType typeDecl)
Construct an object of TransMethodBody.

Parameters:
varGen - variable name generator
mdecl - method body to be translated
Method Detail

translate

public JBlock translate()
Performs the translation of method body and returns the resulting method body, which may be modified during the translation. For specification statements such as assume, assert, and unreachable, the translation produces their assertion check code (of type RacNode) and stores them into their ASTs.

  ensures \result != null;
 

See Also:
visitJmlAssumeStatement(JmlAssumeStatement), visitJmlAssertStatement(JmlAssertStatement), visitCompoundStatement(JStatement[]), visitJmlUnreachableStatement(JmlUnreachableStatement)

visitJmlAssertStatement

public void visitJmlAssertStatement(JmlAssertStatement self)
Translates the given JML assert statement and stores the translated assertion check code into the AST node. An assert_redundantly statement is translated only if the command-line option noredundancy is turned off (which is the default). The translated assertion check code has the following form:
 [[assert E;]] ==
   boolean v = false;
   [[E, v]]
   if (!v) {
     throw new JMLAssertError();
   }
 

 also
   requires self != null;
   modifies self.*;
   ensures isCheckable(self) ==> self.assertionCode() != null;
 

Specified by:
visitJmlAssertStatement in interface JmlVisitor
Overrides:
visitJmlAssertStatement in class JmlAbstractVisitor
See Also:
visitJmlAssumeStatement(JmlAssumeStatement), translate()

visitJmlDebugStatement

public void visitJmlDebugStatement(JmlDebugStatement self)
Translates the given JML debug statement and stores the translated code into the AST node. The translated code has the following form:
 [[debug E;]] ==
   do {
      [[E]]
   } while (false);
 

 also
   requires self != null;
   modifies self.*;
   ensures self.assertionCode() != null;
 

Specified by:
visitJmlDebugStatement in interface JmlVisitor
Overrides:
visitJmlDebugStatement in class JmlAbstractVisitor
See Also:
visitJmlAssumeStatement(JmlAssumeStatement), translate()

isCheckable

private static boolean isCheckable(JmlAssertOrAssumeStatement clause)
Returns true if the given assume (or assert) statement is checkable. The statement is checkable if it is not a redundant specification or the command line option noredundancy is not turned on.


isCheckable

private static boolean isCheckable(JmlHenceByStatement clause)
Returns true if the given hence_by statement is checkable. The statement is checkable if it is not a redundant specification or the command line option noredundancy is not turned on.


isCheckable

private static boolean isCheckable(JmlLoopSpecification clause)
Returns true if the given loop invariant is checkable. The statement is checkable if it is not a redundant specification or the command line option noredundancy is not turned on. In addition, an informal variant function is not checkable.


visitJmlAssumeStatement

public void visitJmlAssumeStatement(JmlAssumeStatement self)
Translates the JML assume statement and stores the translated assertion check code into the AST node. An assume_redundantly statement is translated only if the command-line option noredundancy is turned off (which is the default). Note that the assumptions are checked only if the runtime option reportAssumptionViolation is set (which is the default). The translated assertion code has the following form:
 [[assume E;]] == 
   if (JMLChecker.reportAssumptionViolation()) {
     boolean v = false;
     [[E, v]]
     if (!v) {
       throw new JMLAssumeError();
     }
   }
 

 also
   requires self != null;
   modifies self.*;
   ensures isCheckable(self) ==> self.assertionCode() != null;
 

Specified by:
visitJmlAssumeStatement in interface JmlVisitor
Overrides:
visitJmlAssumeStatement in class JmlAbstractVisitor
See Also:
visitJmlAssertStatement(JmlAssertStatement), translate()

visitJmlGuardedStatement

public void visitJmlGuardedStatement(JmlGuardedStatement self)
Translates the given JML guarded statement. Currently not supported yet.

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

visitJmlHenceByStatement

public void visitJmlHenceByStatement(JmlHenceByStatement self)
Translates the given JML hence_by and stores the translated assertion check code into the AST node. An hence_by_redundantly statement is translated only if the command-line option noredundancy is turned off (which is the default). The translated assertion code has the following form:
 [[hence_by P;]] == 
   boolean v = false;
   [[P, v]]
   if (!v) {
      throw new JMLHenceByError();
   }
 

 also
   requires self != null;
   modifies self.*;
   ensures isCheckable(self) ==> self.assertionCode() != null;
 

Specified by:
visitJmlHenceByStatement in interface JmlVisitor
Overrides:
visitJmlHenceByStatement in class JmlAbstractVisitor
See Also:
visitJmlAssertStatement(JmlAssertStatement), supported yet.

visitJmlLoopStatement

public void visitJmlLoopStatement(JmlLoopStatement self)
Translates the given JML loop statement and stores the instrumented code into the AST node of self. The pretty-printer is supposed to print the instrumented code instead of the original AST node. For the structure of instrumented code, refer to methods transWhileLoop, transDoLoop, and transForLoop.

   also
     requires self != null;
     modifies self.*;
 

Specified by:
visitJmlLoopStatement in interface JmlVisitor
Overrides:
visitJmlLoopStatement in class JmlAbstractVisitor
See Also:
#transWhileLoop(), #transDoLoop(), #transForLoop(), RacPrettyPrinter#visitJmlLoopStatement()

invariantCheckCode

private RacNode invariantCheckCode(JmlLoopInvariant[] invs)
Returns code that checks the given loop invariants. If there is no invariant to check (e.g., all are redundant invariants and the command-line option --noredundancy is turned on), null is returned. Otherwise, the following form of code is returned.
  if (IS_ACTIVE()) {
    JMLChecker.enter();
    boolean v = false;
    [[I,v]]
    JMLChecker.exit();
    if (!v) {
      throw new JMLLoopInvariantError(...);
    }
  }
 

 requires invs != null;
 ensures (* \result may be null *);
 


variantCheckCode

private RacNode variantCheckCode(JmlVariantFunction[] vars)
Returns code that checks the given loop variants. If there is no variant to check (e.g., all are redundant variants and the command-line option --noredundancy is turned on), null is returned. Otherwise, the following form of code is returned.
  if (IS_ACTIVE()) {
    JMLChecker.enter();
    int v1 = 0;
    [[E1,v1]]
    JMLChecker.exit();
    if (v1 < 0 || (!isFirst && v1 >= vo1)) {
      throw new JMLLoopVariantError(...);
    }
    vo1 = v1;
    isFirst = false;
  }
  ...
  if (IS_ACTIVE()) {
    JMLChecker.enter();
    int vn = 0;
    [[E1,vn]]
    JMLChecker.exit();
    if (vn < 0 || (!isFirst && vn >= von)) {
      throw new JMLLoopVariantError(...);
    }
    von = vn;
    isFirst = false;
  }
 
The declaration of temporary variables such as vo1, ..., von, and isFirst is piggybacked through the name field of the RacNode, and is of the following string.
  boolean isFirst = true;
  int vo1 = 0;
  ...
  int von = 0;
 

 requires vars != null;
 ensures (* \result may be null *);
 


transWhileLoop

private void transWhileLoop(JmlLoopStatement self,
                            RacNode checkInv,
                            RacNode checkVar)
Translates the given JML loop statement with the given invariant check code and variant check code. The given loop statement is supposed to be a while loop. The translated code is stored into the AST node of self, and it has the following form:
 [[while (B) S]] == 
   {
     boolean v = false;
     <>
     while (true) {
       <>
       <>
       if (!(B)) {
         v = true;
         break;
       }
       S
     }
     if (!v) {
       <>
     }
   }
 

   requires self != null;
   requires checkInv != null || checkVar != null;
   requires self.loopStmt() instanceof JForStatement;
   modifies self.*;
 

See Also:
variantCheckCode(JmlVariantFunction[]), invariantCheckCode(JmlLoopInvariant[])

transDoLoop

private void transDoLoop(JmlLoopStatement self,
                         RacNode checkInv,
                         RacNode checkVar)
Translates the given JML loop statement with the given invariant check code and variant check code. The given loop statement is supposed to be a while loop. The translated code is stored into the AST node of self, and it has the following form:
 [[while (B) S]] == 
   {
     <>
     while (true) {
       <>
       <>
       if (!(B)) {
         break;
       }
       S
     }
     <>
   }
 

   requires self != null;
   requires checkInv != null || checkVar != null;
   requires self.loopStmt() instanceof JDoStatement;
   modifies self.*;
 

See Also:
variantCheckCode(JmlVariantFunction[]), invariantCheckCode(JmlLoopInvariant[])

transForLoop

private void transForLoop(JmlLoopStatement self,
                          RacNode checkInv,
                          RacNode checkVar)
Translates the given JML loop statement with the given invariant check code and variant check code. The given loop statement is supposed to be a for loop. The translated code is stored into the AST node of self, and it has the following form:
 [[for (I1, ..., In; B; U1, ..., Un) S]] == 
   {
     I1, ..., In;
     boolean vExit = false;
     boolean vIncr = false;
     <>
     while (true) {
       if (vIncr) {
         U1, ..., Un;
       } else {
         vIncr = true;
       }
       <>
       <>
       if (!(B)) {
         vExit = true;
         break;
       }
       S
     }
     if (!vExit) {
       <>
     }
   }
 

   requires checkInv != null || checkVar != null;
   requires self.loopStmt() instanceof JForStatement;
   modifies self.*;
 

See Also:
variantCheckCode(JmlVariantFunction[]), invariantCheckCode(JmlLoopInvariant[])

conjoinInvariants

private JExpression conjoinInvariants(JmlLoopInvariant[] invs)
Conjoins the given loop invariants and returns the result. If there is no invariant to conjoin (e.g., all are redundant invariants and the command-line option --noredundancy is turned on), null is returned.

 requires invs != null;
 ensures (* \result may be null *);
 


visitJmlInvariantStatement

public void visitJmlInvariantStatement(JmlInvariantStatement self)
Translates the given JML invariant statement. Currently not supported yet.

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

visitJmlNondetChoiceStatement

public void visitJmlNondetChoiceStatement(JmlNondetChoiceStatement self)
Translates the given JML nondeterministic choice statement. Currently not supported yet.

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

visitJmlNondetIfStatement

public void visitJmlNondetIfStatement(JmlNondetIfStatement self)
Translates the given JML nondeterministic if statement. Currently not supported yet.

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

visitJmlSpecStatement

public void visitJmlSpecStatement(JmlSpecStatement self)
Translates the given JML specification statement. Currently not supported yet.

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

visitJmlSetStatement

public void visitJmlSetStatement(JmlSetStatement self)
Translates the JML set statement and stores the translated assertion check code into the AST node. The translated assertion code has the following structure:
 [[set g = E;]] ==
   { 
      T g; 
      [[E,g]]
      ghost$g(g);      // dynamic call to setter
   }
 [[set g *= E;]] ==
   { 
      T g = ghost$v(); // dynamic call to getter
      T v; 
      [[E,v]]
      g *= v;          // commound assignments (e.g., +=, -=, etc).
      ghost$v(g);      // dynamic call to setter
   }
 

 also
   requires self != null;
   modifies self.*;
   ensures self.assertionCode() != null;
 

Specified by:
visitJmlSetStatement in interface JmlVisitor
Overrides:
visitJmlSetStatement in class JmlAbstractVisitor
See Also:
TransClass, TransInterface, TransType

ghostFieldSetter

private RacNode ghostFieldSetter(JClassFieldExpression fieldExpr,
                                 String argVar)
Returns Java source code that makes a dynamic call to the setter method of the given ghost field, fieldExpr, to set the ghost value to the value of the given variable, argVar. Assume that fieldExpr is of the form "E.g", where E's type is T. Then, the returned code has the following general structure:
  T v;
  [[E, v]]
  rac$invoke("T", v, "g", typeOf(argVar), wrapped(argVar));
 

 requires fieldExpr != null && argVar != null && 
          (* fieldExpr is a reference to a ghost field *);
 ensures \result != null;
 


getGhostFieldSetter

public static RacNode getGhostFieldSetter(JClassFieldExpression fieldExpr,
                                          String argVar,
                                          VarGenerator varGen)
Returns Java source code that makes a dynamic call to the setter method of the given ghost field, fieldExpr, to set the ghost value to the value of the given variable, argVar.


transPrefix

private static RacNode transPrefix(VarGenerator varGen,
                                   JClassFieldExpression fieldExpr)
Translates the prefix expression of the given field reference expression, fieldExpr. The expression is assumed to be a reference to a non-static ghost field. If there is no need to translate the prefix (e.g., super, T.super, this, T.this, T), then null is returned; otherwise, the translated code of the following form is returned.
  T v;
  [[E, v]]
 
where E is the prefix expression, and v is a temporary variable. The name of the temporary variable, v, is stored in the name field of the result object.

 requires varGen != null && fieldExpr != null;
 ensures (* \result may be null *);
 


isStatic

private static boolean isStatic(JClassFieldExpression expr)
Returns true if the given field expression is a reference to a static field.

 requires expr != null;
 


operator

public static String operator(JAssignmentExpression expr)
Returns the string representation of the assignment operator of the given assignment expression. E.g., " = " for simple assignment expression.

 requires expr != null;
 ensures \result != null && \fresh(\result);
 


visitJmlUnreachableStatement

public void visitJmlUnreachableStatement(JmlUnreachableStatement self)
Translates the JML unreachable statement. The translated assertion code has the following form:
 [[unreachable;]] == check(v [&& !assumed]);
 
The optional conjunction in the check statement is generated only if the statement is in the scope of any assume statement. This is because the assert condition must hold only if the assume conditions hold. The flag assumed is set by assume statements.

Specified by:
visitJmlUnreachableStatement in interface JmlVisitor
Overrides:
visitJmlUnreachableStatement in class JmlAbstractVisitor
See Also:
visitJmlAssumeStatement(JmlAssumeStatement)

visitAssertStatement

public void visitAssertStatement(JAssertStatement self)
Translates the given Java assert statement.

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

visitBlockStatement

public void visitBlockStatement(JBlock self)
Translates the given Java block statement.

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

visitConstructorBlock

public void visitConstructorBlock(JConstructorBlock self)
Translates the given Java constructor statement.

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

visitBreakStatement

public void visitBreakStatement(JBreakStatement self)
Translates the given Java break statement.

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

visitCompoundStatement

public void visitCompoundStatement(JCompoundStatement self)
Translates the given Java compound statement.

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

visitCompoundStatement

public void visitCompoundStatement(JStatement[] body)
Translates the given Java compound statement.

Overrides:
visitCompoundStatement in class JmlAbstractVisitor

visitContinueStatement

public void visitContinueStatement(JContinueStatement self)
Translates the given Java continue statement.

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

visitEmptyStatement

public void visitEmptyStatement(JEmptyStatement self)
Translates the given Java empty statement.

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

visitExpressionListStatement

public void visitExpressionListStatement(JExpressionListStatement self)
Translates the given Java expression list statement.

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

visitExpressionStatement

public void visitExpressionStatement(JExpressionStatement self)
Translates the given Java expression statement.

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

visitIfStatement

public void visitIfStatement(JIfStatement self)
Translates the given Java if statement.

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

visitLabeledStatement

public void visitLabeledStatement(JLabeledStatement self)
Translates the given Java labeled statement.

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

visitForStatement

public void visitForStatement(JForStatement self)
Translates the given Java for statement.

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

visitDoStatement

public void visitDoStatement(JDoStatement self)
Translates the given Java do statement.

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

visitWhileStatement

public void visitWhileStatement(JWhileStatement self)
Translates the given Java while statement.

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

visitReturnStatement

public void visitReturnStatement(JReturnStatement self)
Translates the given Java return statement.

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

visitSwitchStatement

public void visitSwitchStatement(JSwitchStatement self)
Translates the given Java switch statement.

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

visitSwitchGroup

public void visitSwitchGroup(JSwitchGroup self)
Translates the given Java switch group statement.

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

visitSynchronizedStatement

public void visitSynchronizedStatement(JSynchronizedStatement self)
Translates the given Java synchronized statement.

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

visitThrowStatement

public void visitThrowStatement(JThrowStatement self)
Translates the given Java throw statement.

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

visitTryCatchStatement

public void visitTryCatchStatement(JTryCatchStatement self)
Translates the given Java try/catch statement.

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

visitTryFinallyStatement

public void visitTryFinallyStatement(JTryFinallyStatement self)
Translates the given Java try/finally statement.

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

visitTypeDeclarationStatement

public void visitTypeDeclarationStatement(JTypeDeclarationStatement self)
Translates the given Java type declaration statement.

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

visitVariableDeclarationStatement

public void visitVariableDeclarationStatement(JVariableDeclarationStatement self)
Translates the given Java variable declaration statement.

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

needDynamicInvocationMethod

private static void needDynamicInvocationMethod()
Records that a ghost field inheritance mechanism is needed.


defaultValue

public static String defaultValue(CType type)
Return the default value of the type type.


isActive

protected String isActive()
Returns a string representation of the condition that tests if the given type of assertion is active. Assertion checking is active only when the instance has completed its construction.


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.