org.jmlspecs.jmlrac
Class WrapperMethod

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.jmlrac.TransUtils
          org.jmlspecs.jmlrac.WrapperMethod

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, RacConstants

Direct Known Subclasses:

ConstructorWrapper, FinalizerWrapper

public class WrapperMethod

extends TransUtils

A class for generating wrapper methods. A wrapper method is a method that wraps a method with assertion check methods such as pre and postcondition check methods. The original method is renamed and called by the wrapper method inside the wrap. Wrapper methods are generated for only concrete methods; no wrapper methods are generated for abstract methods.

Version:

$Revision: 1.31 $

Author:

Yoonsik Cheon

Field Summary
protected  StringBuffer	args           arguments to pre/orig, post, or xpost method calls
private  boolean	hasReturn           true if the target method has return type.
protected  String	ident           name of the target method.
protected  boolean	isHelper           true if the target method is a helper.
protected  boolean	isStatic           true if the target method is a static method.
protected  JmlMethodDeclaration	methodDecl           target method to be wrapped.
protected  StringBuffer	postArgs           arguments to pre/orig, post, or xpost method calls
protected  CType	returnType           return type of the target method.
protected  String	typeName           type name whose methods are to be wrapped.
protected  StringBuffer	xpostArgs           arguments to pre/orig, post, or xpost method calls

 

Fields inherited from class org.jmlspecs.jmlrac.TransUtils

typeDecl

 

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

WrapperMethod(String typeName, JmlMethodDeclaration mdecl)           Construct a new instance.

 

Method Summary
protected  void	buildArguments()           Builds arguments to various assertion check methods such as pre- and postcondition check methods.
protected  JBlock	buildWrapperBody()           Returns code for the body of the wrapper method being created.
protected  String	callOriginalMethod()           Returns code for invoking the original method.
protected  String	checkConstraint()           Returns code for checking history constraint.
protected  String	checkPostcondition()           Returns code for checking normal postcondition.
protected  String	checkPostInvariant()           Returns code for checking invariant in the post-state.
protected  String	checkPrecondition()           Returns code for checking precondition.
protected  String	checkPreInvariant()           Returns code for checking invariant in the pre-state.
protected  String	checkXPostcondition()           Returns code for checking exceptional postcondition.
protected  String	constraintCallArg()           Returns, in the string form, the argument for calling a constraint check method.
protected  String	evalOldInConstraint()           Returns code for evaluating old expressions in constraints.
JMethodDeclarationType	generate()           Returns a wrapper method.
protected  String	identification(String state)           Returns a string that identifies the method being translated.
protected  String	isActive(String type)           Returns a string representation of the condition that tests if the given type of assertion is active.
protected  String	mandatoryReturn()           Returns a mandatory return statement.
protected  String	nocheckDuringInit()           Returns code for bypassing assertion checks during the class and instance initialization.
protected  String	optionalReturn()           Returns an optional return statement.
protected  String	racMethodName(String type)           Returns the name of runtime assertion checker method for the given type.
protected  String	resultVarDecl()           Returns code for declaring result variable.
protected  String	wrap(String type, String comment, String stmt)           Returns the given statement, stmt, wrapped in assertion check demarcation.
protected  String	wrap2(String type, String comment, String stmt)           Returns the given statement, stmt, wrapped in assertion check demarcation.
protected  String	wrap3(String type, String comment, String stmt)           Returns the given statement, stmt, wrapped in assertion check demarcation.

 

Methods inherited from class org.jmlspecs.jmlrac.TransUtils

applyBigintBinOperator, applyBigintCast, applyBigintToNumber, applyBigintUnOperator, applyUnaryPromoteExpression, beingTested, createBigintConvertionAssertion, defaultValue, dynamicCallName, evalOldName, evalOldName, evalOldName, evalOldName, excludedFromInheritance, getTypeID, initIncludedInInheritance, invariantLikeName, isBigintArray, isMain, modelPublicAccessorName, numberToBigint, specAccessorNeeded, specPublicAccessorName, subtypeConstraintName, toPrintableString, toString, toString, toString, typeToClass, unwrapObject, useReflection, wrappedValue, wrapValue

 

Methods inherited from class org.multijava.util.Utils

assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

typeName

protected final String typeName

type name whose methods are to be wrapped. This field is used to generate the names of various assertion check methods.

methodDecl

protected final JmlMethodDeclaration methodDecl

target method to be wrapped.

 protected invariant methodDecl != null;
 

isHelper

protected final boolean isHelper

true if the target method is a helper.

 protected invariant isHelper == methodDecl.isHelper();
 

isStatic

protected final boolean isStatic

true if the target method is a static method.

 protected invariant isStatic == methodDecl.isStatic();
 

hasReturn

private final boolean hasReturn

true if the target method has return type.

 private invariant hasReturn == 
   (returnType != null && !returnType.isVoid());
 

