ChannelInfo.java

ChannelInfo.java

current inspection = 2009-09-03 21:56:13 (id #1)

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

ChannelClientInfo addClient(ClientInfo)

Kind	Annotation Text
pre	(soft) cClient != null
pre	(soft) cClient.myChannelClientInfos != null
pre	(soft) cClient.myParser != null
pre	(soft) init'ed(cClient.myParser.stringConverter)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.hChannelUserList != null
pre	(soft) this.myParser != null
pre	(soft) this.sName != null
presumption	cClient.myParser.stringConverter.lowercase@335 != null
presumption	cTemp.cClient.sNickname != null
presumption	getIRCStringConverter(...).lowercase != null
post	cClient.myParser.stringConverter == One-of{old cClient.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1), old this.myParser.stringConverter}
post	init'ed(cClient.myParser.stringConverter)
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#1)[...])
post	init'ed(new char[](IRCStringConverter#2).length)
post	init'ed(this.myParser.stringConverter)
post	new ChannelClientInfo(addClient#1) num objects <= 1
post	new ChannelClientInfo(addClient#1).cClient != null
post	new ChannelClientInfo(addClient#1).cClient == cClient
post	new ChannelClientInfo(addClient#1).myChannel != null
post	new ChannelClientInfo(addClient#1).myChannel == this
post	new ChannelClientInfo(addClient#1).myMap == &new HashMap(ChannelClientInfo#1)
post	new ChannelClientInfo(addClient#1).myParser != null
post	new ChannelClientInfo(addClient#1).myParser == this.myParser
post	new HashMap(ChannelClientInfo#1) num objects <= 1
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	return_value != null
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, old cClient.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
unanalyzed	call on getChannel
unanalyzed	call on getClient
unanalyzed	call on getName
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:values

void alterMode(bool, Character, String)

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.currentSocketState)
pre	(soft) init'ed(this.myParser.out)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.hParamModes != null
pre	(soft) this.lModeQueue != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) this.myParser.hChanModesBool != null
pre	(soft) this.myParser.hChanModesOther != null
pre	(soft) this.myParser.hChannelList != null
pre	(soft) this.myParser.hPrefixModes != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
pre	this.myParser != null
pre	this.myParser.h005Info != null
presumption	java.util.Map:get(...)@633 != null
post	init'ed(java.lang.String:substring(...)._tainted)
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	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(java.lang.String:substring(...)._ tainted)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	possibly_updated(this.myParser.cMyself. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
unanalyzed	call on call
unanalyzed	call on callDebugInfo
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
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:equalsIgnoreCase
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.String:indexOf
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.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.List:clear
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:isEmpty
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.Queue:offer
unanalyzed	call on setAwayReason
test_vector	java.lang.String:isEmpty(...)@643: {1}, {0}
test_vector	java.lang.String:matches(...)@1730: {1}, {0}
test_vector	java.util.List:contains(...)@622: {0}, {1}
test_vector	java.util.Map:containsKey(...)@610: {0}, {1}
test_vector	java.util.Map:containsKey(...)@620: {0}, {1}
test_vector	java.util.Map:containsKey(...)@630: {0}, {1}
test_vector	positive: {1}, {0}

void clearModeQueue()

Kind	Annotation Text
pre	this.lModeQueue != null

void com.dmdirc.parser.irc.ChannelInfo(IRCParser, String)

Kind	Annotation Text
post	init'ed(this.listModeQueueTime)
post	init'ed(this.myParser)
post	init'ed(this.sName)
post	new HashMap(ChannelInfo#7) num objects == 1
post	new Hashtable(ChannelInfo#1) num objects == 1
post	new Hashtable(ChannelInfo#2) num objects == 1
post	new Hashtable(ChannelInfo#3) num objects == 1
post	new LinkedList(ChannelInfo#4) num objects == 1
post	new LinkedList(ChannelInfo#5) num objects == 1
post	new LinkedList(ChannelInfo#6) num objects == 1
post	this.askedForListModes == 0
post	this.bAddingNames == 1
post	this.hChannelUserList == &new Hashtable(Channel Info#1)
post	this.hListModes == &new Hashtable(ChannelInfo#3 )
post	this.hParamModes == &new Hashtable(ChannelInfo# 2)
post	this.hasGotListModes == 0
post	this.lAddingModes == &new LinkedList(ChannelInf o#4)
post	this.lModeQueue == &new LinkedList(ChannelInfo# 5)
post	this.listModeQueue == &new LinkedList(ChannelIn fo#6)
post	this.myMap == &new HashMap(ChannelInfo#7)
post	this.myParser == tParser
post	this.nCreateTime == 0
post	this.nTopicTime == 0
post	this.sName == name
post	this.sTopic == &""
post	this.sTopicUser == &""

com.dmdirc.parser.irc.ChannelInfo__static_init

Kind	Annotation Text

void delClient(ClientInfo)

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.cMyself)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.hClientList != null
pre	this.hChannelUserList != null
presumption	cTemp.cClient.sNickname != null
presumption	cTemp.myChannel.sName@350 != null
presumption	cTemp.myChannel@350 != null
presumption	clTemp.myChannelClientInfos@350 != null
presumption	clTemp.myParser.stringConverter.lowercase@350 != null
presumption	clTemp.myParser@350 != null
presumption	clTemp.sNickname != null
presumption	getIRCStringConverter(...).lowercase@350 != null
presumption	getIRCStringConverter(...).lowercase@355 != null
presumption	this.myParser.stringConverter.lowercase@350 != 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#1)[...])
post	init'ed(new char[](IRCStringConverter#2).length)
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)[...])
unanalyzed	call on forceRemoveClient
unanalyzed	call on getChannel
unanalyzed	call on getClient
unanalyzed	call on getName
unanalyzed	call on getNickname
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:isEmpty
unanalyzed	call on java.util.Map:remove
unanalyzed	call on java.util.Map:values

void emptyChannel()

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.cMyself)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) init'ed(this.myParser.stringConverter. lowercase[...])
pre	(soft) this.myParser != null
pre	(soft) this.myParser.hClientList != null
pre	(soft) this.myParser.stringConverter.lowercase != null
pre	this.hChannelUserList != null
presumption	cTemp.myChannelClientInfos@273 != null
presumption	cTemp.myParser.stringConverter.lowercase@273 != null
presumption	cTemp.myParser@273 != null
presumption	cTemp.sNickname != null
presumption	client.cClient@273 != null
presumption	client.myChannel.sName@273 != null
presumption	client.myChannel@273 != null
presumption	java.util.Iterator:next(...)@273 != null
presumption	java.util.Map:values(...)@273 != null
presumption	this.myParser.stringConverter.lowercase@277 != null
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1) num objects)
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) num objects)
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	init'ed(new char[](IRCStringConverter#2).length)
post	init'ed(new char[](IRCStringConverter#2)[...])
post	init'ed(this.myParser.stringConverter)
unanalyzed	call on forceRemoveClient
unanalyzed	call on getChannel
unanalyzed	call on getName
unanalyzed	call on getNickname
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:isEmpty
unanalyzed	call on java.util.Map:remove
test_vector	java.util.Iterator:hasNext(...)@273: {0}, {1}

bool getAddState(Character)

Kind	Annotation Text
pre	this.lAddingModes != null
post	init'ed(return_value)

List getChannelClients()

Kind	Annotation Text
pre	this.hChannelUserList != null
post	new ArrayList(getChannelClients#1) num objects == 1
post	return_value == &new ArrayList(getChannelClient s#1)

long getCreateTime()

Kind	Annotation Text
pre	init'ed(this.nCreateTime)
post	init'ed(return_value)
post	return_value == this.nCreateTime

List getListModeParam(Character)

Kind	Annotation Text
pre	(soft) this.hListModes != null
pre	this.myParser != null
pre	this.myParser.hChanModesOther != null
presumption	java.util.Map:get(...)@550 != null
post	init'ed(return_value)
test_vector	java.lang.Byte:byteValue(...)@550: {1}, {-128..0, 2..255}
test_vector	java.util.Map:containsKey(...)@550: {0}, {1}
test_vector	java.util.Map:containsKey(...)@552: {1}, {0}

Queue getListModeQueue()

Kind	Annotation Text
pre	(soft) this.myParser != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
pre	init'ed(this.listModeQueueTime)
post	init'ed(return_value)
post	init'ed(this.listModeQueueTime)
post	new LinkedList(getListModeQueue#1) num objects <= 1
post	return_value == One-of{this.listModeQueue, &new LinkedList(getListModeQueue#1)}
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

Map getMap()

Kind	Annotation Text
pre	init'ed(this.myMap)
post	init'ed(return_value)
post	return_value == this.myMap

long getMode()

Kind	Annotation Text
pre	init'ed(this.nModes)
post	init'ed(return_value)
post	return_value == this.nModes

String getModeParam(Character)

Kind	Annotation Text
pre	this.hParamModes != null
post	init'ed(return_value)
test_vector	java.util.Map:containsKey(...)@494: {0}, {1}

String getModeStr()

Kind	Annotation Text
pre	init'ed(this.nModes)
pre	this.hParamModes != null
pre	this.myParser != null
pre	this.myParser.hChanModesBool != null
presumption	java.util.Iterator:next(...)@457 != null
presumption	java.util.Iterator:next(...)@461 != null
presumption	java.util.Map:get(...)@458 != null
presumption	java.util.Map:get(...)@462 != null
presumption	java.util.Map:keySet(...)@457 != null
presumption	java.util.Map:keySet(...)@461 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &java.lang.StringBuilder:toStri ng(...)
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
test_vector	java.lang.String:isEmpty(...)@463: {1}, {0}
test_vector	java.util.Iterator:hasNext(...)@457: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@461: {0}, {1}

String getName()

Kind	Annotation Text
post	init'ed(return_value)
post	return_value == this.sName

IRCParser getParser()

Kind	Annotation Text
post	init'ed(return_value)
post	return_value == this.myParser

String getTopic()

Kind	Annotation Text
pre	init'ed(this.sTopic)
post	init'ed(return_value)
post	return_value == this.sTopic

long getTopicTime()

Kind	Annotation Text
pre	init'ed(this.nTopicTime)
post	init'ed(return_value)
post	return_value == this.nTopicTime

String getTopicUser()

Kind	Annotation Text
pre	init'ed(this.sTopicUser)
post	init'ed(return_value)
post	return_value == this.sTopicUser

ChannelClientInfo getUser(ClientInfo)

Kind	Annotation Text
pre	this.hChannelUserList != null
presumption	java.util.Iterator:next(...)@320 != null
presumption	java.util.Map:values(...)@320 != null
post	init'ed(return_value)
test_vector	java.util.Iterator:hasNext(...)@320: {0}, {1}

ChannelClientInfo getUser(String)

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.stringConverter. lowercase[...])
pre	(soft) this.myParser.stringConverter.lowercase != null
pre	(soft) this.sName != null
pre	init'ed(this.myParser.stringConverter)
pre	sWho != null
pre	this.hChannelUserList != null
pre	this.myParser != null
post	init'ed(new ClientInfo(getUser#2*).sNickname)
post	init'ed(return_value)
post	new ChannelClientInfo(getUser#1*) num objects == 0
post	new ClientInfo(getUser#2*) num objects == 0
post	new HashMap(ChannelClientInfo#1) num objects == 0
post	new HashMap(ClientInfo#3) num objects == 0
post	new Hashtable(ClientInfo#1) num objects == 0
post	new IRCStringConverter(getIRCStringConverter#1) num objects == 0
post	new LinkedList(ClientInfo#2) num objects == 0
post	new char[](IRCStringConverter#1) num objects == 0
post	new char[](IRCStringConverter#2) num objects == 0
post	not_init'ed(new ChannelClientInfo(getUser#1*). cClient)
post	not_init'ed(new ChannelClientInfo(getUser#1*). myChannel)
post	not_init'ed(new ChannelClientInfo(getUser#1*). myMap)
post	not_init'ed(new ChannelClientInfo(getUser#1*). myParser)
post	not_init'ed(new ClientInfo(getUser#2*).bIsFake)
post	not_init'ed(new ClientInfo(getUser#2*).lModeQueue)
post	not_init'ed(new ClientInfo(getUser#2*). myAwayReason)
post	not_init'ed(new ClientInfo(getUser#2*). myChannelClientInfos)
post	not_init'ed(new ClientInfo(getUser#2*).myMap)
post	not_init'ed(new ClientInfo(getUser#2*).myParser)
post	not_init'ed(new ClientInfo(getUser#2*).sHost)
post	not_init'ed(new ClientInfo(getUser#2*).sIdent)
post	not_init'ed(new ClientInfo(getUser#2*).sRealName)
post	not_init'ed(new IRCStringConverter(getIRCStringConv erter#1).limit)
post	not_init'ed(new IRCStringConverter(getIRCStringConv erter#1).lowercase)
post	not_init'ed(new IRCStringConverter(getIRCStringConv erter#1).uppercase)
post	not_init'ed(new char[](IRCStringConverter#1). length)
post	not_init'ed(new char[](IRCStringConverter#2). length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.myParser.stringConverter != null
unanalyzed	call on com.dmdirc.parser.irc.ChannelClientInfo
unanalyzed	call on getChannel
unanalyzed	call on getName
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.util.HashMap
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put

ChannelClientInfo getUser(String, bool)

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.stringConverter. lowercase[...])
pre	(soft) this.myParser.stringConverter.lowercase != null
pre	(soft) this.sName != null
pre	init'ed(this.myParser.stringConverter)
pre	sWho != null
pre	this.hChannelUserList != null
pre	this.myParser != null
presumption	setFake(...).myParser.stringConverter.lowercase != null
post	init'ed(new ClientInfo(getUser#2).sNickname)
post	init'ed(return_value)
post	new ChannelClientInfo(getUser#1) num objects <= 1
post	new ChannelClientInfo(getUser#1).cClient == &new ClientInfo(getUser#2)
post	new ChannelClientInfo(getUser#1).myChannel != null
post	new ChannelClientInfo(getUser#1).myChannel == this
post	new ChannelClientInfo(getUser#1).myMap == &new HashMap(ChannelClientInfo#1)
post	new ChannelClientInfo(getUser#1).myParser != null
post	new ChannelClientInfo(getUser#1).myParser == this.myParser
post	new ClientInfo(getUser#2) num objects <= 1
post	new ClientInfo(getUser#2).bIsFake == 1
post	new ClientInfo(getUser#2).lModeQueue == &new LinkedList(ClientInfo#2)
post	new ClientInfo(getUser#2).myAwayReason == &""
post	new ClientInfo(getUser#2).myChannelClientInfos == &new Hashtable(ClientInfo#1)
post	new ClientInfo(getUser#2).myMap == &new HashMap(ClientInfo#3)
post	new ClientInfo(getUser#2).myParser != null
post	new ClientInfo(getUser#2).myParser == this.myParser
post	new ClientInfo(getUser#2).sHost in Addr_Set{null, &""}
post	new ClientInfo(getUser#2).sIdent in Addr_Set{null,&""}
post	new ClientInfo(getUser#2).sRealName == &""
post	new HashMap(ChannelClientInfo#1) num objects <= 1
post	new HashMap(ClientInfo#3) num objects <= 1
post	new Hashtable(ClientInfo#1) num objects <= 1
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	new IRCStringConverter(getIRCStringConverter#1) num objects == 0
post	new IRCStringConverter(getIRCStringConverter#1). limit == 4
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == &new char[](IRCStringConverter#1)
post	new IRCStringConverter(getIRCStringConverter#1). uppercase == &new char[](IRCStringConverter#2)
post	new LinkedList(ClientInfo#2) num objects <= 1
post	new char[](IRCStringConverter#1) num objects == 0
post	new char[](IRCStringConverter#1) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects == 0
post	new char[](IRCStringConverter#2) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2).length == 127
post	not_init'ed(new IRCStringConverter(getIRCStringConv erter#1).limit)
post	not_init'ed(new IRCStringConverter(getIRCStringConv erter#1).lowercase)
post	not_init'ed(new IRCStringConverter(getIRCStringConv erter#1).uppercase)
post	not_init'ed(new char[](IRCStringConverter#1). length)
post	not_init'ed(new char[](IRCStringConverter#2). length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.myParser.stringConverter != null
unanalyzed	call on getChannel
unanalyzed	call on getName
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.util.HashMap
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:put
test_vector	createFake: {0}, {1}
test_vector	java.util.Map:containsKey(...)@303: {0}, {1}

int getUserCount()

Kind	Annotation Text
pre	this.hChannelUserList != null
post	init'ed(return_value)

bool hasAskedForListModes()

Kind	Annotation Text
pre	init'ed(this.askedForListModes)
post	init'ed(return_value)
post	return_value == this.askedForListModes

bool hasGotListModes()

Kind	Annotation Text
pre	init'ed(this.hasGotListModes)
post	init'ed(return_value)
post	return_value == this.hasGotListModes

bool isAddingNames()

Kind	Annotation Text
pre	init'ed(this.bAddingNames)
post	init'ed(return_value)
post	return_value == this.bAddingNames

void renameClient(String, ChannelClientInfo)

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) init'ed(this.myParser.stringConverter. lowercase[...])
pre	(soft) this.myParser != null
pre	(soft) this.myParser.stringConverter.lowercase != null
pre	this.hChannelUserList != null
presumption	cTemp.cClient.sNickname@370 != null
presumption	cTemp.cClient@370 != null
presumption	java.util.Map:get(...)@370 != null
post	init'ed(this.myParser.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	new IRCStringConverter(getIRCStringConverter#1). limit == 4
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == &new char[](IRCStringConverter#1)
post	new IRCStringConverter(getIRCStringConverter#1). uppercase == &new char[](IRCStringConverter#2)
post	new char[](IRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray
test_vector	java.util.Map:containsKey(...)@369: {0}, {1}

void requestListModes()

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.currentSocketState)
pre	(soft) init'ed(this.myParser.out)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser.cMyself != null
pre	(soft) this.myParser.h005Info != null
pre	(soft) this.myParser.hChanModesOther != null
pre	(soft) this.myParser.hChannelList != null
pre	(soft) this.myParser.hPrefixModes != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
pre	(soft) this.myParser.sNetworkName != null
pre	this.hChannelUserList != null
pre	this.myParser != null
presumption	java.util.Iterator:next(...)@159 != null
presumption	java.util.Map:get(...)@141 != null
presumption	java.util.Map:get(...)@160 != null
presumption	java.util.Map:keySet(...)@159 != null
presumption	me.myParser@124 != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1) num objects)
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) num objects)
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	init'ed(new char[](IRCStringConverter#2).length)
post	init'ed(new char[](IRCStringConverter#2)[...])
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.askedForListModes)
post	possibly_updated(this.myParser.cMyself. myAwayReason)
unanalyzed	call on call
unanalyzed	call on doSendString
unanalyzed	call on getClient
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
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:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
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.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:values
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on setAwayReason
test_vector	java.lang.Byte:byteValue(...)@160: {-128..0, 2..255}, {1}
test_vector	java.lang.Character:charValue(...)@162: {0..72, 74..2¹⁶-1}, {73}
test_vector	java.lang.Character:charValue(...)@162: {101}, {0..100, 102..2¹⁶-1}
test_vector	java.lang.Character:charValue(...)@165: {0..71, 73..2¹⁶-1}, {72}
test_vector	java.lang.String:equals(...)@134: {1}, {0}
test_vector	java.lang.String:equals(...)@135: {0}, {1}
test_vector	java.lang.String:equals(...)@137: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@159: {0}, {1}
test_vector	java.util.Map:containsKey(...)@155: {1}, {0}
test_vector	java.util.Map:get(...)@141: Addr_Set{null}, Inverse{null}

void resetAddState()

Kind	Annotation Text
pre	this.lAddingModes != null

void sendAction(String)

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.currentSocketState)
pre	(soft) init'ed(this.myParser.out)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) this.myParser.hChanModesOther != null
pre	(soft) this.myParser.hChannelList != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
pre	sMessage != null
post	init'ed(java.lang.String:substring(...)._tainted)
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 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. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
unanalyzed	call on call
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
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:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
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.lang.String:toUpperCase
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on sendMessage
unanalyzed	call on setAwayReason
test_vector	java.lang.String:isEmpty(...)@732: {0}, {1}

void sendCTCP(String, String)

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.currentSocketState)
pre	(soft) init'ed(this.myParser.out)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) sMessage != null
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) this.myParser.hChanModesOther != null
pre	(soft) this.myParser.hChannelList != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
pre	sType != null
post	init'ed(java.lang.String:substring(...)._tainted)
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 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. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
unanalyzed	call on call
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
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:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
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.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on setAwayReason
test_vector	java.lang.String:isEmpty(...)@743: {0}, {1}
test_vector	java.lang.String:isEmpty(...)@745: {1}, {0}

void sendCTCPReply(String, String)

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.currentSocketState)
pre	(soft) init'ed(this.myParser.out)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) sMessage != null
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) this.myParser.hChanModesOther != null
pre	(soft) this.myParser.hChannelList != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
pre	sType != null
post	init'ed(java.lang.String:substring(...)._tainted)
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 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. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
unanalyzed	call on call
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
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:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
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.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on setAwayReason
test_vector	java.lang.String:isEmpty(...)@756: {0}, {1}
test_vector	java.lang.String:isEmpty(...)@758: {1}, {0}

void sendMessage(String)

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.currentSocketState)
pre	(soft) init'ed(this.myParser.out)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) this.myParser.hChanModesOther != null
pre	(soft) this.myParser.hChannelList != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
pre	sMessage != null
post	init'ed(java.lang.String:substring(...)._tainted)
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 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. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
unanalyzed	call on call
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
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:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
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.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on setAwayReason
test_vector	java.lang.String:isEmpty(...)@710: {0}, {1}

void sendModes()

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.currentSocketState)
pre	(soft) init'ed(this.myParser.out)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) this.myParser.hChanModesOther != null
pre	(soft) this.myParser.hChannelList != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
pre	this.lModeQueue != null
presumption	java.util.List:get(...)@677 != null
post	init'ed(java.lang.String:substring(...)._tainted)
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 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. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
unanalyzed	call on call
unanalyzed	call on callDebugInfo
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
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:equalsIgnoreCase
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.String:indexOf
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.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.List:clear
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on setAwayReason
test_vector	java.lang.String:charAt(...)@679: {0..42, 44..2¹⁶-1}, {43}
test_vector	java.lang.StringBuilder:length(...)@688: {-2³¹..0}, {1..2³²-1}
test_vector	java.lang.StringBuilder:length(...)@689: {-2³¹..0}, {1..2³²-1}
test_vector	java.lang.StringBuilder:length(...)@690: {-2³¹..0}, {1..2³²-1}
test_vector	java.lang.StringBuilder:length(...)@691: {-2³¹..0}, {1..2³²-1}
test_vector	java.util.List:isEmpty(...)@667: {0}, {1}

void sendNotice(String)

Kind	Annotation Text
pre	(soft) init'ed(this.myParser.currentSocketState)
pre	(soft) init'ed(this.myParser.out)
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) this.myParser.hChanModesOther != null
pre	(soft) this.myParser.hChannelList != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
pre	sMessage != null
post	init'ed(java.lang.String:substring(...)._tainted)
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 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. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
unanalyzed	call on call
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
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:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
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.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on setAwayReason
test_vector	java.lang.String:isEmpty(...)@721: {0}, {1}

void setAddState(Character, bool)

Kind	Annotation Text
pre	this.lAddingModes != null
test_vector	newState: {0}, {1}

void setAddingNames(bool)

Kind	Annotation Text
post	init'ed(this.bAddingNames)
post	this.bAddingNames == newValue

void setCreateTime(long)

Kind	Annotation Text
post	init'ed(this.nCreateTime)
post	this.nCreateTime == nNewTime

void setHasGotListModes(bool)

Kind	Annotation Text
post	init'ed(this.hasGotListModes)
post	this.hasGotListModes == newValue

void setListModeParam(Character, ChannelListModeItem, bool)

Kind	Annotation Text
pre	(soft) givenItem != null
pre	(soft) givenItem.myItem != null
pre	(soft) givenItem.myOwner != null
pre	(soft) givenMode != null
pre	(soft) init'ed(this.myParser.stringConverter. lowercase[...])
pre	(soft) this.hListModes != null
pre	(soft) this.myParser.h005Info != null
pre	(soft) this.myParser.sNetworkName != null
pre	(soft) this.myParser.stringConverter != null
pre	(soft) this.myParser.stringConverter.lowercase != null
pre	(soft) this.myParser.stringConverter.lowercase. length >= 1
pre	this.myParser != null
pre	this.myParser.hChanModesOther != null
presumption	getIRCStringConverter(...).lowercase.length@514 >= 1
presumption	getIRCStringConverter(...).lowercase@514 != null
presumption	java.util.ArrayList:get(...)@532 != null
presumption	java.util.Map:get(...)@510 != null
presumption	java.util.Map:get(...)@530 != null
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1) num objects)
post	init'ed(new char[](IRCStringConverter#1) num objects)
post	init'ed(new char[](IRCStringConverter#2) num objects)
post	init'ed(this.myParser.stringConverter)
post	possibly_updated(new IRCStringConverter(getIRCStrin gConverter#1).limit)
post	possibly_updated(new IRCStringConverter(getIRCStrin gConverter#1).lowercase)
post	possibly_updated(new IRCStringConverter(getIRCStrin gConverter#1).uppercase)
post	possibly_updated(new char[](IRCStringConverter#1). length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2). length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equalsIgnoreCase
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:substring
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
test_vector	bAdd: {0}, {1}
test_vector	java.lang.Byte:byteValue(...)@510: {1}, {-128..0, 2..255}
test_vector	java.lang.Character:charValue(...)@513: {0..112, 114..2¹⁶-1}, {113}
test_vector	java.lang.Character:charValue(...)@513: {98}, {0..97, 99..2¹⁶-1}
test_vector	java.lang.Character:charValue(...)@516: {0..97, 99..2¹⁶-1}, {98}
test_vector	java.lang.Character:charValue(...)@518: {0..112, 114..2¹⁶-1}, {113}
test_vector	java.lang.String:charAt(...)@516: {0..36, 38..2¹⁶-1}, {37}
test_vector	java.lang.String:charAt(...)@518: {37}, {0..36, 38..2¹⁶-1}
test_vector	java.lang.String:charAt(...)@521: {0..36, 38..2¹⁶-1}, {37}
test_vector	java.lang.String:equals(...)@515: {0}, {1}
test_vector	java.lang.String:equals(...)@515: {1}, {0}
test_vector	java.util.Map:containsKey(...)@510: {0}, {1}
test_vector	java.util.Map:containsKey(...)@527: {1}, {0}

void setMap(Map)

Kind	Annotation Text
post	init'ed(this.myMap)
post	this.myMap == newMap

void setMode(long)

Kind	Annotation Text
post	init'ed(this.nModes)
post	this.nModes == nNewMode

void setModeParam(Character, String)

Kind	Annotation Text
pre	sValue != null
pre	this.hParamModes != null
test_vector	java.lang.String:isEmpty(...)@479: {0}, {1}
test_vector	java.util.Map:containsKey(...)@480: {0}, {1}

void setTopic(String)

Kind	Annotation Text
post	init'ed(this.sTopic)
post	this.sTopic == sNewTopic

void setTopicTime(long)

Kind	Annotation Text
post	init'ed(this.nTopicTime)
post	this.nTopicTime == nNewTime

void setTopicUser(String)

Kind	Annotation Text
post	init'ed(this.sTopicUser)
post	this.sTopicUser == sNewUser

String toString()

Kind	Annotation Text
post	init'ed(return_value)
post	return_value == this.sName