(David Cok): THIS IS NOT UP TO DATE The original code (which is intact) has been embellished to handle the situation in which source code is not available to be used to generate new java code containing runtime assertion checks. This is the case, for example, in checking the assertions of classes in java.* . This situation obtains when the assertion check code is being generated from a non-.java file and the object being tested is a class, not an interface. In this case the variable genSpecTestFile is set true, and the generated code is produced as follows. (If genSpecTestFile==false, the original rewrite-the-java-file mechanism is used unchanged.)

The generated class must be different from the class under test, since it cannot replace it. We presume that we cannot add to the package of the class under test either, and in any case it is convenient to have the generated class have the same name as the class under test (convenient for generating test code). Thus we use the same class name but a different package for the generated class. For clarity, we will call the class under test class p.C and the generated class testspecs.p.C . The actual generated class name is determined by the --packageName option.

There are two subcases. One in which we generate a subclass of p.C, which is called Wrapper, and one in which we do not generate such a subclass. The variable genWrapperClass is true in the first case, false in the second.

• genWrapperClass must be true if there are any protected methods, fields, or constructors that must be tested or are used in specifications.
• genWrapperClass must be false if the class p.C is final
• genWrapperClass must be false if the class p.C has only or private constructors
• genWrapperClass must be false if the class p.C has fields that are of type p.C (e.g. BigInteger.ZERO, Double.MAX_INTEGER) because we have not implemented any mechanisms to convert a p.C object to a Wrapper object. Although straightforward for BigInteger and Double, it would need to rely on the presence of a copy constructor. Hence we just forbid a Wrapper class in this case.
• If a protected method of p.C is final, we are stuck - we cannot test or access this method.

We generate testspecs.p.C with the following content.

• - All methods that check specifications are members of the generated class, as they are in the case of genSpecTestFile==false, but some field or method access may be different.
• - (genWrapperClass==true): A static public nested class named Wrapper which has p.C as a super class and with content as described in the following.
• - A field named delegee of type p.C if genWrapperClass==false of type Wrapper if genWrapperClass==true
• - Members of p.C with package or private access are not available and cannot be tested. If specifications need to access these members, it may not be possible to test the class.
• - For each public method m of p.C: a public method m in testspecs.p.C is generated (even with genSpecTestFile false) that checks specifications appropriately, calling internal$m(...) as needed. When genSpecTestFile==true, internal$m is modified to call delegee.m(...)
• - For each protected method m of p.C: [must have genWrapperClass==true] a public method m in testspecs.p.C is *generated (even with genSpecTestFile false) that checks *specifications appropriately, calling internal$m(...) as needed. *When genSpecTestFile==true, internal$m is modified to call *delegee.m(...) Also generate a public method in Wrapper with the *same name and arguments that simply calls/returns super.m(...). *Note: If there are any such protected methods of p.C, then *genWrapperClass must be true, since testspecs.p.C will not be able *to call p.C.m .
• - For each public constructor of p.C: If (genWrapperClass==false) generate a public constructor in testspecs.p.C that checks specifications appropriately, calling new p.C(...) as needed. If (genWrapperClass==true) generate a public constructor in testspecs.p.C that checks specifications appropriately, calling new Wrapper(...) as needed and generate a public constructor in Wrapper with the same name and arguments that simply calls super(...)
• - For each protected constructor of p.C: [Must have genWrapperClass==true] generate a public constructor in testspecs.p.C that checks specifications appropriately, calling new Wrapper(...) as needed. And if (genWrapperClass==true) generate a public method in Wrapper with the same name and arguments that simply calls/returns super(...) [not strictly needed for public methods of p.C].
• - there are no public or protected constructors of p.C then genWrapperClass must be false. We then add one constructor to testspecs.p.C of the form public C(p.C o) { delegee = o; } [genWrapperClass==false] public C(Wrapper o) { delegee = o; } [genWrapperClass==true]
• If p.C has only a default constructor, then testspecs.p.C is given a constructor with no arguments that simply sets delegee == new p.C();
• - For each public field f of p.C: If (genWrapperClass==false) references to the field in specifications are changed to delegee.f If (genWrapperClass==true) generate a public method in Wrapper named spec$f$C that simply returns the value of the field. References to the field in specifications will call delegee.spec$f$C(). [ In this latter case, we could use delegee.f, but we do it this way to be consistent with the mechanism for protected fields.]
• - For each protected field f of p.C: [Must have genWrapperClass==true] generate a public method in Wrapper named spec$f$C that simply returns the value of the field. Any references to the field in specifications will call delegee.spec$f$C().
• - Creating objects for testcases. The receivers need to be of type testspecs.p.C. Other objects used as arguments should be of dynamic type Wrapper (if getWrapperClass is true) otherwise of type p.C .

