| method | void process(String, String[]) |
| pre | token != null |
| pre | token.length >= 4 |
| pre | init'ed(token[3]) |
| pre | (soft) init'ed(this.myParser.me.nickname) |
| pre | (soft) init'ed(this.myParser.sThinkNickname) |
| pre | (soft) init'ed(this.myParser.stringConverter) |
| pre | (soft) init'ed(this.myParser.triedAlt) |
| pre | (soft) this.myParser != null |
| pre | (soft) this.myParser.cMyself != null |
| pre | (soft) init'ed(this.myParser.cMyself.bIsFake) |
| pre | (soft) this.myParser.cMyself.sNickname != null |
| pre | (soft) init'ed(this.myParser.currentSocketState) |
| pre | (soft) init'ed(this.myParser.got001) |
| pre | (soft) this.myParser.hChanModesOther != null |
| pre | (soft) this.myParser.hChannelList != null |
| pre | (soft) this.myParser.me != null |
| pre | (soft) init'ed(this.myParser.me.altNickname) |
| pre | (soft) init'ed(this.myParser.me.prependChar) |
| pre | (soft) this.myParser.myCallbackManager != null |
| pre | (soft) this.myParser.myCallbackManager. callbackHash != null |
| pre | (soft) init'ed(this.myParser.out) |
| presumption | getIRCStringConverter(...).lowercase != null |
| presumption | getIRCStringConverter(...).lowercase.length >= 1 |
| post | init'ed(java.lang.String:substring(...)._tainted) |
| post | init'ed(java.lang.StringBuilder:toString(...)._ tainted) |
| post | possibly_updated(this.myParser.cMyself. myAwayReason) |
| post | this.myParser.me.nickname == One-of{old this.myParser.me.nickname, &java.lang. StringBuilder:toString(...), this.myParser.me. altNickname} |
| post | init'ed(this.myParser.me.nickname) |
| post | this.myParser.sThinkNickname == One-of{old this.myParser.sThinkNickname, old this.myParser. me.nickname, &java.lang.StringBuilder:toString( ...), this.myParser.me.altNickname} |
| post | init'ed(this.myParser.sThinkNickname) |
| post | init'ed(this.myParser.stringConverter) |
| post | init'ed(this.myParser.triedAlt) |
| post | new IRCStringConverter(getIRCStringConverter#1) num objects <= 1 |
| 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 char[](IRCStringConverter#1) num objects <= 1 |
| post | new char[](IRCStringConverter#1) num objects == 0 |
| post | init'ed(new char[](IRCStringConverter#1).length) |
| post | init'ed(new char[](IRCStringConverter#1)[...]) |
| post | possibly_updated(new char[](IRCStringConverter#1)[...]) |
| post | new char[](IRCStringConverter#2) num objects <= 1 |
| post | new char[](IRCStringConverter#2) num objects == 0 |
| post | init'ed(new char[](IRCStringConverter#2).length) |
| post | possibly_updated(new char[](IRCStringConverter#2)[...]) |
| unanalyzed | call on getCallbackManager |
| unanalyzed | call on getCallbackType |
| unanalyzed | call on call |
| unanalyzed | call on java.lang.String:toCharArray |
| unanalyzed | call on java.lang.String:length |
| unanalyzed | call on java.util.Map:containsKey |
| unanalyzed | call on java.lang.String:toLowerCase |
| unanalyzed | call on java.lang.RuntimeException |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on callDebugInfo |
| unanalyzed | call on java.lang.String:indexOf |
| unanalyzed | call on java.lang.String:substring |
| unanalyzed | call on java.lang.String:split |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on java.lang.String:equalsIgnoreCase |
| unanalyzed | call on isFake |
| unanalyzed | call on getNickname |
| unanalyzed | call on java.lang.Character:valueOf |
| unanalyzed | call on java.lang.Byte:byteValue |
| unanalyzed | call on doSendString |
| unanalyzed | call on java.lang.String |
| unanalyzed | call on java.lang.Boolean:valueOf |
| unanalyzed | call on java.lang.String:charAt |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on java.lang.Integer:valueOf |
| unanalyzed | call on java.lang.String:isEmpty |
| unanalyzed | call on java.io.PrintWriter:printf |
| unanalyzed | call on setAwayReason |
| unanalyzed | call on java.util.LinkedList |
| unanalyzed | call on getListModeQueue |
| unanalyzed | call on java.util.LinkedList:contains |
| unanalyzed | call on java.util.Queue:offer |
| unanalyzed | call on java.util.LinkedList:offer |
| unanalyzed | call on java.lang.System:currentTimeMillis |
| test_vector | this.myParser.triedAlt: {0}, {1} |
| test_vector | this.myParser.got001: {1}, {0} |
| test_vector | call(...)@76: {1}, {0} |
