org.jmlspecs.checker
Class NonNullStatistics
java.lang.Object
org.jmlspecs.checker.NonNullStatistics
- All Implemented Interfaces:
- Constants, Constants, Constants
- public class NonNullStatistics
- extends Object
- implements Constants
| 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 |
|
Method Summary |
private static void |
abortCurrentSpecCase(String fn)
|
static void |
checkExpression(JExpression j,
JmlContext context,
String fn,
int clause,
boolean ifNot,
boolean ifInvStatic)
|
static void |
checkSpecBody(JmlSpecBody jsb,
JmlContext context,
String fn)
|
static void |
checkSpecBodyClause(JmlSpecBodyClause jsbc,
JmlContext context,
String fn)
|
static void |
checkSpecCase(JmlSpecCase jsc,
JmlContext context,
String fn,
boolean fromHeavy)
|
static void |
checkSpecification(JmlMethodDeclaration jmd,
Object[] jscArr,
JmlContext context,
String fn)
|
static boolean |
getSuperMethod(JmlSourceMethod sm)
|
static boolean |
getSuperParam(JmlSourceMethod sm,
int i)
|
static Vector |
getSuperSpec(JmlMethodDeclaration jmd,
String key)
|
private static void |
handleEqualityExpression(JmlEqualityExpression je,
JmlContext context,
String fn,
int clause,
boolean ifNot,
boolean ifInvStatic)
|
private static void |
handleFreshExpression(JmlFreshExpression jf,
JmlContext context,
int clause,
String fn)
|
private static void |
handleInstanceofExpression(JInstanceofExpression j,
JmlContext context,
String fn,
int clause,
boolean ifInvStatic)
|
static void |
handleMethodDeclaration(JmlMethodDeclaration jmd,
JMethodDeclaration delegee,
String fileName,
JmlContext context)
|
private static void |
handleNNElementExpr(JmlNonNullElementsExpression j,
JmlContext context,
String fn,
int clause,
boolean ifInvStatic)
|
static void |
hmNonnullPut(String key,
String value)
|
static void |
outPutStat()
|
private static void |
putHmSpecCase(String key)
|
static void |
setCurrClass(String classIdent)
|
static void |
setCurrMethod(String methodIdent)
|
| Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
ifDiverges
private static boolean ifDiverges
isLiteralFalse
private static boolean isLiteralFalse
inExceptionalSpec
private static boolean inExceptionalSpec
falseCount
private static int falseCount
intConstructor
private static int intConstructor
intSpecCase
private static int intSpecCase
currMethod
private static String currMethod
currClass
private static String currClass
stackValue
private static Stack stackValue
stackSpecCase
private static Stack stackSpecCase
strArgs
private static String[] strArgs
hmSpecCase
private static HashMap hmSpecCase
ifFalse
public static boolean ifFalse
hmNnStat
public static HashMap hmNnStat
hmArgs
public static HashMap hmArgs
hmNonnull
public static HashMap hmNonnull
hmSuperSpec
public static HashMap hmSuperSpec
NonNullStatistics
public NonNullStatistics(File[] files)
outPutStat
public static void outPutStat()
checkExpression
public static void checkExpression(JExpression j,
JmlContext context,
String fn,
int clause,
boolean ifNot,
boolean ifInvStatic)
throws PositionedError
- Throws:
PositionedError
checkSpecification
public static void checkSpecification(JmlMethodDeclaration jmd,
Object[] jscArr,
JmlContext context,
String fn)
throws PositionedError
- Throws:
PositionedError
checkSpecCase
public static void checkSpecCase(JmlSpecCase jsc,
JmlContext context,
String fn,
boolean fromHeavy)
throws PositionedError
- Throws:
PositionedError
checkSpecBody
public static void checkSpecBody(JmlSpecBody jsb,
JmlContext context,
String fn)
throws PositionedError
- Throws:
PositionedError
checkSpecBodyClause
public static void checkSpecBodyClause(JmlSpecBodyClause jsbc,
JmlContext context,
String fn)
throws PositionedError
- Throws:
PositionedError
handleNNElementExpr
private static void handleNNElementExpr(JmlNonNullElementsExpression j,
JmlContext context,
String fn,
int clause,
boolean ifInvStatic)
handleInstanceofExpression
private static void handleInstanceofExpression(JInstanceofExpression j,
JmlContext context,
String fn,
int clause,
boolean ifInvStatic)
handleEqualityExpression
private static void handleEqualityExpression(JmlEqualityExpression je,
JmlContext context,
String fn,
int clause,
boolean ifNot,
boolean ifInvStatic)
handleFreshExpression
private static void handleFreshExpression(JmlFreshExpression jf,
JmlContext context,
int clause,
String fn)
handleMethodDeclaration
public static void handleMethodDeclaration(JmlMethodDeclaration jmd,
JMethodDeclaration delegee,
String fileName,
JmlContext context)
setCurrMethod
public static void setCurrMethod(String methodIdent)
setCurrClass
public static void setCurrClass(String classIdent)
getSuperMethod
public static boolean getSuperMethod(JmlSourceMethod sm)
getSuperParam
public static boolean getSuperParam(JmlSourceMethod sm,
int i)
throws PositionedError
- Throws:
PositionedError
getSuperSpec
public static Vector getSuperSpec(JmlMethodDeclaration jmd,
String key)
putHmSpecCase
private static void putHmSpecCase(String key)
abortCurrentSpecCase
private static void abortCurrentSpecCase(String fn)
hmNonnullPut
public static void hmNonnullPut(String key,
String value)
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.