Version:

$Revision: 1.74 $

Author:

Yoonsik Cheon, David Cok

See Also:

TransClass, TransInterface

Field Summary
private static CClass	currentCClass           CClass of the target type declaration.
protected static boolean	dynamicInvocationMethodNeeded           True if a dynamic invocation method need be generated for the current type declaration as the result of the translation.
static boolean	genSpecTestFile           true if we are operating on spec files
static boolean	genWrapperClass
private  ArrayList	laterMethods
protected  Set	modelMethods           The set of model or spec_public field names whose access methods have alredy been generated.
static boolean	specInheritanceMethodNeeded           True if a specification inheritance method need be generated for the current type declaration as the result of the translation.
protected  JmlTypeDeclaration	typeDecl           Target type declaration to be translated.
protected  VarGenerator	varGen           Variable generator for generating fresh variable names.

 

Fields inherited from class org.jmlspecs.jmlrac.TransUtils

 

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
protected	TransType(JmlTypeDeclaration typeDecl)           Constructs a TransType object.

 

Method Summary
protected abstract  void	addNewMethod(JmlMethodDeclaration mdecl)           Adds a new method declaration, mdecl, to the instrumented type.
static boolean	dynamicCallNeeded(CClass clazz)           Returns true if dynamic calls are needed to access model, ghost, spec_public, and spec_protected fields declared in the given class clazz.
protected  JmlMethodDeclaration	dynamicInvocationMethod()           Returns a method declaration that makes a dynamic call to the given method using the Java's reflection facility.
protected  void	finalizeTranslation()           Finalizes translation of the type declaration.
protected  JmlTypeDeclaration	findTypeWithRepresentsFor(JmlTypeDeclaration tdecl, CField field)           Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration.
protected  JmlMethodDeclaration	forNameMethod()           Returns a method declaration that returns the class object associated with the class or interface with the given string name.
protected  JmlMethodDeclaration	ghostFieldAccessors(JmlFieldDeclaration fdecl)           Returns a pair of ghost field accessor methods (getter and setter) for the given ghost field declaration.
static String	ident()           Returns the identifier of the type currently being tranlated.
protected  JmlMethodDeclaration	initFlags()           Returns declarations of class/instance initialization flags.
protected  boolean	isAccessorGenerated(CField field)           Returns true if an accessor (or a delegation method) is already generated for a model or spec_public field, field.
static boolean	isInterface()           Returns true if the currently tranlated type is an interface.
private static boolean	isRepresentsDeclExecutable(JmlRepresentsDecl rdecl)           Returns true if the given represents declaration is translatable.
private  JmlMethodDeclaration	modelFieldAccessor(JmlSourceField field, JExpression expr)           Returns a model accessor method for a model field with the given expression (of the represents clause).
void	postTranslationChangesForSpecTestFile(String wrapperClass)
private  void	prepareSpecTestFile()
protected abstract  String	receiver(String className, String clazz, String receiver)           Returns a string form of code that, if executed, returns the receiver of for a dynamic call.
protected  void	setAccessorGenerated(CField field)           Indicates that an accessor (or a delegation method) has been generated for a model or spec_public field, field.
void	translate()           Translates the given type declaration.
protected  void	translateBody(ArrayList inners, ArrayList methods, JPhylum[] fieldsAndInits)           Translates a class body, either of class or interface.
protected abstract  void	translateConstraint()           Translates history constraints, both static and non-static.
protected  JmlFieldDeclaration	translateField(JmlFieldDeclaration fieldDecl)           Translates a JML field declaration, fieldDecl.
String	translateForSpecTestFile()
protected abstract  void	translateInvariant()           Translates invariants, both static and non-static invariants.
protected abstract  void	translateMethod(JmlMethodDeclaration mdecl)           Translates a JML method declaration.
protected  void	translateModelMethod(JmlMethodDeclaration mdecl)           Translates the given model method (or constructor), mdecl. !
protected  void	translateRepresents(JmlRepresentsDecl[] repDecls)           Translates represents clauses of this type declaration.
private  String	unwrap(CType t, String val)
private  String	wrap(CType t, String val)

 

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

genSpecTestFile

public static boolean genSpecTestFile

true if we are operating on spec files

genWrapperClass

public static boolean genWrapperClass

laterMethods

private ArrayList laterMethods

typeDecl

protected JmlTypeDeclaration typeDecl

Target type declaration to be translated.

 protected invariant typeDecl.getCClass() == currentCClass;
 

varGen

