JML

org.jmlspecs.checker
Class NonNullStatistics

java.lang.Object
  extended byorg.jmlspecs.checker.NonNullStatistics
All Implemented Interfaces:
Constants, Constants, Constants

public class NonNullStatistics
extends Object
implements Constants


Field Summary
private static String currClass
           
private static String currMethod
           
private static int falseCount
           
static HashMap hmArgs
           
static HashMap hmNnStat
           
static HashMap hmNonnull
           
private static HashMap hmSpecCase
           
static HashMap hmSuperSpec
           
private static boolean ifDiverges
           
static boolean ifFalse
           
private static boolean inExceptionalSpec
           
private static int intConstructor
           
private static int intSpecCase
           
private static boolean isLiteralFalse
           
private static Stack stackSpecCase
           
private static Stack stackValue
           
private static String[] strArgs
           
 
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
NonNullStatistics(File[] files)
           
 
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
 

Field Detail

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
Constructor Detail

NonNullStatistics

public NonNullStatistics(File[] files)
Method Detail

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

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.