org.jmlspecs.jmlrac
Class TransMethod

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.jmlrac.TransUtils
          org.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

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;
 

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.