JML

org.jmlspecs.jmlrac
Class TransUtils

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

public abstract class TransUtils
extends Utils
implements RacConstants

A utility class for translating JML annotated Java classes into RAC-enabled classes.

Version:
$Revision: 1.48 $
Author:
Yoonsik Cheon

Field Summary
private static HashSet excludedFromInheritance
          The set of types to be excluded, for specification inheritance, from making non-reflective calls to.
private static HashSet includedInInheritance
          The set of types to which non-reflective calls are made for specification inheritance.
private static String[] nonReflectiveRefinementTypes
          An array of type names to which non-reflective calls would be made for specification inheritance.
private static String[] nonReflectiveTypes
          An array of type names to which non-reflective calls would be made for specification inheritance.
static JTypeDeclarationType typeDecl
           
private static Map wrapperClasses
          Mapping from primitive types to their wrapper classes
 
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
TransUtils()
           
 
Method Summary
static String[] applyBigintBinOperator(String binOp)
          Returns a two-item string array which has the two parts in biginteger operation formula mapping the given binary operator binOp
static String[] applyBigintCast(CType typeDest, CType typeSource, String strTypeDest)
          Returns a two-item string array which has the two parts in biginteger operation formula mapping the given destination type typeDest and source type typeSource in cast expression. the parm strTypeDest is needed for in different class, the method "toString" is difined differently.
static String[] applyBigintToNumber(CType typeSource, CType typeNumber)
          Returns a two-item string array which has the two parts in biginteger operation formula mapping the given source type typeSource which is a \bigint or numerical type to destination number type typeNumber which is a numerical type.cast expression. the parm strTypeDest is needed for in different class, the method "toString" is difined differently.
static String applyBigintUnOperator(String unaryOp)
          Returns a string is the end part in biginteger operation formula mapping the given unary operator unaryOp
static String applyUnaryPromoteExpression(CType typeSelf, CType typeExpr, String strExpr)
          Returns a string that represents the Java code that casts strExpr of type typeExpr to typeSelf.
static boolean beingTested(CClass clazz)
          Returns true if the class named is a spec file for which a test wrapper is being created.
static String[] createBigintConvertionAssertion(CType typeSource, CType typeDest)
          Returns a two-item string array which has the two parts in out of range assertion code for translating \bigint to number.
static String defaultValue(CType type)
          Returns a string representation of the default value of the given type, type.
static String dynamicCallName(CClass clazz)
          Returns the name to be used to make dynamic calls to assertion check methods of the given class.
static String evalOldName(String cls, boolean isStatic)
          Returns the name of an old-expression evaluation method for the class named cls.
static String evalOldName(JmlTypeDeclaration tdecl, boolean isStatic)
          Returns the name of an old-expression evaluation method for the type declaration.
static String evalOldName(CClass clazz, boolean isStatic)
           
static String evalOldName(CClassType ctype, boolean isStatic)
           
static boolean excludedFromInheritance(CClass clazz)
          Returns true if the given type, clazz, is excluded from the set of types from which specifications can be inherited without using reflective method calls.
static int getTypeID(CType type)
           
private static void initIncludedInInheritance()
          Initializes the set of types to which non-reflective calls are made for specification inheritance.
static void initIncludedInInheritance(CClass cc)
           
static String invariantLikeName(String prefix, CClass clazz, boolean forStatic)
          Returns the name of invariant-like assertion check method.
static boolean isBigintArray(CType type)
          To check if the type is "\bigint[]"
static boolean isMain(JmlMethodDeclaration mdecl)
          Returns true if the argument is a main method declaration
static String modelPublicAccessorName(CMethod meth)
          Returns the name of the spec_public accessor for the method whose name is ident.
static String numberToBigint(String strVar, CType type)
          Returns a string that represents the Java code that convert the parm strVar to its corresponding value of BigInteger which is the other parm typ indicate the type of strVar.
static boolean specAccessorNeeded(long modifiers)
          Returns true if the modifiers indicate that we need to generate specification-only accessor method.
static String specPublicAccessorName(String ident)
          Returns the name of the spec_public accessor for the method whose name is ident.
static String subtypeConstraintName(String prefix, CClass clazz, boolean isWeakly)
          Returns the name of invariant-like assertion check method.
static String toPrintableString(char c)
          Returns a printable string representation for the given char value.
static String toString(double value)
          Returns the string representation of the given double value.
static String toString(float value)
          Returns the string representation of the given float value.
static String toString(CType value)
          Returns the string representation of the given type.
static String typeToClass(CType type)
          Returns the string representation of the wrapper class for the given type.
protected static String unwrapObject(CType type, String var)
          Returns a string representation of unwrapped value of var with respect to type type.