protected VarGenerator varGen

Variable generator for generating fresh variable names.

currentCClass

private static CClass currentCClass

CClass of the target type declaration.

dynamicInvocationMethodNeeded

protected static boolean dynamicInvocationMethodNeeded

True if a dynamic invocation method need be generated for the current type declaration as the result of the translation.

See Also:

dynamicInvocationMethod()

specInheritanceMethodNeeded

public static boolean specInheritanceMethodNeeded

True if a specification inheritance method need be generated for the current type declaration as the result of the translation.

See Also:

TransExpression#visitJmlInvariantForExpression()

modelMethods

protected Set modelMethods

The set of model or spec_public field names whose access methods have alredy been generated.

See Also:

translateRepresents(JmlRepresentsDecl[]), translateField(JmlFieldDeclaration)

TransType

protected TransType(JmlTypeDeclaration typeDecl)

Constructs a TransType object.

Parameters:

typeDecl - target type declaration to be translated

 requires typeDecl != null;
 

prepareSpecTestFile

private void prepareSpecTestFile()

translate

public void translate()

Translates the given type declaration. The translation may produce a collection of assertion check methods.

translateInvariant

protected abstract void translateInvariant()

Translates invariants, both static and non-static invariants. This method must be implemented by concrete subclasses.

translateConstraint

protected abstract void translateConstraint()

Translates history constraints, both static and non-static. This method must be implemented by concrete subclasses.

translateForSpecTestFile

public String translateForSpecTestFile()

wrap

private String wrap(CType t,
                    String val)

unwrap

private String unwrap(CType t,
                      String val)

postTranslationChangesForSpecTestFile

public void postTranslationChangesForSpecTestFile(String wrapperClass)

translateRepresents

protected void translateRepresents(JmlRepresentsDecl[] repDecls)

Translates represents clauses of this type declaration. For each executable (i.e., functinal abstraction) form of represents clause, this method generates a model field accessor method that calculates the value of the model field in terms of the represents clause's expression. The accessor method has the following general form:

 [[represents m <- E;]] ==
   protected T m() {
     T v = T_init;
     [[E, v]]
     return v;
   }
 

where T is the type of expression E and v is a unique local variable. The generated method declaration is added to the current type (or surrogate class if the type is an interface), and the field is marked that its model access method is generated.

 requires repDecls != null;
 

See Also:

translateField(JmlFieldDeclaration), addNewMethod(JmlMethodDeclaration), setAccessorGenerated(CField)

finalizeTranslation

protected void finalizeTranslation()

Finalizes translation of the type declaration. This method may be overridden by subclasses to do subclass-specific finalization such as generation of specification inheritance mechanism (i.e., inheritance method, surrogate class, etc.). However, this method method must be called at the end to do the common finalization such as adding class/instance initialization flags.

translateBody

protected void translateBody(ArrayList inners,
                             ArrayList methods,
                             JPhylum[] fieldsAndInits)

Translates a class body, either of class or interface.

Parameters:

inners - inner classes

methods - mthod declarations

fieldsAndInits - field declarations

 requires inners != null && methods != null && fieldsAndInits != null;
 

translateField

protected JmlFieldDeclaration translateField(JmlFieldDeclaration fieldDecl)

Translates a JML field declaration, fieldDecl. This method strips off the final modifier from the field declaration. If necessary, this method should be overwritten by subclasses to specially handle final, model, model, spec_public, and spec_protected fields.

 requires fieldDecl != null;
 modifies fieldDecl.*;
 ensures \result != null && \result == fieldDecl;
 

translateModelMethod

protected void translateModelMethod(JmlMethodDeclaration mdecl)

Translates the given model method (or constructor), mdecl. !FIXME!describe translation rules.

translateMethod

protected abstract void translateMethod(JmlMethodDeclaration mdecl)

Translates a JML method declaration. A translation of JML method declaration produces four new methods, and the original method is renamed and made private-accessible:

• Precondition checking method. A protected method to check the precondition of the original method (refer to the class PreconditionMethod).

• Normal and exceptional postcondition checking methods. A couple of protected methods to check the normal and exceptional postconditions of the original method (refer to the classes PostconditionMethod and ExceptionalPostconditionMethod).

• Wrapper method. A wrapper method that wraps the original method with pre and postcondition checking (refer to the class WappersMethod).

  The translation also generate several new instance fields to store temporally values used by the assertion checking methods. There are three kinds of variables that are generated and declared as instance fields.

  • Precondition variables.
  • Old (\old) expression variables.
  • Specification variables.

Similarly, translation of JML constructor declaration also produces four new methods, and the original constructor becomes a wrapper method (refer to the class TransConstructor).

 requires mdecl != null;
 

