JML

org.jmlspecs.jmlrac
Class TransMethod

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.jmlrac.TransUtils
          extended byorg.jmlspecs.jmlrac.TransMethod
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, RacConstants
Direct Known Subclasses:
TransConstructor

public class TransMethod
extends TransUtils

A class for translating JML annotated Java methods into RAC-enabled methods. The translation produces new methods and fields that must be added to the target class, and also renames the original method.

A non_null annotation to a formal parameter is interpreted as a part of preconditions. That is, a non_null annotation to a formal parameter, say x, has the same effect as conjoining the predicate x != null to the precondition of the method.

Version:
$Revision: 1.66 $
Author:
Yoonsik Cheon

Nested Class Summary
protected static class TransMethod.GeneralSpecCase
          A concrete wrapper class to JmlGeneralSpecCase for conjoining multiple specification clauses in a specification case.
protected static class TransMethod.SpecCase
          An abstract superclass for conjoining multiple specification clauses, such as requires and ensures clauses, in a specification case.
protected static class TransMethod.SpecCaseCollector
          A class for collecting all specification cases from a desugared method specification.
 
Field Summary
protected  JmlMethodSpecification desugaredSpec
          desugared specification of the target method to be translated
protected  boolean genSpecTestFile
          True if we are generating a test wrapper for a spec file (and we do not have the original source).
protected  JmlMethodDeclaration methodDecl
          target method to be transformed.
protected  List newFields
          newly created fields (as the result of translation) that need be added to the target class, e.g., old and precondition variables
protected  List newMethods
          newly created methods (as the result of translation) that need be added to the target class
private  String stackVar
           
protected  JmlTypeDeclaration typeDecl
          Target type declaration whose methods are to be translated.
protected  VarGenerator varGen
          for generating fresh variables needed in the generated Java code
 
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
TransMethod(JmlTypeDeclaration typeDecl, VarGenerator varGen)
          Constructs a new TransMethod object.
 
Method Summary
protected  TransPostcondition createPostconditionTranslator(VarGenerator postVarGen, RacContext ctx, VarGenerator preVarGen, boolean isStatic, JExpression pred, String var)
          Creates an appropriate postcondition translator.
protected  PreValueVars genAssertionMethods()
          Generates pre/postcondition check methods.
protected  JStatement[] genDelegatedMethod()
          Generates a method body for a non-abstract method that does not have an implementation; it is used to generate test fixtures for specification files in the absence of .java implementations.
protected  void genStackMethod(PreValueVars vars)
          Generates a private stack field declaration and a pair of push and pop methods.
protected  void genWrapperMethod()
          Renames the original method and generate a wrapper method that calls the original method wrapped with pre and postcondition checking.
 boolean hasNewFields()
          Returns true if any new field declarations has been generated as the result of translation.
 boolean hasNewMethods()
          Returns true if any new method declarations has been generated as the result of translation.
private  boolean methodHasRealExplicitSpecs()
           
protected  String methodName()
          Returns the name of the targe method declaration being translated.
private  boolean methodReturnTypeHasExplicitNullityModifiers()
           
 List newFields()
          Returns a list of new field declarations created by this translation, which need be added to the target class or interface.
 List newMethods()
          Returns a list of new method declaratons created by this transformation, and need be added to the target class or instance.
private  boolean paramsHaveExplicitNullityModifiers()
           
 void perform(JmlMethodDeclaration methodDecl)
          Peforms translation leaving the results in appropriate instance variables.
protected  JExpression postNonNullAnnotation()
          Returns an expression conjoinable to the normal postcondition, that checks the non_null annotation of the method declaration.
protected  JExpression preNonNullAnnotations()
          Composes the (implicit or explicit) non_null annotations of formal parameters, if any, into a JML expression and return it.
private  JExpression preNonNullAnnotationsDefaultToTrueExpr()
           
protected  List translateForAllVarDecl(JmlSpecVarDecl varDecl, VarGenerator varGen)
          Translates the given forall variable declarations.
protected  List translateLetVarDecl(JmlSpecVarDecl varDecl, VarGenerator varGen)
          Translates the given old variable declarations.
protected  RacNode translateSignalsClause(VarGenerator varGen, VarGenerator oldVarGen, JmlSignalsClause sigClause, String preVar, RacNode stmt, List oldExprs)
          Translates the given signals clause.
protected  List translateSpecVarDecls(JmlSpecVarDecl[] varDecls, VarGenerator varGen)
          Translates specification variable declarations.
 
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

protected boolean genSpecTestFile
True if we are generating a test wrapper for a spec file (and we do not have the original source).


typeDecl

protected final JmlTypeDeclaration typeDecl
Target type declaration whose methods are to be translated.

 protected invariant typeDecl != null;
 


methodDecl

