| Kind |
Annotation Text |
| pre | (soft) init'ed(this.myParser.cMyself.myAwayReason) |
| pre | (soft) init'ed(this.myParser.stringConverter) |
| pre | (soft) init'ed(this.myParser.stringConverter. lowercase[...]) |
| pre | (soft) init'ed(token[...]) |
| pre | (soft) this.myParser.cMyself != null |
| pre | (soft) this.myParser.hClientList != null |
| pre | (soft) this.myParser.myCallbackManager != null |
| pre | (soft) this.myParser.myCallbackManager. callbackHash != null |
| pre | (soft) this.myParser.stringConverter.lowercase != null |
| pre | (soft) token != null |
| pre | (soft) token.length in {4..232} |
| pre | (soft) token[3] != null |
| pre | sParam != null |
| pre | this.myParser != 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.cMyself.myAwayReason) |
| post | init'ed(this.myParser.stringConverter) |
| post | new IRCStringConverter(getIRCStringConverter#1) num objects <= 1 |
| post | new char[](IRCStringConverter#1) num objects <= 1 |
| post | new char[](IRCStringConverter#2) num objects <= 1 |
| post | possibly_updated(new char[](IRCStringConverter#1)[...]) |
| post | possibly_updated(new char[](IRCStringConverter#2)[...]) |
| post | possibly_updated(this.myParser.cMyself.bIsAway) |
| post | this.myParser.cMyself.myAwayReason == One-of{old this.myParser.cMyself.myAwayReason, token[3], token[...], &""} |
| post | this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)} |
| unanalyzed | call on call |
| unanalyzed | call on getCallbackManager |
| unanalyzed | call on getCallbackType |
| unanalyzed | call on java.lang.Boolean: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:isEmpty |
| unanalyzed | call on java.lang.String:length |
| 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.util.Map:containsKey |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on parseHost |
| test_vector | java.lang.String:equals(...)@37: {0}, {1} |