static boolean useReflection()
          Returns true if we use reflection for specification inheritance.
static String wrappedValue(CType type, String ident)
          Returns a string representation of a Java expression that denotes a wrapper object for the given variable, ident of type, type.
static String wrapValue(CType type, String var)
          Returns the string representation of wrapping the value of variable var of type type into an object.
 
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

typeDecl

public static JTypeDeclarationType typeDecl

excludedFromInheritance

private static HashSet excludedFromInheritance
The set of types to be excluded, for specification inheritance, from making non-reflective calls to.


includedInInheritance

private static HashSet includedInInheritance
The set of types to which non-reflective calls are made for specification inheritance. The set should contain only interface types from JDK., i.e., whose package names starting with java.


nonReflectiveTypes

private static final String[] nonReflectiveTypes
An array of type names to which non-reflective calls would be made for specification inheritance. This array should contain only interface types from JDK, e.g., those found in the directory JML2/specs/java.


nonReflectiveRefinementTypes

private static final String[] nonReflectiveRefinementTypes
An array of type names to which non-reflective calls would be made for specification inheritance. This array should contain only refinement types from JDK, e.g., those found in the directory JML2/specs/java.


wrapperClasses

private static Map wrapperClasses
Mapping from primitive types to their wrapper classes

Constructor Detail

TransUtils

public TransUtils()
Method Detail

specAccessorNeeded

public static boolean specAccessorNeeded(long modifiers)
Returns true if the modifiers indicate that we need to generate specification-only accessor method. The argument modifier is typically from a model field declaration.

 ensures \result == (hasFlag(modifiers, ACC_PRIVATE) &&
	    (hasFlag(modifiers, ACC_SPEC_PUBLIC) ||
	     hasFlag(modifiers, ACC_SPEC_PROTECTED)));
 


defaultValue

public static String defaultValue(CType type)
Returns a string representation of the default value of the given type, type. The defualt value is determined according to JLS 4.4.5, e.g., "false" for boolean.


wrappedValue

public static String wrappedValue(CType type,
                                  String ident)
Returns a string representation of a Java expression that denotes a wrapper object for the given variable, ident of type, type. E.g., "new Boolean(x)" if ident is "x" and type is boolean.


isMain

public static boolean isMain(JmlMethodDeclaration mdecl)
Returns true if the argument is a main method declaration


evalOldName

public static String evalOldName(String cls,
                                 boolean isStatic)
Returns the name of an old-expression evaluation method for the class named cls.

Parameters:
cls - class name
isStatic - static or instance method?

 requires cls != null;
 ensures \result != null;
 

evalOldName

public static String evalOldName(JmlTypeDeclaration tdecl,
                                 boolean isStatic)
Returns the name of an old-expression evaluation method for the type declaration.

Parameters:
tdecl - type declaration
isStatic - static or instance method?

 requires tdecl != null;
 ensures \result != null;
 

evalOldName

public static String evalOldName(CClassType ctype,
                                 boolean isStatic)

evalOldName

public static String evalOldName(CClass clazz,
                                 boolean isStatic)

invariantLikeName

public static String invariantLikeName(String prefix,
                                       CClass clazz,
                                       boolean forStatic)
Returns the name of invariant-like assertion check method.


subtypeConstraintName

public static String subtypeConstraintName(String prefix,
                                           CClass clazz,
                                           boolean isWeakly)
Returns the name of invariant-like assertion check method.


dynamicCallName

public static String dynamicCallName(CClass clazz)
Returns the name to be used to make dynamic calls to assertion check methods of the given class. The returned is the fully-qualified name of the given class. However, if the class is an interface, it is the surrogate class's fully-qualified name.


beingTested

public static boolean beingTested(CClass clazz)
Returns true if the class named is a spec file for which a test wrapper is being created.


typeToClass