ghostFieldAccessors

protected JmlMethodDeclaration ghostFieldAccessors(JmlFieldDeclaration fdecl)

Returns a pair of ghost field accessor methods (getter and setter) for the given ghost field declaration. The name of both accessors is MN_GHOST + ident + "$" + className, where the constant MN_GHOST is usually "ghost$" and ident is the name of the ghost field. The accessor methods has the following general structure:

  public [static] T ghost$v$C() {
     return v;
  } 
  public [static] void ghost$v$C(T x) {
     v = x;
  } 
 

This method also generates a private field for storing ghost values and possibly an initializer block too. They are stored in the given field declaration for later pretty-printing (see RacPrettyPrinter.visitJmlFieldDeclaration).

  private [static] T v;
  [static] {
     v = initializer;
  }
 

 requires fdecl != null && hasFlag(fdecl.modifiers(), ACC_GHOST);
 modifies fdecl.*;
 ensures \result != null;
 

initFlags

protected JmlMethodDeclaration initFlags()

Returns declarations of class/instance initialization flags. The initialization flags indicate if classes/instances have finished their initializations, and are used to prevent invariant checks from happening during initialization.

addNewMethod

protected abstract void addNewMethod(JmlMethodDeclaration mdecl)

Adds a new method declaration, mdecl, to the instrumented type.

modelFieldAccessor

private JmlMethodDeclaration modelFieldAccessor(JmlSourceField field,
                                                JExpression expr)

Returns a model accessor method for a model field with the given expression (of the represents clause).

Parameters:

field - model field

expr - the right hand side of the represents clause (e.g., E in m <- E.

 requires field != null && field.isModel() && expr != null;
 ensures \result != null;
 

findTypeWithRepresentsFor

protected JmlTypeDeclaration findTypeWithRepresentsFor(JmlTypeDeclaration tdecl,
                                                       CField field)

Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration. If such a clause is found, returns the type declaration that includes the clause; otherwise, returns null.

 requires tdecl != null && 
   field != null && hasFlag(field.modifiers(),ACC_MODEL);
 ensures \result != null ==> (* \result has represents clause  r 
   such that !r.isRedundantly() && r.usesAbstractionFunction() && 
   r.storeRef() refers to field *);
 

isRepresentsDeclExecutable

private static boolean isRepresentsDeclExecutable(JmlRepresentsDecl rdecl)

Returns true if the given represents declaration is translatable. A represents declaration is translatable if the following conditions are satisfied:

• It is not redundant.
• It uses a functional abstraction; i.e., it is of the form: x <- E).

 requires rdecl != null;
 

dynamicInvocationMethod

protected JmlMethodDeclaration dynamicInvocationMethod()

Returns a method declaration that makes a dynamic call to the given method using the Java's reflection facility. The target method is specified by its name, its owner's class name, formal parameter types, and actual arguments. The target method is typically an access method generated by the runtime assertion checker, such as an accessor for a model, ghost, spec_public, or spec_protected field, a setter for a ghost field, and an accessor for a spec_public or spec_protected method. The return value is that of the target method, if necessary, wrapped in an object. If the target method is not found, a instance of JMLNonExecutableException is thrown. If the target method throws a RuntimeException, including JMLNonExecutableException, the exception is rethrown; for other types of exceptions, an instanceof RuntimeException is thrown.

 ensures \result != null;
 

forNameMethod

protected JmlMethodDeclaration forNameMethod()

Returns a method declaration that returns the class object associated with the class or interface with the given string name.

 ensures \result != null;
 

receiver

protected abstract String receiver(String className,
                                   String clazz,
                                   String receiver)

Returns a string form of code that, if executed, returns the receiver of for a dynamic call. This method is used by the method dynamicInvocationMethod to define a subclass-specific dynamic invocation method.

See Also:

dynamicInvocationMethod()

isAccessorGenerated

protected boolean isAccessorGenerated(CField field)

Returns true if an accessor (or a delegation method) is already generated for a model or spec_public field, field.

setAccessorGenerated

protected void setAccessorGenerated(CField field)

Indicates that an accessor (or a delegation method) has been generated for a model or spec_public field, field.

dynamicCallNeeded

public static boolean dynamicCallNeeded(CClass clazz)

Returns true if dynamic calls are needed to access model, ghost, spec_public, and spec_protected fields declared in the given class clazz. The return value is true if the given class is not the same as the one being translated now.

isInterface

public static boolean isInterface()

Returns true if the currently tranlated type is an interface.

ident

public static String ident()

Returns the identifier of the type currently being tranlated.