protected JmlMethodDeclaration methodDecl
target method to be transformed.

 protected invariant methodDecl != null ==>
   typeDecl.methods().contains(methodDecl);
 


newFields

protected List newFields
newly created fields (as the result of translation) that need be added to the target class, e.g., old and precondition variables


newMethods

protected List newMethods
newly created methods (as the result of translation) that need be added to the target class


desugaredSpec

protected JmlMethodSpecification desugaredSpec
desugared specification of the target method to be translated


varGen

protected VarGenerator varGen
for generating fresh variables needed in the generated Java code


stackVar

private String stackVar
Constructor Detail

TransMethod

public TransMethod(JmlTypeDeclaration typeDecl,
                   VarGenerator varGen)
Constructs a new TransMethod object.

Parameters:
typeDecl - target type declaration whose methods are to be translated.
varGen - variable name generator

 requires typeDecl != null && varGen != null;
 
Method Detail

hasNewFields

public boolean hasNewFields()
Returns true if any new field declarations has been generated as the result of translation.

 ensures  \result == newFields.size() > 0;
 


hasNewMethods

public boolean hasNewMethods()
Returns true if any new method declarations has been generated as the result of translation.

 ensures  \result == newMethods.size() > 0;
 


newFields

public List newFields()
Returns a list of new field declarations created by this translation, which need be added to the target class or interface.

 ensures  \result != null && (\forall Object o; \result.contains(o);
   (o instanceof String) && 
   (* o has the form: "[static] T v = init;\n" *));
 


newMethods

public List newMethods()
Returns a list of new method declaratons created by this transformation, and need be added to the target class or instance.

 ensures  \result != null && (\forall Object o; \result.contains(o);
   (o instanceof JmlMethodDeclaration));
 


perform

public void perform(JmlMethodDeclaration methodDecl)
Peforms translation leaving the results in appropriate instance variables.

Parameters:
methodDecl - method to translate

 requires methodDecl != null && typeDecl.methods().contains(methodDecl);
 assignable newMethods, newFields, this.methodDecl, desugaredSpec;
 assignable stackVar;
 

genAssertionMethods

protected PreValueVars genAssertionMethods()
Generates pre/postcondition check methods. The generated methods and any fields (generated as side-effects) are added to the instance fields newMethods and newFields respectively. Returned is the set of (generated) private fields that need to be saved before, and restored after the execution of the method body, due to the possiblity of recursive method calls.

 requires (* desugaredSpec has desugared method spec *);
 //assignable newMethods, newFields, stackVar;
 ensures \result != null;
 


createPostconditionTranslator

protected TransPostcondition createPostconditionTranslator(VarGenerator postVarGen,
                                                           RacContext ctx,
                                                           VarGenerator preVarGen,
                                                           boolean isStatic,
                                                           JExpression pred,
                                                           String var)
Creates an appropriate postcondition translator. This is a hook method for subclasses to override to use different translators.


translateSpecVarDecls

protected List translateSpecVarDecls(JmlSpecVarDecl[] varDecls,
                                     VarGenerator varGen)
Translates specification variable declarations. Initializers are translated and returned with their new private field declarations. The caller is responsible for properly declaring the fields for the specification variables and execute the translated initializers in the appropriate place, e.g., in the method prolog.

 requires varDecls != null && varGen != null;
 ensures \fresh(\result) && (\forall Object o; \result.contains(o);
         o instanceof RacNode);
 

Parameters:
varDecls - declarations to be translated
varGen - variable generator for fresh variable names
Returns:
list of RacNodes, representing translated initializers with the corresponding new field declarations. The field declarations are piggybacked in the name fields of nodes.
See Also:
JMLRacValue

translateLetVarDecl

protected List translateLetVarDecl(JmlSpecVarDecl varDecl,
                                   VarGenerator varGen)
Translates the given old variable declarations. The initializers are translated and and returned with new instance variable declarations. The caller is responsible for properly declaring the new instance variables and execute the code to stores the values of initializers to the new fields.

 requires varDecl != null && varGen != null;
 ensures \fresh(\result) && (\forall Object o; \result.contains(o);
         o instanceof RacNode);
 

Parameters:
varDecl - declaration to be translated
varGen - variable generator for fresh variable names
Returns:
list of RacNodes representing translated code with the new instance field declarations. The field declarations are piggybacked in the name fields of RacNode.
See Also:
JMLRacValue

translateForAllVarDecl

protected List translateForAllVarDecl(JmlSpecVarDecl varDecl,
                                      VarGenerator varGen)
Translates the given forall variable declarations. They are translated into the non-executable values, and and returned with their corresponding instance variable declarations. The caller is responsible for properly declaring the instance variables and execute the code stores non-executable values to the fields.

 requires varDecl != null && varGen != null;
 ensures \fresh(\result) && (\forall Object o; \result.contains(o);
         o instanceof RacNode);
 

