ESC/Java version 1.2.4, 27 September 2001 StringSet ... StringSet: StringSet() ... [0.191 s] passed StringSet: insert(java.lang.String) ... ------------------------------------------------------------------------ StringSet.java:25: Warning: Possible null dereference (Null) if (getIndex (s) < 0) els.add (s); ^ Execution trace information: Executed then branch in "StringSet.java", line 25, col 23. ------------------------------------------------------------------------ StringSet.java:25: Warning: Precondition possibly not established (Pre) if (getIndex (s) < 0) els.add (s); ^ Associated declaration is "/net/af10/evans/escjava/escjava/lib/specs/java/util/Collection.spec", line 217, col 8: //@ requires !containsNull ==> o!=null ^ Execution trace information: Executed then branch in "StringSet.java", line 25, col 23. ------------------------------------------------------------------------ StringSet.java:25: Warning: Precondition possibly not established (Pre) if (getIndex (s) < 0) els.add (s); ^ Associated declaration is "/net/af10/evans/escjava/escjava/lib/specs/java/util/Collection.spec", line 218, col 8: //@ requires \typeof(o) <: elementType || o==null ^ Execution trace information: Executed then branch in "StringSet.java", line 25, col 23. ------------------------------------------------------------------------ [0.178 s] failed StringSet: remove(java.lang.String) ... ------------------------------------------------------------------------ StringSet.java:33: Warning: Possible null dereference (Null) els.removeElementAt (i); ^ Execution trace information: Executed else branch in "StringSet.java", line 32, col 1. ------------------------------------------------------------------------ StringSet.java:33: Warning: Precondition possibly not established (Pre) els.removeElementAt (i); ^ Associated declaration is "/net/af10/evans/escjava/escjava/lib/specs/java/util/Vector.spec", line 569, col 8: //@ requires index < elementCount ; ^ Execution trace information: Executed else branch in "StringSet.java", line 32, col 1. ------------------------------------------------------------------------ [0.192 s] failed StringSet: isIn(java.lang.String) ... [0.019 s] passed StringSet: getIndex(java.lang.String) ... ------------------------------------------------------------------------ StringSet.java:42: Warning: Possible null dereference (Null) for (int i = 0; i < els.size (); i++) { ^ Execution trace information: Reached top of loop after 0 iterations in "StringSet.java", line 42, col 1. ------------------------------------------------------------------------ StringSet.java:43: Warning: Possible null dereference (Null) if (s.equals (els.elementAt (i))) { ^ Execution trace information: Reached top of loop after 0 iterations in "StringSet.java", line 42, col 1. ------------------------------------------------------------------------ [0.193 s] failed StringSet: size() ... ------------------------------------------------------------------------ StringSet.java:53: Warning: Possible null dereference (Null) return els.size (); ^ ------------------------------------------------------------------------ [0.05 s] failed [1.737 s total] 8 warnings