returnType

protected final CType returnType

return type of the target method.

 private invariant returnType == methodDecl.returnType();
 

ident

protected final String ident

name of the target method.

 private invariant ident == methodDecl.ident();
 

args

protected StringBuffer args

arguments to pre/orig, post, or xpost method calls

postArgs

protected StringBuffer postArgs

arguments to pre/orig, post, or xpost method calls

xpostArgs

protected StringBuffer xpostArgs

arguments to pre/orig, post, or xpost method calls

WrapperMethod

public WrapperMethod(String typeName,
                     JmlMethodDeclaration mdecl)

Construct a new instance.

 requires typeName != null && mdecl != null && mdecl.body() != null;
 

Parameters:

mdecl - method to be wrapped; must not be abstract.

generate

public JMethodDeclarationType generate()

Returns a wrapper method. The original method is renamed and called by the wrapper method enclosed in assertion check code such as pre and postcondition check methods. The body of the wrapper method has the following general structure:

 T m(T1 x1, ..., Tn xn) {
   checkPre$m(x1, ..., xn);
   checkInv();
   T r = init_T;
   boolean ok = true;
   try {
     r = orig$m(x1, ..., xn);
     checkPost$m(x1, ..., xn, r);
   }
   catch (JMLEntryPreconditionError e) {
     ok = false;
     throw new JMLInternalPreconditionError(e);
   }
   catch (JMLExitPostconditionError e) {
     ok = false;
     throw new JMLInternalPostconditionError(e);
   }
   catch (JMLAssertionError e) {
     ok = false;
     throw e;
   }
   catch (Throwable e) {
     try {
       checkXPost$m(x1, ..., xn, r, e);
     } 
     catch (JMLAssertionError e1) {
       ok = false;
       throw e1;
     }
   }
   finally {
     if (ok) {
        checkInv();
        checkConstraint();
     }
   }
 }
 

 old String n = methodDecl.ident();
 modifies methodDecl.*;
 assignable args, postArgs, xpostArgs;
 ensures methodDecl.ident().equals(MN_INTERNAL + n) &&
         \fresh(\result);
 

buildWrapperBody

protected JBlock buildWrapperBody()

Returns code for the body of the wrapper method being created. For the structure of the returned code refers to the method generate().

 ensures \result != null;
 

See Also:

generate()

nocheckDuringInit

protected String nocheckDuringInit()

Returns code for bypassing assertion checks during the class and instance initialization. Assertions are also not checked while the object is being constructed. The returned code has the following structure.

  if (!VN_CLASS_INIT [|| !VN_INIT] [|| !VN_CONSTRUCTED()]) {
     [return] m(x1, ..., xn);
     [return;]
  }
 

checkPreInvariant

protected String checkPreInvariant()

Returns code for checking invariant in the pre-state. If the method being translated is a helper method, an empty string is returned; otherwise, the following form of code is returned.

  // check static invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT)) {
    JMLChecker.enter();
    checkInv$static();
    JMLChecker.exit();
  }
  // check instance invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT)) {
    JMLChecker.enter();
    checkInv$instance$T();
    JMLChecker.exit();
  }
 

where T is the name of type being translated. The code for checking instance invariant is generated only if the target method is an instance method.

   requires isHelper;
   ensures \fresh(\result) && "".equals(\result);
 also
   requires !isHelper;
   ensures \fresh(\result) && \result.length() > 0 &&
     (* \result is of the above form of code *);
 

checkPostInvariant

protected String checkPostInvariant()

Returns code for checking invariant in the post-state. If the target method being translated is a helper method, an empty string is returned; otherwise, the following form of code is returned.

  // check static invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT)) {
    JMLChecker.enter();
    checkInv$static();
    JMLChecker.exit();
  }
  // check instance invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT)) {
    JMLChecker.enter();
    checkInv$instance$T();
    JMLChecker.exit();
  }
 

where T is the name of type being translated. The code for checking instance invariant is generated only if the target method is an instance method.

   requires isHelper;
   ensures \fresh(\result) && "".equals(\result);
 also
   requires !isHelper;
   ensures \fresh(\result) && \result.length() > 0 &&
     (* \result is of the above form of code *);
 

evalOldInConstraint

protected String evalOldInConstraint()

Returns code for evaluating old expressions in constraints. A helper need not establish the constraints. Thus, an empty string is returned for a helper and the following form of code for a non-helper.

  // eval old exprs in static constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    evalOldExprInHC$satic(); 
    JMLChecker.exit();
  }
  // eval old exprs in non-static constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    evalOldExprInHC$instance$T();
    JMLChecker.exit();
  }
 

where T is the name of type being translated. The code for instance constraints is generated only if the target method is an instance method.

checkConstraint

protected String checkConstraint()