public static String typeToClass(CType type)
Returns the string representation of the wrapper class for the given type. If the given type is a primitive type (e.g., int), the standard wrapper class (e.g., "java.lang.Integer.TYPE" is returned; otherwise, the type itself (e.g., type.toString() + ".class") is returned.

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

See Also:
wrapValue(CType,String)

unwrapObject

protected static String unwrapObject(CType type,
                                     String var)
Returns a string representation of unwrapped value of var with respect to type type. E.g., "((Integer)" + var + ").intValue()" if type is int.

See Also:
wrapValue(CType,String)

wrapValue

public static String wrapValue(CType type,
                               String var)
Returns the string representation of wrapping the value of variable var of type type into an object. E.g., "new java.lang.Integer(" + var + ")" for type int.

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

See Also:
unwrapObject(CType,String)

toString

public static String toString(double value)
Returns the string representation of the given double value. In particular, translates such special values as INFINITY, NaN, MIN_VALUE, and MAX_VALUE.


toString

public static String toString(float value)
Returns the string representation of the given float value. In particular, translates such special values as INFINITY, NaN, MIN_VALUE, and MAX_VALUE.


toString

public static String toString(CType value)
Returns the string representation of the given type. If the type is JmlStdType.TYPE, the result is "java.lang.Class"; otherwise it is value.toString().


getTypeID

public static int getTypeID(CType type)

toPrintableString

public static String toPrintableString(char c)
Returns a printable string representation for the given char value. E.g., "a" for 'a', "\\n" for '\n' and "\\u0000" for '\u0000'.


specPublicAccessorName

public static String specPublicAccessorName(String ident)
Returns the name of the spec_public accessor for the method whose name is ident.


modelPublicAccessorName

public static String modelPublicAccessorName(CMethod meth)
Returns the name of the spec_public accessor for the method whose name is ident.


useReflection

public static boolean useReflection()
Returns true if we use reflection for specification inheritance.


excludedFromInheritance

public static boolean excludedFromInheritance(CClass clazz)
Returns true if the given type, clazz, is excluded from the set of types from which specifications can be inherited without using reflective method calls. All types from JDK except for those listed in includedInInheritance are excluded. Also excluded are thise listed in excludedFromInheritance.

See Also:
excludedFromInheritance, includedInInheritance

initIncludedInInheritance

private static void initIncludedInInheritance()
Initializes the set of types to which non-reflective calls are made for specification inheritance. The set should contain only interface types from JDK., i.e., whose package names starting with java.

 assignable includedInInheritance;
 ensures includedInInheritance != null;
 

See Also:
includedInInheritance

initIncludedInInheritance

public static void initIncludedInInheritance(CClass cc)

applyBigintBinOperator

public static String[] applyBigintBinOperator(String binOp)
Returns a two-item string array which has the two parts in biginteger operation formula mapping the given binary operator binOp

See Also:
TransExpression.applyOperator(String v1, String v2, String binOp, CType type)

applyBigintUnOperator

public static String applyBigintUnOperator(String unaryOp)
Returns a string is the end part in biginteger operation formula mapping the given unary operator unaryOp

See Also:
TransExpression.applyOperator(String v, String unaryOp, CType type)

applyBigintCast

public static String[] applyBigintCast(CType typeDest,
                                       CType typeSource,
                                       String strTypeDest)
Returns a two-item string array which has the two parts in biginteger operation formula mapping the given destination type typeDest and source type typeSource in cast expression. the parm strTypeDest is needed for in different class, the method "toString" is difined differently.

See Also:
RacPrettyPrinter.toString(org.multijava.mjc.CType), TransExpression.toString(org.multijava.mjc.CType), TransExpression.applyCast(String v, CType typeDest, CType typeVar)

applyUnaryPromoteExpression

public static String applyUnaryPromoteExpression(CType typeSelf,
                                                 CType typeExpr,
                                                 String strExpr)
Returns a string that represents the Java code that casts strExpr of type typeExpr to typeSelf.

See Also:
TransExpression.visitUnaryPromoteExpression(org.multijava.mjc.JUnaryPromote)

numberToBigint

public static String numberToBigint(String strVar,
                                    CType type)
Returns a string that represents the Java code that convert the parm strVar to its corresponding value of BigInteger which is the other parm typ indicate the type of strVar.


applyBigintToNumber

public static String[] applyBigintToNumber(CType typeSource,
                                           CType typeNumber)
Returns a two-item string array which has the two parts in biginteger operation formula mapping the given source type typeSource which is a \bigint or numerical type to destination number type typeNumber which is a numerical type.cast expression. the parm strTypeDest is needed for in different class, the method "toString" is difined differently.

See Also:
TransExpression.applyArrayAccessExpression(java.lang.String, org.multijava.mjc.CType, org.multijava.mjc.CType), RacPrettyPrinter.visitArrayAccessExpression(org.multijava.mjc.JArrayAccessExpression)

createBigintConvertionAssertion

public static String[] createBigintConvertionAssertion(CType typeSource,
                                                       CType typeDest)
Returns a two-item string array which has the two parts in out of range assertion code for translating \bigint to number.

See Also:
TransExpression.applyArrayAccessExpression(java.lang.String, org.multijava.mjc.CType, org.multijava.mjc.CType), RacPrettyPrinter.visitArrayAccessExpression(org.multijava.mjc.JArrayAccessExpression)

isBigintArray

public static boolean isBigintArray(CType type)
To check if the type is "\bigint[]"


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.