| method | void process(String, String[]) |
| pre | sParam != null |
| pre | (soft) this.myParser.sNetworkName != null |
| pre | (soft) init'ed(this.myParser.stringConverter) |
| pre | (soft) this.myParser != null |
| pre | (soft) this.myParser...myCallbackManager != null |
| pre | (soft) this.myParser...myCallbackManager. callbackHash != null |
| pre | (soft) this.myParser.cMyself != null |
| pre | (soft) this.myParser.cMyself.sNickname != null |
| pre | (soft) this.myParser.h005Info != null |
| pre | (soft) this.myParser.hChanModesBool != null |
| pre | (soft) this.myParser.hChanModesOther != null |
| pre | (soft) this.myParser.hChanPrefix != null |
| pre | (soft) this.myParser.hClientList != null |
| pre | (soft) this.myParser.hPrefixMap != null |
| pre | (soft) this.myParser.hPrefixModes != null |
| pre | (soft) this.myParser.hUserModes != null |
| pre | (soft) init'ed(this.myParser.lastLine) |
| pre | (soft) this.myParser.myCallbackManager != null |
| pre | (soft) this.myParser.myCallbackManager. callbackHash != null |
| pre | (soft) this.myParser.myProcessingManager != null |
| pre | (soft) this.myParser.myProcessingManager.myParser != null |
| pre | (soft) this.myParser.myProcessingManager. processHash != null |
| pre | (soft) token != null |
| pre | (soft) token.length in {4, 7..232-1} |
| pre | (soft) token[...] != null |
| pre | (soft) token[3] != null |
| pre | (soft) token[4] != null |
| pre | (soft) token[5] != null |
| pre | (soft) token[6] != null |
| presumption | java.lang.Integer:parseInt(...)@96 <= 232-2 |
| post | java.lang.StringBuilder:toString(...)._tainted == 0 |
| post | possibly_updated(this.myParser.nNextKeyCMBool) |
| post | possibly_updated(this.myParser.nNextKeyPrefix) |
| post | possibly_updated(this.myParser.nNextKeyUser) |
| post | this.myParser.sNetworkName != null |
| post | init'ed(this.myParser.stringConverter) |
| post | init'ed(new IRCStringConverter(getIRCStringConverte r#1) num objects) |
| post | new IRCStringConverter(getIRCStringConverter#1) num objects == 0 |
| post | init'ed(new IRCStringConverter(getIRCStringConverte r#1).limit) |
| post | init'ed(new IRCStringConverter(getIRCStringConverte r#1).lowercase) |
| post | init'ed(new IRCStringConverter(getIRCStringConverte r#1).uppercase) |
| post | new IRCStringConverter(updateCharArrays#1) num objects <= 232-4 |
| post | init'ed(new IRCStringConverter(updateCharArrays#1). limit) |
| post | init'ed(new IRCStringConverter(updateCharArrays#1). lowercase) |
| post | init'ed(new IRCStringConverter(updateCharArrays#1). uppercase) |
| post | init'ed(new char[](IRCStringConverter#1) num objects) |
| post | new char[](IRCStringConverter#1) num objects <= 232-4 |
| post | new char[](IRCStringConverter#1) num objects == 0 |
| post | init'ed(new char[](IRCStringConverter#1).length) |
| post | init'ed(new char[](IRCStringConverter#1)[...]) |
| post | init'ed(new char[](IRCStringConverter#2) num objects) |
| post | new char[](IRCStringConverter#2) num objects <= 232-4 |
| post | new char[](IRCStringConverter#2) num objects == 0 |
| post | init'ed(new char[](IRCStringConverter#2).length) |
| post | init'ed(new char[](IRCStringConverter#2)[...]) |
| unanalyzed | call on getIRCD |
| unanalyzed | call on getCallbackManager |
| unanalyzed | call on getCallbackType |
| unanalyzed | call on call |
| unanalyzed | call on java.util.Map:containsKey |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.lang.String:matches |
| unanalyzed | call on java.lang.String:equalsIgnoreCase |
| unanalyzed | call on java.lang.String:toLowerCase |
| unanalyzed | call on java.lang.RuntimeException |
| unanalyzed | call on java.util.Map:clear |
| unanalyzed | call on java.lang.Character:valueOf |
| unanalyzed | call on java.lang.String:length |
| unanalyzed | call on java.util.Map:put |
| unanalyzed | call on callDebugInfo |
| unanalyzed | call on java.lang.String:charAt |
| unanalyzed | call on java.lang.String:format |
| unanalyzed | call on java.lang.Integer:valueOf |
| unanalyzed | call on java.lang.Long:valueOf |
| unanalyzed | call on java.util.Map:size |
| unanalyzed | call on getNickname |
| unanalyzed | call on java.lang.String:toCharArray |
| unanalyzed | call on java.lang.String |
| unanalyzed | call on forceRemoveClient |
| unanalyzed | call on java.util.Map:remove |
| unanalyzed | call on java.lang.Boolean:valueOf |
| unanalyzed | call on java.lang.String:substring |
| unanalyzed | call on java.lang.String:split |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on java.lang.Character:toString |
| unanalyzed | call on java.lang.Byte:valueOf |
| unanalyzed | call on java.util.Hashtable:containsKey |
| unanalyzed | call on java.util.Hashtable:get |
| unanalyzed | call on java.lang.Exception |
| unanalyzed | call on java.lang.Object:getClass |
| unanalyzed | call on java.lang.Class:getPackage |
| unanalyzed | call on java.lang.Package:getName |
| unanalyzed | call on java.lang.Class:getName |
| unanalyzed | call on doDebug |
| unanalyzed | call on java.util.Hashtable:remove |
| unanalyzed | call on java.util.Hashtable:put |
| test_vector | token.length: {4}, {7..232-1} |
| test_vector | java.lang.String:equals(...)@37: {0}, {1} |
| test_vector | java.lang.String:equals(...)@39: {0}, {1} |
| test_vector | java.lang.String:equals(...)@52: {0}, {1} |
| test_vector | java.lang.String:equals(...)@62: {0}, {1} |
| test_vector | java.lang.String:equals(...)@65: {0}, {1} |
| test_vector | java.lang.String:equals(...)@83: {0}, {1} |
| test_vector | java.lang.String:equals(...)@85: {0}, {1} |
| test_vector | java.lang.String:equals(...)@87: {0}, {1} |
| test_vector | java.lang.String:equals(...)@89: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@67: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@69: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@71: {1}, {0} |
| test_vector | java.util.Map:size(...)@2007: {-231..0, 2..232-1}, {1} |