Returns code for checking history constraint. The constraint is not checked for constructors. If the target method being translated is a helper method, an empty string is returned; otherwise, the following form of code is returned.

  // check static constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    checkHC$static();
    JMLChecker.exit();
  }
  // check instance constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    checkHC$instance$T();
    JMLChecker.exit();
  }
 

where T is the name of type being translated. The code for checking instance constraint is generated only if the target method is an instance method.

constraintCallArg

protected String constraintCallArg()

Returns, in the string form, the argument for calling a constraint check method.

buildArguments

protected void buildArguments()

Builds arguments to various assertion check methods such as pre- and postcondition check methods. If the target method has arguments x1, x2, ..., xn, and throws some exceptions, this method sets the field args to "(x1,...,xn)", postArgs to "(x1,...,xn,VN_RESULT)", and xpostArgs to "(x1,...,xn,VN_XRESULT)".

 assignable args, postArgs, xpostArgs;
 ensures args != null && postArgs != null && xpostArgs != null;
 

callOriginalMethod

protected String callOriginalMethod()

Returns code for invoking the original method. I.e., [ VN_RESULT = ] internal$m(x1,...,xn);.

resultVarDecl

protected String resultVarDecl()

Returns code for declaring result variable. I.e., T VN_RESULT = init_value_of_T;, where T is the return type.

checkPrecondition

protected String checkPrecondition()

Returns code for checking precondition. The returned code has the following structure.

  // check precondition
  if (JMLChecker.isActive(JMLChecker.PRECONDITION)) {
    JMLChecker.enter();
    checkPre$m$T(x1,...,xn);
    JMLChecker.exit();
  }
 

where m is the name of method being translated and T is the name of the owning type.

checkPostcondition

protected String checkPostcondition()

Returns code for checking normal postcondition. The returned code has the following structure.

  // check normal postcondition
  if (JMLChecker.isActive(JMLChecker.POSTCONDITION)) {
    JMLChecker.enter();
    checkPost$m$T(x1,...,xn,r);
    JMLChecker.exit();
  }
 

where m is the name of method being translated and T is the name of the owning type.

checkXPostcondition

protected String checkXPostcondition()

Returns code for checking exceptional postcondition. The returned code has the following structure.

  // check exceptional postcondition
  if (JMLChecker.isActive(JMLChecker.POSTCONDITION)) {
    JMLChecker.enter();
    checkXPost$m$T(x1,...,xn,r,e);
    JMLChecker.exit();
  }
 

where m is the name of method being translated and T is the name of the owning type.

mandatoryReturn

protected String mandatoryReturn()

Returns a mandatory return statement. I.e, return [ VN_RESULT ];. The optional result variable is generated only if the method being translated has a non-void return type.

optionalReturn

protected String optionalReturn()

Returns an optional return statement. I.e, [ return VN_RESULT ; ]. If the method being translated has a void return type, the result is an empty string.

wrap

protected String wrap(String type,
                      String comment,
                      String stmt)

Returns the given statement, stmt, wrapped in assertion check demarcation. The returned code has the following structure.

  // comment
  if (JMLChecker.isActive(JMLChecker.type)) {
    JMLChecker.enter();
    stmt;
    JMLChecker.exit();
  }
 


Parameters:
type - assertion type, e.g., PRECONDITION, etc.
comment - header comment
stmt - statement to be wrapped

wrap2

protected String wrap2(String type,
                       String comment,
                       String stmt)

Returns the given statement, stmt, wrapped in assertion check demarcation. The whole code is indented two tabs. The returned code has the following structure.

  // comment
  if (JMLChecker.isActive(JMLChecker.type)) {
    JMLChecker.enter();
    stmt;
    JMLChecker.exit();
  }
 


Parameters:
type - assertion type, e.g., PRECONDITION, etc.
comment - header comment
stmt - statement to be wrapped

wrap3

protected String wrap3(String type,
                       String comment,
                       String stmt)

Returns the given statement, stmt, wrapped in assertion check demarcation. The whole code is indented three tabs. The returned code has the following structure.

  // comment
  if (JMLChecker.isActive(JMLChecker.type)) {
    JMLChecker.enter();
    stmt;
    JMLChecker.exit();
  }
 


Parameters:
type - assertion type, e.g., PRECONDITION, etc.
comment - header comment
stmt - statement to be wrapped

isActive

protected String isActive(String type)

Returns a string representation of the condition that tests if the given type of assertion is active.

 ensures \result.equals("JMLChecker.isActive(JMLChecker." + type +")"); 
 

identification

protected String identification(String state)

Returns a string that identifies the method being translated.

racMethodName

protected String racMethodName(String type)

Returns the name of runtime assertion checker method for the given type.

 requires (* type is MN_CHECK_PRE, MN_CHECK_POST, MN_CHECK_XPOST, etc.*);
 ensures \result.equals(type + ident + "$" + typeName);