Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.checker
Interface Constants

All Superinterfaces:
Constants, Constants
All Known Subinterfaces:
RacConstants, RacVisitor
All Known Implementing Classes:
CTypeType, JConstructorDeclarationWrapper, JFieldDeclarationWrapper, JInterfaceDeclarationWrapper, JMethodDeclarationWrapper, JmlAbstractVisitor, JmlAccumSubclassingInfo, JmlBinaryArithmeticExpressionHelper, JmlCompilationUnitContext, JmlContext, JmlExpression, JmlMemberAccess, JmlNode, JmlNumericType, JmlRelationalExpression, JmlSigBinaryMethod, JmlSourceClass, JmlSourceField, JmlSourceMethod, JmlStdType, JmlStoreRefKeyword, JmlUnaryExpression, JStatementWrapper, Main.JmlGenerateAssertionTask, NNull, NonNullStatistics, PreValueVars, QInterval, QSet, RacAbstractVisitor, RacPrettyPrinter, SpecWriter, TestJmlParser, Translator, TransUtils, VarGenerator
public interface Constants
extends Constants

Defines all additional constants shared by JML package files.

Field Summary
static int ACC2_RAC_METHOD
           
static long ACC_CODE
           
static long ACC_CODE_BIGINT_MATH
           
static long ACC_CODE_JAVA_MATH
           
static long ACC_CODE_SAFE_MATH
           
static long ACC_GHOST
           
static long ACC_HELPER
           
static long ACC_INSTANCE
           
static long ACC_MODEL
           
static long ACC_MONITORED
           
static long ACC_NON_NULL
           
static long ACC_NON_NULL_BY_DEFAULT
           
static long ACC_NULLABLE
           
static long ACC_NULLABLE_BY_DEFAULT
           
static long ACC_QUERY
           
static long ACC_SECRET
           
static long ACC_SPEC_BIGINT_MATH
           
static long ACC_SPEC_JAVA_MATH
           
static long ACC_SPEC_PROTECTED
           
static long ACC_SPEC_PUBLIC
           
static long ACC_SPEC_SAFE_MATH
           
static long ACC_UNINITIALIZED
           
static long[] ACCESS_FLAG_ARRAY
          These arrays are used to map flags to names for pretty printing and error messages and to issue style warnings for modifiers out of order.
static String[] ACCESS_FLAG_NAMES
          These arrays are used to map flags to names for pretty printing and error messages and to issue style warnings for modifiers out of order.
static byte AMID_BIGINT_MATH
           
static int EVERYTHING
           
static String JML_JMLObjectSet
           
static int NOT_SPECIFIED
           
static int NOTHING
           
static int OPE_BACKWARD_IMPLIES
           
static int OPE_EQUIV
           
static int OPE_EXISTS
           
static int OPE_FORALL
           
static int OPE_IMPLIES
           
static int OPE_L_ARROW
           
static int OPE_MAX
           
static int OPE_MIN
           
static int OPE_NOT_EQUIV
           
static int OPE_NUM_OF
           
static int OPE_PRODUCT
           
static int OPE_R_ARROW
           
static int OPE_SUBTYPE
           
static int OPE_SUM
           
static int SAME
           
static int TID_BIGINT
           
static int TID_REAL
           
static int TID_TYPE
           
static String TN_JMLOBJECTSET
          Used in typechecking set comprehension expressions.
static String TN_JMLTYPE
          Used in typechecking set comprehension expressions.
static String TN_JMLVALUESET
          Used in typechecking set comprehension expressions.
 
Fields inherited from interface org.multijava.mjc.Constants
ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, 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, 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_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
 

Field Detail

TID_TYPE

public static final int TID_TYPE

TID_BIGINT

public static final int TID_BIGINT

TID_REAL

public static final int TID_REAL

AMID_BIGINT_MATH

public static final byte AMID_BIGINT_MATH

JML_JMLObjectSet

public static final String JML_JMLObjectSet

ACC_MODEL

public static final long ACC_MODEL

ACC_INSTANCE

public static final long ACC_INSTANCE

ACC_SPEC_PUBLIC

public static final long ACC_SPEC_PUBLIC

ACC_SPEC_PROTECTED

public static final long ACC_SPEC_PROTECTED

ACC_GHOST

public static final long ACC_GHOST

ACC_MONITORED

public static final long ACC_MONITORED

ACC_UNINITIALIZED

public static final long ACC_UNINITIALIZED

ACC_NON_NULL

public static final long ACC_NON_NULL

ACC_HELPER

public static final long ACC_HELPER

ACC_CODE_JAVA_MATH

public static final long ACC_CODE_JAVA_MATH

ACC_CODE_SAFE_MATH

public static final long ACC_CODE_SAFE_MATH

ACC_CODE_BIGINT_MATH

public static final long ACC_CODE_BIGINT_MATH

ACC_SPEC_JAVA_MATH

public static final long ACC_SPEC_JAVA_MATH

ACC_SPEC_SAFE_MATH

public static final long ACC_SPEC_SAFE_MATH

ACC_SPEC_BIGINT_MATH

public static final long ACC_SPEC_BIGINT_MATH

ACC_NULLABLE

public static final long ACC_NULLABLE

ACC_NULLABLE_BY_DEFAULT

public static final long ACC_NULLABLE_BY_DEFAULT

ACC_NON_NULL_BY_DEFAULT

public static final long ACC_NON_NULL_BY_DEFAULT

ACC2_RAC_METHOD

public static final int ACC2_RAC_METHOD

ACC_QUERY

public static final long ACC_QUERY

ACC_SECRET

public static final long ACC_SECRET

ACC_CODE

public static final long ACC_CODE

ACCESS_FLAG_ARRAY

public static final long[] ACCESS_FLAG_ARRAY
These arrays are used to map flags to names for pretty printing and error messages and to issue style warnings for modifiers out of order.

See Also:
ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES

ACCESS_FLAG_NAMES

public static final String[] ACCESS_FLAG_NAMES
These arrays are used to map flags to names for pretty printing and error messages and to issue style warnings for modifiers out of order.

See Also:
ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES

OPE_L_ARROW

public static final int OPE_L_ARROW

OPE_R_ARROW

public static final int OPE_R_ARROW

OPE_EQUIV

public static final int OPE_EQUIV

OPE_NOT_EQUIV

public static final int OPE_NOT_EQUIV

OPE_IMPLIES

public static final int OPE_IMPLIES

OPE_BACKWARD_IMPLIES

public static final int OPE_BACKWARD_IMPLIES

OPE_FORALL

public static final int OPE_FORALL

OPE_EXISTS

public static final int OPE_EXISTS

OPE_MAX

public static final int OPE_MAX

OPE_MIN

public static final int OPE_MIN

OPE_NUM_OF

public static final int OPE_NUM_OF

OPE_PRODUCT

public static final int OPE_PRODUCT

OPE_SUM

public static final int OPE_SUM

OPE_SUBTYPE

public static final int OPE_SUBTYPE

TN_JMLOBJECTSET

public static final String TN_JMLOBJECTSET
Used in typechecking set comprehension expressions.

TN_JMLVALUESET

public static final String TN_JMLVALUESET
Used in typechecking set comprehension expressions.

TN_JMLTYPE

public static final String TN_JMLTYPE
Used in typechecking set comprehension expressions.

NOTHING

public static final int NOTHING

EVERYTHING

public static final int EVERYTHING

NOT_SPECIFIED

public static final int NOT_SPECIFIED

SAME

public static final int SAME
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
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.