Parameters:
varDecl - declaration to be translated
varGen - variable generator for fresh variable names
Returns:
list of RacNodes representing translated code with the corresponding instance field declarations. The field declarations are piggybacked in the name fields of RacNode.
See Also:
JMLRacValue

translateSignalsClause

protected RacNode translateSignalsClause(VarGenerator varGen,
                                         VarGenerator oldVarGen,
                                         JmlSignalsClause sigClause,
                                         String preVar,
                                         RacNode stmt,
                                         List oldExprs)
Translates the given signals clause. The overall translation rule for exceptional postconditions is roughly defined as follows.
  [[signals (Ei ei) Pi]] =
    if (e instanceof Ei) {
       Ei ei = (Ei) e;
       boolean vi = false;
       [[Pi, vi]]
       b = b && vi;
    }
    check(b);
    if (e instanceof java.lang.RuntimeException)
       throw (java.lang.RuntimeException) e;
    else if (e instanceof java.lang.Error)
       throw (java.lang.Error) e;
    if (e instanceof CEi)
       throw (CEi) e;
 
where the variable e refers to actual exceptions thrown and b conjoins the results of evaluating all exceptional predicates. Both variables are defined in the body of exceptional postcondition checking method. If the exceptional postcondition is satisfied, the original exception is rethrown at the end; CEi denotes a checked exception that is listed in the method declaration.

This method method produces the first if statement (of the translation rule) corresponding to the given signals clause. The method accumulates the generated if statement by appending it to the argument stmt. The accumulated if statements is is returned as the result. The method also accumulates the translated old expressions appearing in the given signals clause to the argument oldExprs. For the translation, the method uses the variable generator varGen to generate fresh variables and the variable generator oldVarGen for fresh old variables.

Parameters:
varGen - variable generator for fresh variables
oldVarGen - variable generator for old variables
sigClause - the signals clause to translate
preVar - precondition variable
stmt - accumlated result of signals clauses translation
oldExprs - old expressions accumulated so far
See Also:

 requires varGen != null && oldVarGen != null && sigClause != null
   && preVar != null && oldExprs != null;
 modifies oldExprs.theList;
 ensures \result != null;
 

genWrapperMethod

protected void genWrapperMethod()
Renames the original method and generate a wrapper method that calls the original method wrapped with pre and postcondition checking. The body of the wrapper method looks like the following.
 T m(T1 x1, ..., Tn xn) {
   checkPre$m(x1, ..., xn);
   T r = init_T;
   try {
     r = orig$m(x1, ..., xn);
   }
   catch (Exception e) {
     checkExcept$m(x1, ..., xn, e);
   }
   checkPost$m(x1, ..., xn, r);
 }
 


genDelegatedMethod

protected JStatement[] genDelegatedMethod()
Generates a method body for a non-abstract method that does not have an implementation; it is used to generate test fixtures for specification files in the absence of .java implementations.


genStackMethod

protected void genStackMethod(PreValueVars vars)
Generates a private stack field declaration and a pair of push and pop methods. The stack is used to save the pre-state values such as preconditions, old variables, and old expressions into, and restore them from. The reason is to pass correct pre-state values to the post-state assertion check methods such as the postcondition check method in the presence of recursive method calls. The generated stack field and methods are added to the type declaration being translated. The code has the following form.
 private [static] Stack var = new Stack();
 private [static] void saveTo$var() {
   Object val[] = new Object[n];
   val[1] = preVar1;
   ...
   val[n] = preVarn;
   var.push(val);
 }
 private [static] void restoreFrom$var() {
   Object val[] = (Object[]) var.pop();
   preVar1 = val[1];
   ...
   preVarn = val[n];
 }
 


methodReturnTypeHasExplicitNullityModifiers

private boolean methodReturnTypeHasExplicitNullityModifiers()

paramsHaveExplicitNullityModifiers

private boolean paramsHaveExplicitNullityModifiers()

preNonNullAnnotationsDefaultToTrueExpr

private JExpression preNonNullAnnotationsDefaultToTrueExpr()

preNonNullAnnotations

protected JExpression preNonNullAnnotations()
Composes the (implicit or explicit) non_null annotations of formal parameters, if any, into a JML expression and return it. If all parameters are nullable then, the method returns null.

 ensures (* \result may be null *);
 


postNonNullAnnotation

protected JExpression postNonNullAnnotation()
Returns an expression conjoinable to the normal postcondition, that checks the non_null annotation of the method declaration. If the method declaration is nullable then null is returned.


methodHasRealExplicitSpecs

private boolean methodHasRealExplicitSpecs()
Returns:
true iff methodDecl has explicit spec cases at least one of which is not a redundant spec case (e.g. imples_that introduces a redundant spec case.

methodName

protected String methodName()
Returns the name of the targe method declaration being translated.


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.