Messages

Last Msg First Msg

method

com.dmdirc.parser.irc.ChannelInfo__static_init

method	void com.dmdirc.parser.irc.ChannelInfo(IRCParser, String)
post	this.askedForListModes == 0
post	this.hasGotListModes == 0
post	this.nCreateTime == 0
post	this.nTopicTime == 0
post	this.bAddingNames == 1
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.hChannelUserList == &new Hashtable(Channel Info#1)
post	this.hListModes == &new Hashtable(ChannelInfo#3 )
post	this.hParamModes == &new Hashtable(ChannelInfo# 2)
post	this.lAddingModes == &new LinkedList(ChannelInf o#4)
post	this.lModeQueue == &new LinkedList(ChannelInfo# 5)
post	this.listModeQueue == &new LinkedList(ChannelIn fo#6)
post	init'ed(this.listModeQueueTime)
post	this.myMap == &new HashMap(ChannelInfo#7)
post	this.myParser == tParser
post	init'ed(this.myParser)
post	this.sName == name
post	init'ed(this.sName)
post	this.sTopic == &""
post	this.sTopicUser == &""

method	Queue getListModeQueue()
pre	init'ed(this.listModeQueueTime)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
post	return_value == One-of{this.listModeQueue, &new LinkedList(getListModeQueue#1)}
post	init'ed(return_value)
post	init'ed(this.listModeQueueTime)
post	new LinkedList(getListModeQueue#1) num objects <= 1
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 call
unanalyzed	call on java.lang.Integer:valueOf

method	void requestListModes()
pre	this.hChannelUserList != null
pre	this.myParser != null
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser.cMyself != null
pre	(soft) init'ed(this.myParser.currentSocketState)
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) init'ed(this.myParser.out)
pre	(soft) this.myParser.sNetworkName != 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	possibly_updated(this.askedForListModes)
post	possibly_updated(this.myParser.cMyself. myAwayReason)
post	init'ed(this.myParser.stringConverter)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1) num objects)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
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	new char[](IRCStringConverter#1) num objects <= 1
post	init'ed(new char[](IRCStringConverter#1).length)
post	init'ed(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2) num objects)
post	new char[](IRCStringConverter#2) num objects <= 1
post	init'ed(new char[](IRCStringConverter#2).length)
post	init'ed(new char[](IRCStringConverter#2)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.util.Map:values
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on getClient
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:equalsIgnoreCase
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.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
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
test_vector	java.lang.Byte:byteValue(...)@160: {-128..0, 2..255}, {1}
test_vector	java.lang.Character:charValue(...)@162: {101}, {0..100, 102..2¹⁶-1}
test_vector	java.lang.Character:charValue(...)@162: {0..72, 74..2¹⁶-1}, {73}
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}

Prev Msg Next Msg

overflow

click for all messages in this file Low Prob.

check that i in {-2³¹-1..2³²-2}

Prev Msg Next Msg

method	bool hasAskedForListModes()
pre	init'ed(this.askedForListModes)
post	return_value == this.askedForListModes
post	init'ed(return_value)

method	bool hasGotListModes()
pre	init'ed(this.hasGotListModes)
post	return_value == this.hasGotListModes
post	init'ed(return_value)

method	void setHasGotListModes(bool)
post	this.hasGotListModes == newValue
post	init'ed(this.hasGotListModes)

method	void setMap(Map)
post	this.myMap == newMap
post	init'ed(this.myMap)

method	Map getMap()
pre	init'ed(this.myMap)
post	return_value == this.myMap
post	init'ed(return_value)

method	void setAddingNames(bool)
post	this.bAddingNames == newValue
post	init'ed(this.bAddingNames)

method	bool isAddingNames()
pre	init'ed(this.bAddingNames)
post	return_value == this.bAddingNames
post	init'ed(return_value)

method	String getName()
post	return_value == this.sName
post	init'ed(return_value)

method	int getUserCount()
pre	this.hChannelUserList != null
post	init'ed(return_value)

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

method	void emptyChannel()
pre	this.hChannelUserList != null
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) init'ed(this.myParser.cMyself)
pre	(soft) this.myParser.hClientList != null
pre	(soft) this.myParser.stringConverter.lowercase != null
pre	(soft) init'ed(this.myParser.stringConverter. lowercase[...])
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(this.myParser.stringConverter)
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)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on getChannel
unanalyzed	call on getName
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.util.Map:remove
unanalyzed	call on java.util.Map:isEmpty
unanalyzed	call on getNickname
unanalyzed	call on forceRemoveClient
test_vector	java.util.Iterator:hasNext(...)@273: {0}, {1}

method	ChannelClientInfo getUser(String)
pre	init'ed(this.myParser.stringConverter)
pre	sWho != null
pre	this.hChannelUserList != null
pre	this.myParser != null
pre	(soft) this.myParser.stringConverter.lowercase != null
pre	(soft) init'ed(this.myParser.stringConverter. lowercase[...])
pre	(soft) this.sName != null
post	init'ed(return_value)
post	this.myParser.stringConverter != null
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 LinkedList(ClientInfo#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*).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*).sRealName)
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*).sHost)
post	not_init'ed(new ClientInfo(getUser#2*).sIdent)
post	init'ed(new ClientInfo(getUser#2*).sNickname)
post	new IRCStringConverter(getIRCStringConverter#1) num objects == 0
post	new char[](IRCStringConverter#1) num objects == 0
post	new char[](IRCStringConverter#2) num objects == 0
post	not_init'ed(new IRCStringConverter(getIRCStringConv erter#1).limit)
post	not_init'ed(new char[](IRCStringConverter#1). length)
post	not_init'ed(new char[](IRCStringConverter#2). length)
post	not_init'ed(new IRCStringConverter(getIRCStringConv erter#1).lowercase)
post	not_init'ed(new IRCStringConverter(getIRCStringConv erter#1).uppercase)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on getChannel
unanalyzed	call on getName
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on com.dmdirc.parser.irc.ChannelClientInfo
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Map:put

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

Prev Msg Next Msg

precondition failure

click for all messages in this file High Prob.

com/dmdirc/parser/irc/IRCStringConverter. toLowerCase: input != null

Prev Msg Next Msg

method	ChannelClientInfo getUser(ClientInfo)
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}

method	ChannelClientInfo addClient(ClientInfo)
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	return_value != null
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, old cClient.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
post	init'ed(this.myParser.stringConverter)
post	new ChannelClientInfo(addClient#1) num objects <= 1
post	new ChannelClientInfo(addClient#1).cClient == cClient
post	new ChannelClientInfo(addClient#1).cClient != null
post	new ChannelClientInfo(addClient#1).myChannel == this
post	new ChannelClientInfo(addClient#1).myChannel != null
post	new ChannelClientInfo(addClient#1).myMap == &new HashMap(ChannelClientInfo#1)
post	new ChannelClientInfo(addClient#1).myParser == this.myParser
post	new ChannelClientInfo(addClient#1).myParser != null
post	new HashMap(ChannelClientInfo#1) num objects <= 1
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
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	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	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:values
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on getClient
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on getChannel
unanalyzed	call on getName
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Map:put

method	void delClient(ClientInfo)
pre	this.hChannelUserList != null
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) init'ed(this.myParser.cMyself)
pre	(soft) this.myParser.hClientList != 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(this.myParser.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
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	init'ed(new char[](IRCStringConverter#1).length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:values
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on getClient
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on getChannel
unanalyzed	call on getName
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.util.Map:remove
unanalyzed	call on java.util.Map:isEmpty
unanalyzed	call on getNickname
unanalyzed	call on forceRemoveClient

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that clTemp != null

Prev Msg Next Msg

method	void renameClient(String, ChannelClientInfo)
pre	this.hChannelUserList != null
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.stringConverter.lowercase != null
pre	(soft) init'ed(this.myParser.stringConverter. lowercase[...])
presumption	cTemp.cClient.sNickname@370 != null
presumption	cTemp.cClient@370 != null
presumption	java.util.Map:get(...)@370 != null
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
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	possibly_updated(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
test_vector	java.util.Map:containsKey(...)@369: {0}, {1}

method	void setCreateTime(long)
post	this.nCreateTime == nNewTime
post	init'ed(this.nCreateTime)

method	long getCreateTime()
pre	init'ed(this.nCreateTime)
post	return_value == this.nCreateTime
post	init'ed(return_value)

method	void setTopicTime(long)
post	this.nTopicTime == nNewTime
post	init'ed(this.nTopicTime)

method	long getTopicTime()
pre	init'ed(this.nTopicTime)
post	return_value == this.nTopicTime
post	init'ed(return_value)

method	void setTopic(String)
post	this.sTopic == sNewTopic
post	init'ed(this.sTopic)

method	String getTopic()
pre	init'ed(this.sTopic)
post	return_value == this.sTopic
post	init'ed(return_value)

method	void setTopicUser(String)
post	this.sTopicUser == sNewUser
post	init'ed(this.sTopicUser)

method	String getTopicUser()
pre	init'ed(this.sTopicUser)
post	return_value == this.sTopicUser
post	init'ed(return_value)

method	void setMode(long)
post	this.nModes == nNewMode
post	init'ed(this.nModes)

method	long getMode()
pre	init'ed(this.nModes)
post	return_value == this.nModes
post	init'ed(return_value)

method	String getModeStr()
pre	this.hParamModes != null
pre	this.myParser != null
pre	this.myParser.hChanModesBool != null
pre	init'ed(this.nModes)
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}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into sTemp

Prev Msg Next Msg

method	void setModeParam(Character, String)
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}

method	String getModeParam(Character)
pre	this.hParamModes != null
post	init'ed(return_value)
test_vector	java.util.Map:containsKey(...)@494: {0}, {1}

method	void setListModeParam(Character, ChannelListModeIt em, bool)
pre	this.myParser != null
pre	this.myParser.hChanModesOther != null
pre	(soft) givenItem != null
pre	(soft) givenItem.myItem != null
pre	(soft) givenItem.myOwner != null
pre	(soft) givenMode != null
pre	(soft) this.myParser.stringConverter != null
pre	(soft) this.hListModes != null
pre	(soft) this.myParser.h005Info != null
pre	(soft) this.myParser.sNetworkName != null
pre	(soft) this.myParser.stringConverter.lowercase != null
pre	(soft) this.myParser.stringConverter.lowercase. length >= 1
pre	(soft) init'ed(this.myParser.stringConverter. lowercase[...])
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(this.myParser.stringConverter)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1) num objects)
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	init'ed(new char[](IRCStringConverter#1) num objects)
post	possibly_updated(new char[](IRCStringConverter#1). length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2) num objects)
post	possibly_updated(new char[](IRCStringConverter#2). length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
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.util.Map:get
unanalyzed	call on java.lang.String:matches
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:substring
test_vector	bAdd: {0}, {1}
test_vector	java.lang.Byte:byteValue(...)@510: {1}, {-128..0, 2..255}
test_vector	java.lang.Character:charValue(...)@513: {98}, {0..97, 99..2¹⁶-1}
test_vector	java.lang.Character:charValue(...)@513: {0..112, 114..2¹⁶-1}, {113}
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: {1}, {0}
test_vector	java.lang.String:equals(...)@515: {0}, {1}
test_vector	java.util.Map:containsKey(...)@510: {0}, {1}
test_vector	java.util.Map:containsKey(...)@527: {1}, {0}

method	List getListModeParam(Character)
pre	this.myParser != null
pre	this.myParser.hChanModesOther != null
pre	(soft) this.hListModes != 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}

method	bool getAddState(Character)
pre	this.lAddingModes != null
post	init'ed(return_value)

method	void setAddState(Character, bool)
pre	this.lAddingModes != null
test_vector	newState: {0}, {1}

method	void resetAddState()
pre	this.lAddingModes != null

method	void alterMode(bool, Character, String)
pre	this.myParser != null
pre	this.myParser.h005Info != null
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) init'ed(this.myParser.currentSocketState)
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	(soft) init'ed(this.myParser.out)
presumption	java.util.Map:get(...)@633 != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(java.lang.String:substring(...)._ tainted)
post	possibly_updated(this.myParser.cMyself. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
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	init'ed(new char[](IRCStringConverter#1).length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.List:clear
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:matches
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on callDebugInfo
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.util.List:size
unanalyzed	call on java.lang.String:equalsIgnoreCase
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.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
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.util.List:isEmpty
unanalyzed	call on java.util.List:get
test_vector	positive: {1}, {0}
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}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into modestr

Prev Msg Next Msg

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that existingParam != null

Prev Msg Next Msg

method	void sendModes()
pre	this.lModeQueue != null
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) init'ed(this.myParser.currentSocketState)
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	(soft) init'ed(this.myParser.out)
presumption	java.util.List:get(...)@677 != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.myParser.cMyself. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
post	init'ed(this.myParser.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
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	init'ed(new char[](IRCStringConverter#1).length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.util.List:clear
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on callDebugInfo
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:equalsIgnoreCase
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.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
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
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}

Prev Msg Next Msg

use of default init

click for all messages in this file Low Prob.

check if init'ed(modeparam.length)

Prev Msg Next Msg

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that not_init'ed(modestr)

Prev Msg Next Msg

Prev Msg Next Msg

use of default init

click for all messages in this file Low Prob.

check if init'ed(modeparam.length)

test always goes same way

Low Prob.

Test predetermined because modeparam.length == 0

dead code

Low Prob.

Dead code here because modeparam.length == 0

Prev Msg Next Msg

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that not_init'ed(modestr)

Prev Msg Next Msg

method	void clearModeQueue()
pre	this.lModeQueue != null

method	void sendMessage(String)
pre	sMessage != null
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) init'ed(this.myParser.currentSocketState)
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	(soft) init'ed(this.myParser.out)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.myParser.cMyself. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
post	init'ed(this.myParser.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
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	init'ed(new char[](IRCStringConverter#1).length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:equalsIgnoreCase
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.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
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
test_vector	java.lang.String:isEmpty(...)@710: {0}, {1}

method	void sendNotice(String)
pre	sMessage != null
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) init'ed(this.myParser.currentSocketState)
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	(soft) init'ed(this.myParser.out)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.myParser.cMyself. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
post	init'ed(this.myParser.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
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	init'ed(new char[](IRCStringConverter#1).length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:equalsIgnoreCase
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.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
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
test_vector	java.lang.String:isEmpty(...)@721: {0}, {1}

method	void sendAction(String)
pre	sMessage != null
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) init'ed(this.myParser.currentSocketState)
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	(soft) init'ed(this.myParser.out)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.myParser.cMyself. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
post	init'ed(this.myParser.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
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	init'ed(new char[](IRCStringConverter#1).length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:toUpperCase
unanalyzed	call on sendMessage
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:equalsIgnoreCase
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.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
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
test_vector	java.lang.String:isEmpty(...)@732: {0}, {1}

method	void sendCTCP(String, String)
pre	sType != null
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) sMessage != null
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) init'ed(this.myParser.currentSocketState)
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	(soft) init'ed(this.myParser.out)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.myParser.cMyself. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
post	init'ed(this.myParser.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
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	init'ed(new char[](IRCStringConverter#1).length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:equalsIgnoreCase
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.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
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
test_vector	java.lang.String:isEmpty(...)@743: {0}, {1}
test_vector	java.lang.String:isEmpty(...)@745: {1}, {0}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into char1

Prev Msg Next Msg

method	void sendCTCPReply(String, String)
pre	sType != null
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) sMessage != null
pre	(soft) this.myParser != null
pre	(soft) this.myParser.cMyself != null
pre	(soft) init'ed(this.myParser.currentSocketState)
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	(soft) init'ed(this.myParser.out)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.myParser.cMyself. myAwayReason)
post	this.myParser.stringConverter == One-of{old this.myParser.stringConverter, &new IRCStringConverter(getIRCStringConverter#1)}
post	init'ed(this.myParser.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
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	init'ed(new char[](IRCStringConverter#1).length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:equalsIgnoreCase
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.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
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
test_vector	java.lang.String:isEmpty(...)@756: {0}, {1}
test_vector	java.lang.String:isEmpty(...)@758: {1}, {0}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into char1

Prev Msg Next Msg

method	String toString()
post	return_value == this.sName
post	init'ed(return_value)

method	IRCParser getParser()
post	return_value == this.myParser
post	init'ed(return_value)