| Kind |
Annotation Text |
| pre | (soft) init'ed(this.myParser...lastLine) |
| pre | (soft) init'ed(this.myParser.cMyself.bIsFake) |
| pre | (soft) init'ed(this.myParser.cMyself.sNickname) |
| pre | (soft) init'ed(this.myParser.lastLine) |
| pre | (soft) init'ed(this.myParser.sThinkNickname) |
| pre | (soft) init'ed(this.myParser.stringConverter) |
| pre | (soft) init'ed(this.myParser.stringConverter. lowercase[...]) |
| pre | (soft) sParam != null |
| pre | (soft) this.myParser...myCallbackManager != null |
| pre | (soft) this.myParser...myCallbackManager. callbackHash != null |
| pre | (soft) this.myParser.cMyself != null |
| pre | (soft) this.myParser.hChanPrefix != null |
| pre | (soft) this.myParser.hChannelList != null |
| pre | (soft) this.myParser.hClientList != null |
| pre | (soft) this.myParser.myCallbackManager != null |
| pre | (soft) this.myParser.myCallbackManager. callbackHash != null |
| pre | (soft) this.myParser.myIgnoreList != null |
| pre | (soft) this.myParser.myIgnoreList.ignoreInfo != null |
| pre | (soft) this.myParser.myProcessingManager != null |
| pre | (soft) this.myParser.myProcessingManager.myParser != null |
| pre | (soft) this.myParser.myProcessingManager. processHash != null |
| pre | (soft) this.myParser.stringConverter.lowercase != null |
| pre | (soft) token.length in {1..232} |
| pre | (soft) token[1] != null |
| pre | (soft) token[2] != null |
| pre | (soft) token[...] != null |
| pre | this.myParser != null |
| pre | token != null |
| pre | token[0] != null |
| presumption | getIRCStringConverter(...).lowercase.length@159 >= 1 |
| presumption | getIRCStringConverter(...).lowercase@159 != null |
| presumption | iChannel.hChannelUserList != null |
| presumption | iClient.sHost != null |
| presumption | java.lang.Character:valueOf(...)@104 != null |
| presumption | java.lang.Character:valueOf(...)@84 != null |
| presumption | java.lang.Character:valueOf(...)@93 != null |
| presumption | this.myParser.stringConverter.lowercase != null |
| 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 | init'ed(new char[](IRCStringConverter#1).length) |
| post | init'ed(new char[](IRCStringConverter#2).length) |
| post | init'ed(this.myParser.stringConverter) |
| post | new IRCStringConverter(getIRCStringConverter#1) num objects <= 1 |
| post | new IRCStringConverter(getIRCStringConverter#1) num objects == 0 |
| post | new char[](IRCStringConverter#1) num objects <= 1 |
| post | new char[](IRCStringConverter#1) num objects == 0 |
| post | new char[](IRCStringConverter#2) num objects <= 1 |
| post | new char[](IRCStringConverter#2) num objects == 0 |
| post | possibly_updated(java.lang.String:substring(...)._ tainted) |
| post | possibly_updated(new char[](IRCStringConverter#1)[...]) |
| post | possibly_updated(new char[](IRCStringConverter#2)[...]) |
| post | token[0] != null |
| post | token[0] == One-of{old token[0], &java.lang. String:substring(...)} |
| unanalyzed | call on call |
| unanalyzed | call on callDebugInfo |
| unanalyzed | call on callErrorInfo |
| unanalyzed | call on get |
| unanalyzed | call on getCallbackManager |
| unanalyzed | call on getCallbackType |
| unanalyzed | call on getChannelInfo |
| unanalyzed | call on getClient |
| unanalyzed | call on getClientInfo |
| unanalyzed | call on getLastLine |
| unanalyzed | call on getNickname |
| unanalyzed | call on isFake |
| unanalyzed | call on isValidChannelName |
| unanalyzed | call on java.lang.Character:valueOf |
| unanalyzed | call on java.lang.Exception |
| unanalyzed | call on java.lang.Exception:getMessage |
| unanalyzed | call on java.lang.Integer:parseInt |
| unanalyzed | call on java.lang.Integer:valueOf |
| unanalyzed | call on java.lang.RuntimeException |
| unanalyzed | call on java.lang.String |
| unanalyzed | call on java.lang.String:charAt |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on java.lang.String:format |
| unanalyzed | call on java.lang.String:isEmpty |
| unanalyzed | call on java.lang.String:length |
| unanalyzed | call on java.lang.String:matches |
| unanalyzed | call on java.lang.String:split |
| unanalyzed | call on java.lang.String:substring |
| unanalyzed | call on java.lang.String:toCharArray |
| unanalyzed | call on java.lang.String:toLowerCase |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on java.util.Collection:iterator |
| unanalyzed | call on java.util.Hashtable:containsKey |
| unanalyzed | call on java.util.Hashtable:get |
| unanalyzed | call on java.util.List:get |
| unanalyzed | call on java.util.List:size |
| unanalyzed | call on java.util.Map:containsKey |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.util.Map:isEmpty |
| unanalyzed | call on java.util.Map:values |
| unanalyzed | call on parseHost |
| unanalyzed | call on process |
| test_vector | java.lang.Character:equals(...)@104: {0}, {1} |
| test_vector | java.lang.Character:equals(...)@93: {0}, {1} |
| test_vector | java.lang.String:charAt(...)@121: {0..57, 59..216-1}, {58} |
| test_vector | java.lang.String:charAt(...)@51: {0..57, 59..216-1}, {58} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@142: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@152: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@160: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@170: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@179: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@189: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@67: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@90: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@93: {0}, {1} |
| test_vector | java.lang.String:indexOf(...)@67: {-231.. -2, 0..232-1}, {-1} |
| test_vector | java.lang.String:isEmpty(...)@113: {1}, {0} |
| test_vector | java.lang.String:isEmpty(...)@126: {0}, {1} |
| test_vector | java.lang.String:length(...)@121: {0,1}, {2..232-1} |
| test_vector | java.lang.String:length(...)@89: {0,1}, {2..232-1} |
| test_vector | token.length: {4..232}, {1,2}, {3} |