Messages

Last Msg First Msg

method

com.dmdirc.parser.irc.IRCParser$1__static_init

method

com.dmdirc.parser.irc.IRCParser__static_init

method

void com.dmdirc.parser.irc.IRCParser$1(IRCParser)

method	X509Certificate[] getAcceptedIssuers()
post	return_value == null

method

void checkClientTrusted(X509Certificate[], String)

method

void checkServerTrusted(X509Certificate[], String)

method

void com.dmdirc.parser.irc.IRCParser()

call too complex - analysis skipped Info call on void com.dmdirc.parser.irc.IRCParser(MyInfo , ServerInfo)

method

void com.dmdirc.parser.irc.IRCParser(ServerInfo)

call too complex - analysis skipped Info call on void com.dmdirc.parser.irc.IRCParser(MyInfo , ServerInfo)

method

void com.dmdirc.parser.irc.IRCParser(MyInfo)

call too complex - analysis skipped Info call on void com.dmdirc.parser.irc.IRCParser(MyInfo , ServerInfo)

method	void com.dmdirc.parser.irc.IRCParser(MyInfo, ServerInfo)
pre	(soft) com.dmdirc.parser.irc.callbacks. CallbackManager__static_init.new Class[](CallbackMa nager__static_init#1)[...] != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	init'ed(this.addLastLine)
post	this.autoListMode == 1
post	this.disconnectOnFatal == 1
post	this.nNextKeyCMBool == 1
post	this.nNextKeyPrefix == 1
post	this.nNextKeyUser == 1
post	this.removeAfterCallback == 1
post	new ArrayList(RegexStringList#1) num objects == 1
post	new AtomicBoolean(IRCParser#4) num objects == 1
post	new CallbackManager(IRCParser#16) num objects == 1
post	new ClientInfo(IRCParser#13) num objects == 1
post	new ClientInfo(IRCParser#13).bIsFake == 1
post	new ClientInfo(resetState#1) num objects == 1
post	this.cMyself.bIsFake == 1
post	new HashMap(ClientInfo#3) num objects == 1
post	new Hashtable(CallbackManager#1) num objects == 1
post	new Hashtable(ClientInfo#1) num objects == 1
post	new Hashtable(IRCParser#10) num objects == 1
post	new Hashtable(IRCParser#11) num objects == 1
post	new Hashtable(IRCParser#12) num objects == 1
post	new Hashtable(IRCParser#14) num objects == 1
post	new Hashtable(IRCParser#5) num objects == 1
post	new Hashtable(IRCParser#6) num objects == 1
post	new Hashtable(IRCParser#7) num objects == 1
post	new Hashtable(IRCParser#8) num objects == 1
post	new Hashtable(IRCParser#9) num objects == 1
post	new Hashtable(ProcessingManager#1) num objects == 1
post	new IRCParser$1(IRCParser#19) num objects == 1
post	new IRCStringConverter(updateCharArrays#1) num objects == 1
post	new LinkedList(ClientInfo#2) num objects == 1
post	new MyInfo(IRCParser#1) num objects == 1
post	new ProcessingManager(IRCParser#17) num objects == 1
post	new RegexStringList(IRCParser#15) num objects == 1
post	new Semaphore(IRCParser#3) num objects == 1
post	new ServerInfo(IRCParser#2) num objects == 1
post	new TrustManager[](IRCParser#18) num objects == 1
post	this.myTrustManager.length == 1
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#2) num objects == 1
post	this.bindIP == &""
post	this.lastLine == &""
post	this.lastPingValue == &""
post	this.sNetworkName == &""
post	this.sServerName == &""
post	new ClientInfo(IRCParser#13).myAwayReason == &""
post	new ClientInfo(IRCParser#13).sRealName == &""
post	this.cMyself.myAwayReason == &""
post	this.cMyself.sRealName == &""
post	new ServerInfo(IRCParser#2).password == &""
post	new ServerInfo(IRCParser#2).proxyPass == &""
post	new ServerInfo(IRCParser#2).proxyUser == &""
post	this.cMyself == &new ClientInfo(resetState#1)
post	init'ed(this.createFake)
post	this.currentSocketState == &com.dmdirc.parser. irc.SocketState__static_init.new SocketState(Socket State__static_init#2)
post	this.got001 == 0
post	this.post005 == 0
post	this.triedAlt == 0
post	this.h005Info == &new Hashtable(IRCParser#14)
post	this.hChanModesBool == &new Hashtable(IRCParser #8)
post	this.hChanModesOther == &new Hashtable(IRCParse r#9)
post	this.hChanPrefix == &new Hashtable(IRCParser#10 )
post	this.hChannelList == &new Hashtable(IRCParser#1 2)
post	this.hClientList == &new Hashtable(IRCParser#11 )
post	this.hPrefixMap == &new Hashtable(IRCParser#6)
post	this.hPrefixModes == &new Hashtable(IRCParser#5 )
post	this.hUserModes == &new Hashtable(IRCParser#7)
post	this.me == One-of{&new MyInfo(IRCParser#1), myDetails}
post	this.me != null
post	this.myCallbackManager == &new CallbackManager( IRCParser#16)
post	this.myIgnoreList == &new RegexStringList(IRCPa rser#15)
post	this.myProcessingManager == &new ProcessingManager(IRCParser#17)
post	this.myTrustManager == &new TrustManager[](IRCP arser#18)
post	this.trustAllCerts == &new TrustManager[](IRCPa rser#18)
post	this.pingCountDownLength == 6
post	this.pingNeeded == &new AtomicBoolean(IRCParser #4)
post	this.pingTimer == null
post	this.pingTimerLength == 10_000
post	this.pingTimerSem == &new Semaphore(IRCParser#3 )
post	this.server == One-of{&new ServerInfo(IRCParser #2), serverDetails}
post	this.server != null
post	this.stringConverter == &new IRCStringConverter (updateCharArrays#1)
post	this.myCallbackManager.callbackHash == &new Hashtable(CallbackManager#1)
post	this.myCallbackManager.myParser == this
post	this.myCallbackManager.myParser != null
post	new ClientInfo(IRCParser#13).myParser == this.myCallbackManager.myParser
post	this.cMyself.myParser == this.myCallbackManager. myParser
post	this.myProcessingManager.myParser == this.myCallbackManager.myParser
post	new ClientInfo(IRCParser#13).lModeQueue == &new LinkedList(ClientInfo#2)
post	new ClientInfo(IRCParser#13).myChannelClientInfos == &new Hashtable(ClientInfo#1)
post	new ClientInfo(IRCParser#13).myMap == &new HashMap(ClientInfo#3)
post	new ClientInfo(IRCParser#13).sHost == One-of{this.bindIP, undefined}
post	new ClientInfo(IRCParser#13).sHost in Addr_Set{null,&""}
post	new ClientInfo(IRCParser#13).sIdent == One-of{this.bindIP, undefined}
post	new ClientInfo(IRCParser#13).sIdent in Addr_Set{null,&""}
post	init'ed(new ClientInfo(IRCParser#13).sNickname)
post	this.cMyself.lModeQueue == &new LinkedList(ClientInfo#2)
post	this.cMyself.myChannelClientInfos == &new Hashtable(ClientInfo#1)
post	this.cMyself.myMap == &new HashMap(ClientInfo#3 )
post	this.cMyself.sHost == One-of{this.bindIP, undefined}
post	this.cMyself.sHost in Addr_Set{null,&""}
post	this.cMyself.sIdent == One-of{this.bindIP, undefined}
post	this.cMyself.sIdent in Addr_Set{null,&""}
post	this.cMyself.sNickname == undefined
post	this.cMyself.sNickname == null
post	this.stringConverter.limit == 4
post	this.stringConverter.lowercase == &new char[](IRCStringConverter#1)
post	this.stringConverter.uppercase == &new char[](IRCStringConverter#2)
post	new MyInfo(IRCParser#1).altNickname == One-of{&"IRC-Parser", &java.lang. StringBuilder:toString(...)}
post	new MyInfo(IRCParser#1).altNickname in Addr_Set{&"IRC-Parser",&java.lang. StringBuilder:toString(...)}
post	new MyInfo(IRCParser#1).nickname != null
post	new MyInfo(IRCParser#1).prependChar == 95
post	new MyInfo(IRCParser#1).realname == One-of{&"DMDIrc IRCParser", &java.lang. StringBuilder:toString(...)}
post	new MyInfo(IRCParser#1).realname in Addr_Set{&"DMDIrc IRCParser",&java.lang. StringBuilder:toString(...)}
post	new MyInfo(IRCParser#1).username != null
post	this.myProcessingManager.processHash == &new Hashtable(ProcessingManager#1)
post	this.myIgnoreList.ignoreInfo == &new ArrayList(RegexStringList#1)
post	new ServerInfo(IRCParser#2).host == &"irc.quakenet.org"
post	init'ed(new ServerInfo(IRCParser#2).isSSL)
post	new ServerInfo(IRCParser#2).port == 6_667
post	new ServerInfo(IRCParser#2).proxyHost == &"127.0.0.1"
post	new ServerInfo(IRCParser#2).proxyPort == 1_080
post	init'ed(new ServerInfo(IRCParser#2).useSocksProxy)
post	this.myTrustManager[0] == &new IRCParser$1(IRCP arser#19)
post	this.stringConverter.lowercase.length == 127
post	this.stringConverter.uppercase.length == 127
post	possibly_updated(this.stringConverter.lowercase[...])
post	possibly_updated(this.stringConverter.uppercase[...])
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.Timer:cancel
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on java.util.Map:clear
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 callDebugInfo
unanalyzed	call on com.dmdirc.parser.irc.ClientInfo
unanalyzed	call on setFake
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.util.Hashtable:containsKey
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.System:getProperty
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.lang.Class:getSimpleName
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.lang.Class:isAnnotationPresent
unanalyzed	call on java.lang.Class:asSubclass
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.Class:getPackage
unanalyzed	call on java.lang.Package:getName
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.Class:getName
unanalyzed	call on doDebug
unanalyzed	call on java.util.Hashtable:remove
unanalyzed	call on java.util.Hashtable:put
unanalyzed	call on handles
unanalyzed	call on com.dmdirc.parser.irc.IRCProcessor
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.HashMap
test_vector	myDetails: Addr_Set{null}, Inverse{null}
test_vector	serverDetails: Addr_Set{null}, Inverse{null}

method	String getBindIP()
pre	init'ed(this.bindIP)
post	return_value == this.bindIP
post	init'ed(return_value)

method	void setBindIP(String)
post	this.bindIP == newValue
post	init'ed(this.bindIP)

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

method	void setCreateFake(bool)
post	this.createFake == newValue
post	init'ed(this.createFake)

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

method	void setAutoListMode(bool)
post	this.autoListMode == newValue
post	init'ed(this.autoListMode)

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

method	void setRemoveAfterCallback(bool)
post	this.removeAfterCallback == newValue
post	init'ed(this.removeAfterCallback)

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

method	void setAddLastLine(bool)
post	this.addLastLine == newValue
post	init'ed(this.addLastLine)

method	SocketState getSocketState()
pre	init'ed(this.currentSocketState)
post	return_value == this.currentSocketState
post	init'ed(return_value)

method	ProcessingManager getProcessingManager()
pre	init'ed(this.myProcessingManager)
post	return_value == this.myProcessingManager
post	init'ed(return_value)

method	CallbackManager getCallbackManager()
pre	init'ed(this.myCallbackManager)
post	return_value == this.myCallbackManager
post	init'ed(return_value)

method	TrustManager[] getDefaultTrustManager()
post	return_value == this.trustAllCerts
post	init'ed(return_value)

method	TrustManager[] getTrustManager()
pre	init'ed(this.myTrustManager)
post	return_value == this.myTrustManager
post	init'ed(return_value)

method	void setTrustManager(TrustManager[])
post	this.myTrustManager == newTrustManager
post	init'ed(this.myTrustManager)

method	void setKeyManagers(KeyManager[])
post	this.myKeyManagers == newKeyManagers
post	init'ed(this.myKeyManagers)

method	RegexStringList getIgnoreList()
pre	init'ed(this.myIgnoreList)
post	return_value == this.myIgnoreList
post	init'ed(return_value)

method	void setIgnoreList(RegexStringList)
post	this.myIgnoreList == ignoreList
post	init'ed(this.myIgnoreList)

method	bool callServerError(String)
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that getCallbackType(...) != null

call too complex - analysis skipped Info call on bool call(Object[])

Prev Msg Next Msg

method	bool callDataIn(String)
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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

method	bool callDataOut(String, bool)
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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

method	bool callDebugInfo(int, String, Object[])
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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	bool callDebugInfo(int, String)
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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

method	bool callErrorInfo(ParserError)
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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

method	bool callConnectError(ParserError)
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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

method	bool callSocketClosed()
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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

method	bool callPingFailed()
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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

method	bool callPingSent()
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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

method	bool callPingSuccess()
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
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

method	bool callPost005()
pre	init'ed(this.post005)
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
post	this.post005 == 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
test_vector	this.post005: {0}, {1}

method	void resetState()
pre	init'ed(this.pingTimer)
pre	this.h005Info != null
pre	this.hChanModesBool != null
pre	this.hChanModesOther != null
pre	this.hChanPrefix != null
pre	this.hChannelList != null
pre	this.hClientList != null
pre	this.hPrefixMap != null
pre	this.hPrefixModes != null
pre	this.hUserModes != null
pre	this.pingTimerSem != null
post	this.cMyself == &new ClientInfo(resetState#1)
post	this.currentSocketState == &com.dmdirc.parser. irc.SocketState__static_init.new SocketState(Socket State__static_init#2)
post	this.got001 == 0
post	this.post005 == 0
post	this.triedAlt == 0
post	this.lastLine == &""
post	this.sNetworkName == &""
post	this.sServerName == &""
post	this.cMyself.myAwayReason == &""
post	this.cMyself.sRealName == &""
post	this.nNextKeyCMBool == 1
post	this.nNextKeyPrefix == 1
post	this.nNextKeyUser == 1
post	new ClientInfo(resetState#1) num objects == 1
post	this.cMyself.bIsFake == 1
post	new HashMap(ClientInfo#3) num objects == 1
post	new Hashtable(ClientInfo#1) num objects == 1
post	new IRCStringConverter(updateCharArrays#1) num objects == 1
post	new LinkedList(ClientInfo#2) num objects == 1
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#2) num objects == 1
post	this.pingTimer == null
post	this.stringConverter == &new IRCStringConverter (updateCharArrays#1)
post	this.cMyself.lModeQueue == &new LinkedList(ClientInfo#2)
post	this.cMyself.myChannelClientInfos == &new Hashtable(ClientInfo#1)
post	this.cMyself.myMap == &new HashMap(ClientInfo#3 )
post	this.cMyself.myParser == this
post	this.cMyself.myParser != null
post	this.cMyself.sHost == One-of{this.lastLine, undefined}
post	this.cMyself.sHost in Addr_Set{null,&""}
post	this.cMyself.sIdent == One-of{this.lastLine, undefined}
post	this.cMyself.sIdent in Addr_Set{null,&""}
post	this.cMyself.sNickname == undefined
post	this.cMyself.sNickname == null
post	new IRCStringConverter(updateCharArrays#1).limit == 4
post	new IRCStringConverter(updateCharArrays#1). lowercase == &new char[](IRCStringConverter#1)
post	new IRCStringConverter(updateCharArrays#1). uppercase == &new char[](IRCStringConverter#2)
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
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
test_vector	this.pingTimer: Addr_Set{null}, Inverse{null}

method	void onPostErrorInfo(ParserError, bool)
pre	errorInfo != null
pre	init'ed(errorInfo.errorLevel)
pre	(soft) init'ed(this.cMyself)
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) init'ed(this.pingTimer)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) init'ed(this.disconnectOnFatal)
post	this.cMyself == old this.cMyself
post	this.currentSocketState == old this. currentSocketState
post	this.got001 == old this.got001
post	this.lastLine == old this.lastLine
post	this.nNextKeyCMBool == old this.nNextKeyCMBool
post	this.nNextKeyPrefix == old this.nNextKeyPrefix
post	this.nNextKeyUser == old this.nNextKeyUser
post	this.pingTimer == old this.pingTimer
post	this.post005 == old this.post005
post	this.sNetworkName == old this.sNetworkName
post	this.sServerName == old this.sServerName
post	this.stringConverter == old this.stringConverter
post	this.triedAlt == old this.triedAlt
post	new IRCStringConverter(getIRCStringConverter#1) num objects == undefined
post	new IRCStringConverter(getIRCStringConverter#1) num objects == 0, if init'ed
post	new IRCStringConverter(getIRCStringConverter#1). limit == new IRCStringConverter(getIRCStringConvert er#1) num objects
post	new IRCStringConverter(updateCharArrays#1) num objects == new IRCStringConverter(getIRCStringConv erter#1) num objects
post	new IRCStringConverter(updateCharArrays#1).limit == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1).length == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1)[...] == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2).length == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2)[...] == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == undefined
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == null
post	new IRCStringConverter(getIRCStringConverter#1). uppercase == new IRCStringConverter(getIRCStringCon verter#1).lowercase
post	new IRCStringConverter(updateCharArrays#1). lowercase == new IRCStringConverter(getIRCStringCon verter#1).lowercase
post	new IRCStringConverter(updateCharArrays#1). uppercase == new IRCStringConverter(getIRCStringCon verter#1).lowercase
test_vector	errorInfo.errorLevel mod 2: {0}, {1}
test_vector	this.disconnectOnFatal: {0}, {1}

call too complex - analysis skipped Info call on void disconnect(String)

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

method	void setDisconnectOnFatal(bool)
post	this.disconnectOnFatal == newValue
post	init'ed(this.disconnectOnFatal)

method	void connect()
pre	init'ed(this.pingTimer)
pre	this.h005Info != null
pre	this.hChanModesBool != null
pre	this.hChanModesOther != null
pre	this.hChanPrefix != null
pre	this.hChannelList != null
pre	this.hClientList != null
pre	this.hPrefixMap != null
pre	this.hPrefixModes != null
pre	this.hUserModes != null
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
pre	this.pingTimerSem != null
pre	this.server != null
pre	init'ed(this.server.host)
pre	init'ed(this.server.isSSL)
pre	this.server.port in {1..2¹⁶-1}
pre	init'ed(this.server.useSocksProxy)
pre	(soft) init'ed(com/dmdirc/parser/irc/IRCAuthenticat or.me)
pre	(soft) init'ed(this.myTrustManager)
pre	(soft) this.socket != null
pre	(soft) init'ed(this.bindIP)
pre	(soft) init'ed(this.myKeyManagers)
pre	(soft) this.server.proxyHost != null
pre	(soft) init'ed(this.server.proxyPass)
pre	(soft) this.server.proxyPort in {1..2¹⁶-1}
pre	(soft) init'ed(this.server.proxyUser)
presumption	getIRCAuthenticator(...).replies != null
presumption	init'ed(java.net.Proxy$Type.SOCKS)
presumption	javax.net.ssl.SSLContext:getInstance(...)@680 != null
presumption	javax.net.ssl.SSLContext:getSocketFactory(...)@683 != null
presumption	javax.net.ssl.SSLSocketFactory:createSocket(... )@685 != null
presumption	javax.net.ssl.SSLSocketFactory:createSocket(... )@688 != null
presumption	javax.net.ssl.SSLSocketFactory:createSocket(... )@692 != null
presumption	javax.net.ssl.SSLSocketFactory:createSocket(... )@695 != null
post	com/dmdirc/parser/irc/IRCAuthenticator.me == One-of{old com/dmdirc/parser/irc/IRCAuthenticator. me, &new IRCAuthenticator(getIRCAuthenticator#1 )}
post	init'ed(com/dmdirc/parser/irc/IRCAuthenticator.me)
post	this.cMyself == &new ClientInfo(resetState#1)
post	this.currentSocketState in Addr_Set{&com. dmdirc.parser.irc.SocketState__static_init.new SocketState(SocketState__static_init#2),&com. dmdirc.parser.irc.SocketState__static_init.new SocketState(SocketState__static_init#3)}
post	this.got001 == 0
post	this.post005 == 0
post	this.triedAlt == 0
post	this.in == &new BufferedReader(connect#19)
post	this.lastLine == &""
post	this.sNetworkName == &""
post	this.sServerName == &""
post	new ClientInfo(resetState#1).myAwayReason == &""
post	new ClientInfo(resetState#1).sRealName == &""
post	this.myTrustManager == One-of{old this. myTrustManager, this.trustAllCerts}
post	init'ed(this.myTrustManager)
post	this.nNextKeyCMBool == 1
post	this.nNextKeyPrefix == 1
post	this.nNextKeyUser == 1
post	new ClientInfo(resetState#1) num objects == 1
post	new ClientInfo(resetState#1).bIsFake == 1
post	new HashMap(ClientInfo#3) num objects == 1
post	new Hashtable(ClientInfo#1) num objects == 1
post	new IRCStringConverter(updateCharArrays#1) num objects == 1
post	new LinkedList(ClientInfo#2) num objects == 1
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#2) num objects == 1
post	this.out == &new PrintWriter(connect#18)
post	this.pingTimer == null
post	this.socket != null
post	this.stringConverter == &new IRCStringConverter (updateCharArrays#1)
post	new BufferedReader(connect#19) num objects == 1
post	new ClientInfo(resetState#1).lModeQueue == &new LinkedList(ClientInfo#2)
post	new ClientInfo(resetState#1).myChannelClientInfos == &new Hashtable(ClientInfo#1)
post	new ClientInfo(resetState#1).myMap == &new HashMap(ClientInfo#3)
post	new ClientInfo(resetState#1).myParser == this
post	new ClientInfo(resetState#1).myParser != null
post	new ClientInfo(resetState#1).sHost == One-of{this.lastLine, undefined}
post	new ClientInfo(resetState#1).sHost in Addr_Set{null,&""}
post	new ClientInfo(resetState#1).sIdent == One-of{this.lastLine, undefined}
post	new ClientInfo(resetState#1).sIdent in Addr_Set{null,&""}
post	init'ed(new ClientInfo(resetState#1).sNickname)
post	new HashMap(IRCAuthenticator#1) num objects <= 1
post	new IRCAuthenticator(getIRCAuthenticator#1) num objects <= 1
post	init'ed(new IRCAuthenticator(getIRCAuthenticator#1) .replies)
post	new IRCStringConverter(updateCharArrays#1).limit == 4
post	new IRCStringConverter(updateCharArrays#1). lowercase == &new char[](IRCStringConverter#1)
post	new IRCStringConverter(updateCharArrays#1). uppercase == &new char[](IRCStringConverter#2)
post	new PrintWriter(connect#18) num objects == 1
post	new Socket(connect#10) num objects <= 1
post	new Socket(connect#6) num objects <= 1
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.Timer:cancel
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on java.util.Map:clear
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 com.dmdirc.parser.irc.ClientInfo
unanalyzed	call on setFake
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.net.Authenticator
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.net.Authenticator:setDefault
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.net.PasswordAuthentication
unanalyzed	call on java.util.Map:remove
unanalyzed	call on java.util.Map:put
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
test_vector	this.myTrustManager: Inverse{null}, Addr_Set{null}
test_vector	this.bindIP: Addr_Set{null}, Inverse{null}
test_vector	this.server.isSSL: {1}, {0}
test_vector	this.server.proxyUser: Addr_Set{null}, Inverse{null}
test_vector	this.server.useSocksProxy: {0}, {1}
test_vector	java.lang.String:isEmpty(...)@642: {1}, {0}
test_vector	java.lang.String:isEmpty(...)@652: {1}, {0}
test_vector	java.lang.String:isEmpty(...)@661: {1}, {0}
test_vector	java.lang.String:isEmpty(...)@687: {0}, {1}

method	void sendConnectionStrings()
pre	init'ed(this.me.nickname)
pre	init'ed(this.currentSocketState)
pre	this.me != null
pre	init'ed(this.me.realname)
pre	init'ed(this.me.username)
pre	this.server != null
pre	init'ed(this.server.host)
pre	this.server.password != null
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.cMyself.bIsFake)
pre	(soft) this.cMyself.sNickname != null
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
presumption	java.net.InetAddress:getLocalHost(...)@720 != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	this.me.nickname == old this.me.nickname
post	init'ed(this.me.nickname)
post	this.sThinkNickname == One-of{old this. sThinkNickname, old this.me.nickname}
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.stringConverter)
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	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.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on isFake
unanalyzed	call on getNickname
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	java.lang.String:isEmpty(...)@714: {1}, {0}

method	void handleConnectException(Exception)
pre	e != null
pre	init'ed(this.currentSocketState)
pre	init'ed(this.lastLine)
pre	init'ed(this.pingTimer)
pre	this.h005Info != null
pre	this.hChanModesBool != null
pre	this.hChanModesOther != null
pre	this.hChanPrefix != null
pre	this.hChannelList != null
pre	this.hClientList != null
pre	this.hPrefixMap != null
pre	this.hPrefixModes != null
pre	this.hUserModes != null
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
pre	this.pingTimerSem != null
post	this.cMyself == &new ClientInfo(resetState#1)
post	this.currentSocketState == &com.dmdirc.parser. irc.SocketState__static_init.new SocketState(Socket State__static_init#2)
post	this.got001 == 0
post	this.post005 == 0
post	this.triedAlt == 0
post	this.lastLine == &""
post	this.sNetworkName == &""
post	this.sServerName == &""
post	this.cMyself.myAwayReason == &""
post	this.cMyself.sRealName == &""
post	this.nNextKeyCMBool == 1
post	this.nNextKeyPrefix == 1
post	this.nNextKeyUser == 1
post	new ClientInfo(resetState#1) num objects == 1
post	this.cMyself.bIsFake == 1
post	new HashMap(ClientInfo#3) num objects == 1
post	new Hashtable(ClientInfo#1) num objects == 1
post	new IRCStringConverter(updateCharArrays#1) num objects == 1
post	new LinkedList(ClientInfo#2) num objects == 1
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#2) num objects == 1
post	this.pingTimer == null
post	this.stringConverter == &new IRCStringConverter (updateCharArrays#1)
post	this.cMyself.lModeQueue == &new LinkedList(ClientInfo#2)
post	this.cMyself.myChannelClientInfos == &new Hashtable(ClientInfo#1)
post	this.cMyself.myMap == &new HashMap(ClientInfo#3 )
post	this.cMyself.myParser == this
post	this.cMyself.myParser != null
post	this.cMyself.sHost == One-of{this.lastLine, undefined}
post	this.cMyself.sHost in Addr_Set{null,&""}
post	this.cMyself.sIdent == One-of{this.lastLine, undefined}
post	this.cMyself.sIdent in Addr_Set{null,&""}
post	this.cMyself.sNickname == undefined
post	this.cMyself.sNickname == null
post	this.stringConverter.limit == 4
post	this.stringConverter.lowercase == &new char[](IRCStringConverter#1)
post	this.stringConverter.uppercase == &new char[](IRCStringConverter#2)
post	this.stringConverter.lowercase.length == 127
post	this.stringConverter.uppercase.length == 127
post	possibly_updated(this.stringConverter.lowercase[...])
post	possibly_updated(this.stringConverter.uppercase[...])
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.Timer:cancel
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on java.util.Map:clear
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 com.dmdirc.parser.irc.ClientInfo
unanalyzed	call on setFake
unanalyzed	call on java.lang.Integer:valueOf
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

method	void run()
pre	init'ed(this.hasBegan)
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(com/dmdirc/parser/irc/IRCAuthenticat or.me)
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) init'ed(this.lastLine)
pre	(soft) this.lastPingValue != null
pre	(soft) init'ed(this.me.nickname)
pre	(soft) init'ed(this.myTrustManager)
pre	(soft) init'ed(this.pingTimer)
pre	(soft) this.socket != null
pre	(soft) init'ed(this...lastLine)
pre	(soft) this...myCallbackManager != null
pre	(soft) this...myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.bindIP)
pre	(soft) this.h005Info != null
pre	(soft) this.hChanModesBool != null
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChanPrefix != null
pre	(soft) this.hChannelList != null
pre	(soft) this.hClientList != null
pre	(soft) this.hPrefixMap != null
pre	(soft) this.hPrefixModes != null
pre	(soft) this.hUserModes != null
pre	(soft) this.me != null
pre	(soft) init'ed(this.me.realname)
pre	(soft) init'ed(this.me.username)
pre	(soft) init'ed(this.myKeyManagers)
pre	(soft) this.myProcessingManager != null
pre	(soft) this.myProcessingManager.myParser != null
pre	(soft) this.myProcessingManager.processHash != null
pre	(soft) this.pingNeeded != null
pre	(soft) init'ed(this.pingTime)
pre	(soft) this.pingTimerSem != null
pre	(soft) this.server != null
pre	(soft) init'ed(this.server.host)
pre	(soft) init'ed(this.server.isSSL)
pre	(soft) this.server.password != null
pre	(soft) this.server.port in {1..2¹⁶-1}
pre	(soft) this.server.proxyHost != null
pre	(soft) init'ed(this.server.proxyPass)
pre	(soft) this.server.proxyPort in {1..2¹⁶-1}
pre	(soft) init'ed(this.server.proxyUser)
pre	(soft) init'ed(this.server.useSocksProxy)
presumption	new ClientInfo(resetState#1).sNickname@754 != null
post	com/dmdirc/parser/irc/IRCAuthenticator.me == One-of{old com/dmdirc/parser/irc/IRCAuthenticator. me, &new IRCAuthenticator(getIRCAuthenticator#1 )}
post	init'ed(com/dmdirc/parser/irc/IRCAuthenticator.me)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(java.lang.String:substring(...)._ tainted)
post	this.cMyself == One-of{old this.cMyself, &new ClientInfo(resetState#1)}
post	init'ed(this.cMyself.myAwayReason)
post	this.currentSocketState == One-of{old this.currentSocketState, &com.dmdirc.parser. irc.SocketState__static_init.new SocketState(Socket State__static_init#2)}
post	init'ed(this.currentSocketState)
post	possibly_updated(this.got001)
post	this.hasBegan == 1
post	this.in == One-of{old this.in, &new BufferedReader(connect#19)}
post	this.lastLine == One-of{old this.lastLine, &""}
post	init'ed(this.lastLine)
post	possibly_updated(this.lastPingValue)
post	init'ed(this.me.nickname)
post	this.myTrustManager == One-of{old this. myTrustManager, this.trustAllCerts}
post	init'ed(this.myTrustManager)
post	this.nNextKeyCMBool == One-of{old this. nNextKeyCMBool, 1}
post	this.nNextKeyPrefix == One-of{old this. nNextKeyPrefix, 1}
post	this.nNextKeyUser == One-of{old this.nNextKeyUser, 1}
post	this.out == One-of{old this.out, &new PrintWriter(connect#18)}
post	this.pingTimer == One-of{old this.pingTimer, null}
post	init'ed(this.pingTimer)
post	possibly_updated(this.post005)
post	this.sNetworkName == One-of{old this.sNetworkName, &""}
post	this.sServerName == One-of{old this.sServerName, &""}
post	this.sThinkNickname == One-of{old this. sThinkNickname, old this.me.nickname}
post	possibly_updated(this.serverLag)
post	this.socket != null
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(update CharArrays#1)}
post	possibly_updated(this.triedAlt)
post	new BufferedReader(connect#19) num objects <= 1
post	new ClientInfo(resetState#1) num objects <= 1
post	init'ed(new ClientInfo(resetState#1).bIsFake)
post	init'ed(new ClientInfo(resetState#1).lModeQueue)
post	init'ed(new ClientInfo(resetState#1).myAwayReason)
post	possibly_updated(new ClientInfo(resetState#1). myAwayReason)
post	init'ed(new ClientInfo(resetState#1). myChannelClientInfos)
post	init'ed(new ClientInfo(resetState#1).myMap)
post	init'ed(new ClientInfo(resetState#1).myParser)
post	possibly_updated(new ClientInfo(resetState#1). sHost)
post	possibly_updated(new ClientInfo(resetState#1). sIdent)
post	possibly_updated(new ClientInfo(resetState#1). sNickname)
post	init'ed(new ClientInfo(resetState#1).sNickname)
post	init'ed(new ClientInfo(resetState#1).sRealName)
post	new HashMap(ClientInfo#3) num objects <= 1
post	new HashMap(IRCAuthenticator#1) num objects <= 1
post	new Hashtable(ClientInfo#1) num objects <= 1
post	new IRCAuthenticator(getIRCAuthenticator#1) num objects <= 1
post	init'ed(new IRCAuthenticator(getIRCAuthenticator#1) .replies)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	possibly_updated(new IRCStringConverter(getIRCStrin gConverter#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	new IRCStringConverter(updateCharArrays#1) num objects <= 1
post	init'ed(new IRCStringConverter(updateCharArrays#1). limit)
post	init'ed(new IRCStringConverter(updateCharArrays#1). lowercase)
post	init'ed(new IRCStringConverter(updateCharArrays#1). uppercase)
post	new LinkedList(ClientInfo#2) num objects <= 1
post	new PrintWriter(connect#18) num objects <= 1
post	new Socket(connect#10) num objects <= 1
post	new Socket(connect#6) num objects <= 1
post	new char[](IRCStringConverter#1) num objects <= 1
post	possibly_updated(new char[](IRCStringConverter#1) num objects)
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	possibly_updated(new char[](IRCStringConverter#2) num objects)
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	init'ed(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.concurrent.atomic. AtomicBoolean:set
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.Timer:cancel
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on isFake
unanalyzed	call on getNickname
unanalyzed	call on java.util.Map:clear
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on getCallbackType
unanalyzed	call on call
unanalyzed	call on callSocketClosed
unanalyzed	call on resetState
unanalyzed	call on callDebugInfo
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on callErrorInfo
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Exception:getMessage
unanalyzed	call on callConnectError
unanalyzed	call on java.io.IOException:getMessage
unanalyzed	call on com.dmdirc.parser.irc.ClientInfo
unanalyzed	call on setFake
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on callPingSuccess
unanalyzed	call on callServerError
unanalyzed	call on java.util.Hashtable:containsKey
unanalyzed	call on java.util.Hashtable:get
unanalyzed	call on java.lang.Exception
unanalyzed	call on getCallbackManager
unanalyzed	call on process
unanalyzed	call on getLastLine
unanalyzed	call on java.io.IOException
unanalyzed	call on java.net.InetSocketAddress
unanalyzed	call on java.net.Proxy
unanalyzed	call on java.net.Socket
unanalyzed	call on java.net.Authenticator
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.net.Authenticator:setDefault
unanalyzed	call on java.net.PasswordAuthentication
unanalyzed	call on java.util.Map:remove
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.net.Socket:connect
unanalyzed	call on java.net.InetAddress:getByName
unanalyzed	call on java.net.Socket:bind
unanalyzed	call on javax.net.ssl.SSLContext:getInstance
unanalyzed	call on java.security.SecureRandom
unanalyzed	call on javax.net.ssl.SSLContext:init
unanalyzed	call on javax.net.ssl.SSLContext:getSocketFactory
unanalyzed	call on javax.net.ssl.SSLSocketFactory:createSocket
unanalyzed	call on java.net.UnknownHostException:getMessage
unanalyzed	call on java.net.Socket:getOutputStream
unanalyzed	call on java.io.PrintWriter
unanalyzed	call on java.net.Socket:getInputStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on java.net.InetAddress:getLocalHost
unanalyzed	call on java.net.InetAddress:getHostAddress
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Hashtable
test_vector	this.hasBegan: {0}, {1}
test_vector	java.io.BufferedReader:readLine(...)@775: Inverse{null}, Addr_Set{null}

method	int getLocalPort()
pre	init'ed(this.currentSocketState)
pre	(soft) this.socket != null
post	init'ed(return_value)

method	void finalize()
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) this.socket != null
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	String getParam(String)
pre	(soft) line != null
post	return_value == undefined
post	return_value == null

Prev Msg Next Msg

array index out of bounds

click for all messages in this file High Prob.

check that (params.length - 1) >= 0

use of default init

Low Prob.

check if init'ed(params.length)

Prev Msg Next Msg

method	String[] tokeniseLine(String)
presumption	java.lang.String:indexOf(...)@848 <= 2³²-3
post	init'ed(java.lang.String:split(...)._tainted)
post	java.lang.String:split(...)[...] == null
post	init'ed(java.lang.String:substring(...)._tainted)
post	return_value in Addr_Set{&java.lang. String:split(...),&new String[](tokeniseLine#2) ,&new String[](tokeniseLine#1)}
post	new String[](tokeniseLine#1) num objects <= 1
post	new String[](tokeniseLine#1).length == 1
post	new String[](tokeniseLine#1)[0] == &""
post	new String[](tokeniseLine#2) num objects <= 1
post	new String[](tokeniseLine#2).length == 1
post	new String[](tokeniseLine#2)[...] == null
test_vector	line: Inverse{null}, Addr_Set{null}
test_vector	java.lang.String:indexOf(...)@848: {-2³¹. .-1}, {0..2³²-3}

Prev Msg Next Msg

use of default init

click for all messages in this file Low Prob.

check if init'ed(temp.length)

Prev Msg Next Msg

method	ClientInfo getClientInfo(String)
pre	init'ed(this.stringConverter)
pre	sHost != null
pre	this.hClientList != null
pre	(soft) this.stringConverter.lowercase != null
pre	(soft) init'ed(this.stringConverter.lowercase[...])
presumption	parseHost(...)@870 init'ed
post	init'ed(return_value)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	this.stringConverter != null
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). 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).length == 127
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
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
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
test_vector	java.util.Map:containsKey(...)@871: {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	ClientInfo getClientInfoOrFake(String)
pre	init'ed(this.stringConverter)
pre	sHost != null
pre	this.hClientList != null
pre	(soft) this.stringConverter.lowercase != null
pre	(soft) init'ed(this.stringConverter.lowercase[...])
presumption	parseHost(...)@882 init'ed
post	init'ed(return_value)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	this.stringConverter != null
post	new ClientInfo(getClientInfoOrFake#1) num objects <= 1
post	new ClientInfo(getClientInfoOrFake#1).bIsFake == 1
post	new ClientInfo(getClientInfoOrFake#1).lModeQueue == &new LinkedList(ClientInfo#2)
post	new ClientInfo(getClientInfoOrFake#1).myAwayReason == &""
post	new ClientInfo(getClientInfoOrFake#1). myChannelClientInfos == &new Hashtable(ClientIn fo#1)
post	new ClientInfo(getClientInfoOrFake#1).myMap == &new HashMap(ClientInfo#3)
post	new ClientInfo(getClientInfoOrFake#1).myParser == this
post	new ClientInfo(getClientInfoOrFake#1).myParser != null
post	new ClientInfo(getClientInfoOrFake#1).sHost in Addr_Set{null,&""}
post	new ClientInfo(getClientInfoOrFake#1).sIdent in Addr_Set{null,&""}
post	new ClientInfo(getClientInfoOrFake#1).sNickname == null
post	new ClientInfo(getClientInfoOrFake#1).sRealName == &""
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). 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).length == 127
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
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
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
test_vector	java.util.Map:containsKey(...)@883: {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	ChannelInfo getChannelInfo(String)
pre	init'ed(this.stringConverter)
pre	sWhat != null
pre	this.hChannelList != null
pre	(soft) this.stringConverter.lowercase != null
pre	(soft) init'ed(this.stringConverter.lowercase[...])
post	init'ed(return_value)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	this.stringConverter != null
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(...)@896: {0}, {1}

method	void sendLine(String)
pre	init'ed(this.out)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.stringConverter)
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	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	possibly_updated(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis

method	void sendString(String)
pre	init'ed(this.out)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.stringConverter)
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	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	possibly_updated(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis

method	void doSendString(String, bool)
pre	init'ed(this.out)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
presumption	channel.myParser.myCallbackManager.callbackHash@932 != null
presumption	channel.myParser.myCallbackManager@932 != null
presumption	channel.myParser@932 != null
presumption	java.util.Map:get(...)@938 != null
presumption	newLine.length in {1..2³²}
presumption	newLine[0] != null
presumption	newLine[1] != null
presumption	newLine[2] != null
presumption	this.stringConverter.lowercase@922 != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.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	init'ed(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
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 java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	this.out: Addr_Set{null}, Inverse{null}
test_vector	java.lang.Byte:byteValue(...)@938: {-128..0, 2..255}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@925: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@927: {0}, {1}
test_vector	java.util.LinkedList:contains(...)@939: {0}, {1}
test_vector	java.util.Map:containsKey(...)@938: {0}, {1}

Prev Msg Next Msg

unused assignment in callee

click for all messages in this file Low Prob.

Unused assignment to (java.lang.String:split(...)._ tainted) in tokeniseLine

Prev Msg Next Msg

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that newLine[0] != null

Prev Msg Next Msg

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that listModeQueue != null

Prev Msg Next Msg

method	String getNetworkName()
pre	init'ed(this.sNetworkName)
post	return_value == this.sNetworkName
post	init'ed(return_value)

method	String getServerName()
pre	init'ed(this.sServerName)
post	return_value == this.sServerName
post	init'ed(return_value)

method	String getLastLine()
pre	init'ed(this.lastLine)
post	return_value == this.lastLine
post	init'ed(return_value)

method	void processLine(String)
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
pre	this.pingNeeded != null
pre	(soft) this.lastPingValue != null
pre	(soft) init'ed(this.post005)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) init'ed(this...lastLine)
pre	(soft) this...myCallbackManager != null
pre	(soft) this...myCallbackManager.callbackHash != null
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) init'ed(this.got001)
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) init'ed(this.lastLine)
pre	(soft) this.myProcessingManager != null
pre	(soft) this.myProcessingManager.myParser != null
pre	(soft) this.myProcessingManager.processHash != null
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.pingTime)
presumption	java.lang.System:currentTimeMillis(...)@1002 - this.pingTime in {-2⁶³.. 2⁶⁴-1}
presumption	token.length <= 2³²-1
presumption	token[0] != null
presumption	token[1] != null
presumption	token[3] != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	possibly_updated(this.lastPingValue)
post	possibly_updated(this.post005)
post	possibly_updated(this.serverLag)
post	possibly_updated(this.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.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.concurrent.atomic. AtomicBoolean:set
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on getCallbackType
unanalyzed	call on call
unanalyzed	call on callErrorInfo
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.util.Hashtable:containsKey
unanalyzed	call on java.util.Hashtable:get
unanalyzed	call on java.lang.Exception
unanalyzed	call on getCallbackManager
unanalyzed	call on process
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Exception:getMessage
unanalyzed	call on getLastLine
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	this.post005: {1}, {0}
test_vector	this.got001: {0}, {1}
test_vector	java.lang.Integer:parseInt(...)@1018: {0..5}, {6..2³²-1}
test_vector	java.lang.String:charAt(...)@1037: {0, 2..2¹⁶-1}, {1}
test_vector	java.lang.String:equals(...)@1000: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@1005: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@1013: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@997: {1}, {0}
test_vector	java.lang.String:equalsIgnoreCase(...)@997: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@999: {1}, {0}
test_vector	java.lang.String:equalsIgnoreCase(...)@999: {0}, {1}
test_vector	java.lang.String:isEmpty(...)@1000: {1}, {0}
test_vector	java.lang.String:isEmpty(...)@1037: {1}, {0}

Prev Msg Next Msg

unused assignment in callee

click for all messages in this file Low Prob.

Unused assignment to (java.lang.String:split(...)._ tainted) in tokeniseLine

Prev Msg Next Msg

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that token[0] != null

Prev Msg Next Msg

method	IRCStringConverter getIRCStringConverter()
pre	init'ed(this.stringConverter)
post	return_value == One-of{old this.stringConverter, &new IRCStringConverter(getIRCStringConverter# 1)}
post	return_value != null
post	this.stringConverter == return_value
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)[...])
test_vector	this.stringConverter: Inverse{null}, Addr_Set{null}

method	void updateCharArrays(byte)
post	this.stringConverter == &new IRCStringConverter (updateCharArrays#1)
post	new IRCStringConverter(updateCharArrays#1) num objects == 1
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#2) num objects == 1
post	this.stringConverter.limit == One-of{4, limit}
post	this.stringConverter.limit in {0..4}
post	this.stringConverter.lowercase == &new char[](IRCStringConverter#1)
post	this.stringConverter.uppercase == &new char[](IRCStringConverter#2)
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])

method	String getBoolChanModes005()
pre	this.hChanModesBool != null
presumption	(int) (java.lang.Math:log(...)@1108/java.lang. Math:log(...)@1108) in {0..2³²-2}
presumption	java.lang.Math:log(...)@1108 != +0
presumption	java.util.Iterator:next(...)@1104 != null
presumption	java.util.Map:get(...)@1105 != null
presumption	java.util.Map:keySet(...)@1104 != null
presumption	java.util.Map:size(...)@1100 >= 1
presumption	java.util.Map:size(...)@1100 - (int) (java.lang.Math:log(...)@1108/java.lang.Math:log(. ..)@1108) in {1..2³²-1}
post	return_value == &new String(getBoolChanModes005 #2)
post	new String(getBoolChanModes005#2) num objects == 1
test_vector	java.lang.Long:longValue(...)@1105: {-2⁶³..0}, {1.. 2⁶⁴-1}
test_vector	java.util.Iterator:hasNext(...)@1104: {0}, {1}

method	void parseChanModes()
pre	this.h005Info != null
pre	this.hChanModesBool != null
pre	this.hChanModesOther != null
pre	init'ed(this.lastLine)
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
pre	(soft) this.hPrefixModes != null
pre	(soft) this.sNetworkName != null
presumption	java.lang.String:length(...)@1175 >= 1
presumption	java.lang.String:length(...)@1182 >= 1
presumption	java.lang.String:length(...)@1189 >= 1
presumption	java.util.Map:get(...)@1136 != null
presumption	java.util.Map:get(...)@1148 != null
post	this.nNextKeyCMBool <= 2⁶⁴-2
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: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
test_vector	java.lang.String:equalsIgnoreCase(...)@1131: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@1133: {0}, {1}
test_vector	java.lang.StringBuilder:indexOf(...)@1140: {0..2³²-1}, {-2³¹..-1}
test_vector	java.util.Map:containsKey(...)@1130: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1140: {1}, {0}
test_vector	java.util.Map:containsKey(...)@1147: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1170: {1}, {0}
test_vector	java.util.Map:containsKey(...)@1178: {1}, {0}
test_vector	java.util.Map:containsKey(...)@1185: {1}, {0}
test_vector	java.util.Map:containsKey(...)@1192: {1}, {0}

Prev Msg Next Msg

use of default init

click for all messages in this file Low Prob.

check if init'ed(bits.length)

test always goes same way

Low Prob.

Test predetermined because bits.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(bits[0])

use of default init

Low Prob.

check if init'ed(bits.length)

Prev Msg Next Msg

Prev Msg Next Msg

array index out of bounds

click for all messages in this file High Prob.

check that bits.length >= 2

null dereference

Medium Prob.

check that not_init'ed(bits[1])

use of default init

Low Prob.

check if init'ed(bits.length)

use of default init

click for all messages in this file Low Prob.

check if init'ed(i)

Prev Msg Next Msg

Prev Msg Next Msg

array index out of bounds

click for all messages in this file Medium Prob.

check that bits.length >= 2

null dereference

Medium Prob.

check that not_init'ed(bits[1])

use of default init

Low Prob.

check if init'ed(bits.length)

use of default init

click for all messages in this file Low Prob.

check if init'ed(i)

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(new__parseChanModes:Object_array_ _5.length)

Prev Msg Next Msg

Prev Msg Next Msg

array index out of bounds

click for all messages in this file High Prob.

check that bits.length >= 3

null dereference

Medium Prob.

check that not_init'ed(bits[2])

use of default init

Low Prob.

check if init'ed(bits.length)

use of default init

click for all messages in this file Low Prob.

check if init'ed(i)

Prev Msg Next Msg

Prev Msg Next Msg

array index out of bounds

click for all messages in this file Medium Prob.

check that bits.length >= 3

null dereference

Medium Prob.

check that not_init'ed(bits[2])

use of default init

Low Prob.

check if init'ed(bits.length)

use of default init

click for all messages in this file Low Prob.

check if init'ed(i)

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(new__parseChanModes:Object_array_ _6.length)

Prev Msg Next Msg

Prev Msg Next Msg

array index out of bounds

click for all messages in this file High Prob.

check that bits.length >= 4

null dereference

Medium Prob.

check that not_init'ed(bits[3])

use of default init

Low Prob.

check if init'ed(bits.length)

use of default init

click for all messages in this file Low Prob.

check if init'ed(i)

Prev Msg Next Msg

Prev Msg Next Msg

array index out of bounds

click for all messages in this file Medium Prob.

check that bits.length >= 4

null dereference

Medium Prob.

check that not_init'ed(bits[3])

use of default init

Low Prob.

check if init'ed(bits.length)

use of default init

click for all messages in this file Low Prob.

check if init'ed(i)

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(new__parseChanModes:Object_array_ _7.length)

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(this.nNextKeyCMBool)

Prev Msg Next Msg

method	String getPrefixModes()
pre	this.h005Info != null
post	init'ed(return_value)
test_vector	java.util.Map:containsKey(...)@1205: {0}, {1}

method	String getBoolChanModes()
pre	this.hChanModesBool != null
presumption	java.util.Iterator:next(...)@1221 != null
presumption	java.util.Map:keySet(...)@1221 != null
presumption	java.util.Map:size(...)@1219 >= 1
post	return_value == &new String(getBoolChanModes#2)
post	new String(getBoolChanModes#2) num objects == 1
test_vector	java.util.Iterator:hasNext(...)@1221: {0}, {1}

Prev Msg Next Msg

array index out of bounds

click for all messages in this file Medium Prob.

check that i < modes.length

overflow

Low Prob.

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

Prev Msg Next Msg

method	String getListChanModes()
pre	this.hChanModesOther != null
post	return_value != null
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:size
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Arrays:sort
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.String:trim

method	String getSetOnlyChanModes()
pre	this.hChanModesOther != null
post	return_value != null
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:size
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Arrays:sort
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.String:trim

method	String getSetUnsetChanModes()
pre	this.hChanModesOther != null
post	return_value != null
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:size
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Arrays:sort
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.String:trim

method	String getOtherModeString(byte)
pre	this.hChanModesOther != null
presumption	java.util.Iterator:next(...)@1270 != null
presumption	java.util.Map:get(...)@1271 != null
presumption	java.util.Map:keySet(...)@1270 != null
presumption	java.util.Map:size(...)@1267 >= 1
post	return_value != null
test_vector	java.util.Iterator:hasNext(...)@1270: {0}, {1}

method	String getUserModeString()
pre	this.h005Info != null
post	init'ed(return_value)
test_vector	java.util.Map:containsKey(...)@1286: {0}, {1}

method	void parseUserModes()
pre	this.h005Info != null
pre	this.hUserModes != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
presumption	java.util.Map:get(...)@1300 != null
post	this.nNextKeyUser <= 2⁶⁴-2
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 callDebugInfo
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.Integer:valueOf
test_vector	java.util.Map:containsKey(...)@1299: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1314: {1}, {0}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into sDefaultModes

Prev Msg Next Msg

method	void parseChanPrefix()
pre	this.h005Info != null
pre	this.hChanPrefix != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
presumption	java.util.Map:get(...)@1328 != null
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 callDebugInfo
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.Integer:valueOf
test_vector	java.util.Map:containsKey(...)@1327: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1341: {1}, {0}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into sDefaultModes

Prev Msg Next Msg

method	void parsePrefixModes()
pre	this.h005Info != null
pre	this.hPrefixMap != null
pre	this.hPrefixModes != null
pre	init'ed(this.lastLine)
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
presumption	java.util.Map:get(...)@1353 != null
post	this.nNextKeyPrefix <= 2⁶⁴-2
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 callDebugInfo
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.Integer:valueOf
test_vector	java.lang.String:equals(...)@1357: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1352: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1382: {1}, {0}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into sDefaultModes

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(this.nNextKeyPrefix)

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(bits.length)

Prev Msg Next Msg

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

method	void joinChannel(String)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.cMyself.sNickname)
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.h005Info != null
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChanPrefix != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.sThinkNickname)
post	possibly_updated(java.lang.String:substring(...)._ tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	init'ed(this.stringConverter)
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	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	possibly_updated(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on isFake
unanalyzed	call on getNickname
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.String: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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.util.Map:isEmpty
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis

method	void joinChannel(String, bool)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.cMyself.sNickname)
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.h005Info != null
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChanPrefix != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.sThinkNickname)
post	possibly_updated(java.lang.String:substring(...)._ tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	init'ed(this.stringConverter)
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	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	possibly_updated(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on isFake
unanalyzed	call on getNickname
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.String: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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.util.Map:isEmpty
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis

method	void joinChannel(String, String)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) sKey != null
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.cMyself.sNickname)
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.h005Info != null
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChanPrefix != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.sThinkNickname)
post	possibly_updated(java.lang.String:substring(...)._ tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	init'ed(this.stringConverter)
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	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	possibly_updated(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on isFake
unanalyzed	call on getNickname
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.String: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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.util.Map:isEmpty
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis

method	void joinChannel(String, String, bool)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) sKey != null
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.cMyself.sNickname)
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.h005Info != null
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChanPrefix != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.sThinkNickname)
presumption	java.util.Map:get(...)@1447 != null
post	possibly_updated(java.lang.String:substring(...)._ tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	init'ed(this.stringConverter)
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	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.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on isFake
unanalyzed	call on getNickname
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
unanalyzed	call on java.lang.String: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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.util.Map:isEmpty
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	autoPrefix: {0}, {1}
test_vector	java.lang.String:isEmpty(...)@1448: {0}, {1}
test_vector	java.lang.String:isEmpty(...)@1460: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1446: {0}, {1}

method	void partChannel(String, String)
pre	init'ed(this.stringConverter)
pre	sChannelName != null
pre	this.hChannelList != null
pre	(soft) sReason != null
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.hChanModesOther != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
pre	(soft) this.stringConverter.lowercase != null
pre	(soft) init'ed(this.stringConverter.lowercase[...])
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	this.stringConverter != null
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	init'ed(new IRCStringConverter(getIRCStringConverte r#1).limit)
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == &new char[](IRCStringConverter#1)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).lowercase)
post	new IRCStringConverter(getIRCStringConverter#1). uppercase == &new char[](IRCStringConverter#2)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).uppercase)
post	new char[](IRCStringConverter#1) num objects == 0
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2).length == 127
post	init'ed(new char[](IRCStringConverter#1).length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects == 0
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	java.lang.String:isEmpty(...)@1475: {0}, {1}

method	void setNickname(String)
pre	init'ed(this.currentSocketState)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.cMyself.bIsFake)
pre	(soft) this.cMyself.sNickname != null
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.me != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	this.me.nickname == One-of{old this.me.nickname, sNewNickName}
post	this.sThinkNickname == One-of{old this. sThinkNickname, sNewNickName}
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.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.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	this.cMyself.bIsFake: {1}, {0}
test_vector	java.lang.String:equals(...)@1489: {0}, {1}

method	int getMaxLength(String, String)
pre	this.cMyself != null
pre	init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.cMyself.sHost)
pre	(soft) init'ed(this.cMyself.sIdent)
pre	(soft) init'ed(this.cMyself.sNickname)
pre	(soft) init'ed(this.lastLine)
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
presumption	java.lang.String:length(...)@1512 <= 2_147_484_153
presumption	java.lang.String:length(...)@1513 <= 2_147_484_153
presumption	java.lang.String:length(...)@1513 + length in {0..2_147_484_153}
post	return_value <= 2_147_484_153
unanalyzed	call on isFake
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.String:length
unanalyzed	call on toString
test_vector	sTarget: Addr_Set{null}, Inverse{null}
test_vector	sType: Addr_Set{null}, Inverse{null}

method	int getMaxLength(int)
pre	nLength <= 2_147_484_153
pre	this.cMyself != null
pre	init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.cMyself.sHost)
pre	(soft) init'ed(this.cMyself.sIdent)
pre	(soft) init'ed(this.cMyself.sNickname)
pre	(soft) init'ed(this.lastLine)
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
presumption	nLength + java.lang.String:length(...)@1529 in {-2³¹..2_147_484_153}
presumption	toString(...)@1529 init'ed
post	return_value <= 2_147_484_153
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
test_vector	this.cMyself.bIsFake: {0}, {1}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into lineLint

Prev Msg Next Msg

method	int getMaxListModes(char)
pre	this.h005Info != null
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.lastLine)
pre	(soft) this.sNetworkName != null
presumption	java.util.Map:get(...)@1555 != null
post	init'ed(return_value)
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
test_vector	java.lang.String:equalsIgnoreCase(...)@1577: {0}, {1}
test_vector	java.util.Map:get(...)@1551: Addr_Set{null}, Inverse{null}
test_vector	java.util.Map:get(...)@1552: Inverse{null}, Addr_Set{null}
test_vector	java.util.Map:get(...)@1572: Addr_Set{null}, Inverse{null}

Prev Msg Next Msg

use of default init

click for all messages in this file Low Prob.

check if init'ed(arr$.length)

use of default init

Low Prob.

check if init'ed(len$)

test always goes same way

Low Prob.

Test predetermined because i$ == len$

dead code

click for all messages in this file Low Prob.

Dead code here because i$ == len$

dead code continues Info Dead code continues

Prev Msg Next Msg

dead code continues Info Dead code continues

method	void sendMessage(String, String)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.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.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	sMessage: Inverse{null}, Addr_Set{null}
test_vector	sTarget: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:isEmpty(...)@1597: {0}, {1}

method	void sendNotice(String, String)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.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.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	sMessage: Inverse{null}, Addr_Set{null}
test_vector	sTarget: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:isEmpty(...)@1610: {0}, {1}

method	void sendAction(String, String)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.stringConverter)
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	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	possibly_updated(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:toUpperCase
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis

method	void sendCTCP(String, String, String)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) sType != null
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
post	init'ed(java.lang.String:substring(...)._tainted)
post	possibly_updated(this.cMyself.myAwayReason)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.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.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	sMessage: Inverse{null}, Addr_Set{null}
test_vector	sTarget: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:isEmpty(...)@1634: {1}, {0}
test_vector	java.lang.String:isEmpty(...)@1634: {0}, {1}

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

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

method	void disconnect(String)
pre	init'ed(this.currentSocketState)
pre	init'ed(this.pingTimer)
pre	this.h005Info != null
pre	this.hChanModesBool != null
pre	this.hChanModesOther != null
pre	this.hChanPrefix != null
pre	this.hChannelList != null
pre	this.hClientList != null
pre	this.hPrefixMap != null
pre	this.hPrefixModes != null
pre	this.hUserModes != null
pre	this.pingTimerSem != null
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.got001)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) sReason != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.socket)
post	init'ed(java.lang.String:substring(...)._tainted)
post	this.cMyself in Addr_Set{&new ClientInfo(resetS tate#1),&new ClientInfo(resetState#1)}
post	possibly_updated(this.cMyself.myAwayReason)
post	this.currentSocketState == &com.dmdirc.parser. irc.SocketState__static_init.new SocketState(Socket State__static_init#2)
post	this.got001 == 0
post	this.lastLine == &""
post	this.nNextKeyCMBool == 1
post	this.nNextKeyPrefix == 1
post	this.nNextKeyUser == 1
post	this.pingTimer == null
post	this.post005 == 0
post	this.sNetworkName == &""
post	this.sServerName == &""
post	this.stringConverter in Addr_Set{&new IRCStringConverter(updateCharArrays#1),&new IRCStringConverter(updateCharArrays#1)}
post	this.triedAlt == 0
post	new ClientInfo(resetState#1) num objects <= 1
post	new ClientInfo(resetState#1) num objects == 0
post	new HashMap(ClientInfo#3) num objects == 0
post	new Hashtable(ClientInfo#1) num objects == 0
post	new IRCStringConverter(updateCharArrays#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	init'ed(new ClientInfo(resetState#1).bIsFake)
post	init'ed(new ClientInfo(resetState#1).lModeQueue)
post	init'ed(new ClientInfo(resetState#1).myAwayReason)
post	init'ed(new ClientInfo(resetState#1). myChannelClientInfos)
post	init'ed(new ClientInfo(resetState#1).myMap)
post	init'ed(new ClientInfo(resetState#1).myParser)
post	possibly_updated(new ClientInfo(resetState#1). sHost)
post	init'ed(new ClientInfo(resetState#1).sHost)
post	possibly_updated(new ClientInfo(resetState#1). sIdent)
post	init'ed(new ClientInfo(resetState#1).sIdent)
post	possibly_updated(new ClientInfo(resetState#1). sNickname)
post	init'ed(new ClientInfo(resetState#1).sNickname)
post	init'ed(new ClientInfo(resetState#1).sRealName)
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	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 IRCStringConverter(updateCharArrays#1) num objects <= 1
post	init'ed(new IRCStringConverter(updateCharArrays#1). limit)
post	init'ed(new IRCStringConverter(updateCharArrays#1). lowercase)
post	init'ed(new IRCStringConverter(updateCharArrays#1). uppercase)
post	new LinkedList(ClientInfo#2) num objects <= 1
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)[...])
post	init'ed(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.Timer:cancel
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.util.Map:clear
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
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 sendString
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on com.dmdirc.parser.irc.ClientInfo
unanalyzed	call on setFake
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	this.got001: {0}, {1}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into e

Prev Msg Next Msg

method	bool isValidChannelName(String)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.cMyself.sNickname)
pre	(soft) this.hChanPrefix != null
pre	(soft) this.hChannelList != null
pre	(soft) init'ed(this.sThinkNickname)
presumption	getIRCStringConverter(...).lowercase.length@1702 >= 1
presumption	getIRCStringConverter(...).lowercase@1702 != null
post	init'ed(return_value)
post	init'ed(this.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	new IRCStringConverter(getIRCStringConverter#1) num objects == 0
post	new IRCStringConverter(getIRCStringConverter#1). limit == 4
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).limit)
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == &new char[](IRCStringConverter#1)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).lowercase)
post	new IRCStringConverter(getIRCStringConverter#1). uppercase == &new char[](IRCStringConverter#2)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).uppercase)
post	new char[](IRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#1) num objects == 0
post	new char[](IRCStringConverter#1).length == 127
post	init'ed(new char[](IRCStringConverter#1).length)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2) num objects == 0
post	new char[](IRCStringConverter#2).length == 127
post	init'ed(new char[](IRCStringConverter#2).length)
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on isFake
unanalyzed	call on getNickname
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
test_vector	sChannelName: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:isEmpty(...)@1700: {0}, {1}
test_vector	java.util.Map:isEmpty(...)@1706: {0}, {1}

method	bool isUserSettable(Character)
pre	this.h005Info != null
presumption	java.util.Map:get(...)@1726 != null
post	init'ed(return_value)
test_vector	java.util.Map:containsKey(...)@1725: {0}, {1}

method	Map get005()
post	return_value == this.h005Info
post	init'ed(return_value)

method	String getIRCD(bool)
pre	this.h005Info != null
pre	(soft) this.sNetworkName != null
presumption	java.util.Map:get(...)@1748 != null
presumption	java.util.Map:get(...)@1784 != null
post	return_value != null
test_vector	getType: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@1781: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@1782: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@1783: {0}, {1}
test_vector	java.lang.String:matches(...)@1752: {0}, {1}
test_vector	java.lang.String:matches(...)@1753: {0}, {1}
test_vector	java.lang.String:matches(...)@1754: {0}, {1}
test_vector	java.lang.String:matches(...)@1755: {0}, {1}
test_vector	java.lang.String:matches(...)@1756: {0}, {1}
test_vector	java.lang.String:matches(...)@1757: {0}, {1}
test_vector	java.lang.String:matches(...)@1758: {0}, {1}
test_vector	java.lang.String:matches(...)@1759: {0}, {1}
test_vector	java.lang.String:matches(...)@1760: {0}, {1}
test_vector	java.lang.String:matches(...)@1761: {0}, {1}
test_vector	java.lang.String:matches(...)@1762: {0}, {1}
test_vector	java.lang.String:matches(...)@1763: {0}, {1}
test_vector	java.lang.String:matches(...)@1764: {0}, {1}
test_vector	java.lang.String:matches(...)@1765: {0}, {1}
test_vector	java.lang.String:matches(...)@1766: {0}, {1}
test_vector	java.lang.String:matches(...)@1767: {0}, {1}
test_vector	java.lang.String:matches(...)@1768: {0}, {1}
test_vector	java.lang.String:matches(...)@1769: {0}, {1}
test_vector	java.lang.String:matches(...)@1770: {0}, {1}
test_vector	java.lang.String:matches(...)@1771: {0}, {1}
test_vector	java.lang.String:matches(...)@1772: {0}, {1}
test_vector	java.lang.String:matches(...)@1773: {0}, {1}
test_vector	java.lang.String:matches(...)@1774: {0}, {1}
test_vector	java.lang.String:matches(...)@1775: {0}, {1}
test_vector	java.lang.String:matches(...)@1776: {0}, {1}
test_vector	java.lang.String:matches(...)@1777: {0}, {1}
test_vector	java.lang.String:matches(...)@1778: {0}, {1}
test_vector	java.lang.String:matches(...)@1784: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1747: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1784: {0}, {1}

method	long getPingTimerLength()
pre	init'ed(this.pingTimerLength)
post	return_value == this.pingTimerLength
post	init'ed(return_value)

method	void setPingTimerLength(long)
pre	init'ed(this.pingTimer)
pre	this.pingNeeded != null
pre	this.pingTimerSem != null
post	this.pingCountDown == 1
post	new Timer(startPingTimer#1) num objects == 1
post	this.pingTimer == &new Timer(startPingTimer#1)
post	this.pingTimerLength == newValue
post	init'ed(this.pingTimerLength)
unanalyzed	call on java.util.concurrent.atomic. AtomicBoolean:set
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.Timer:cancel
unanalyzed	call on java.util.Timer
unanalyzed	call on java.util.TimerTask
unanalyzed	call on java.util.Timer:schedule
unanalyzed	call on java.util.concurrent.Semaphore:release

method	int getPingCountDownLength()
pre	init'ed(this.pingCountDownLength)
post	return_value == this.pingCountDownLength
post	init'ed(return_value)

method	void setPingCountDownLength(int)
post	this.pingCountDownLength == newValue
post	init'ed(this.pingCountDownLength)

method	void startPingTimer()
pre	init'ed(this.pingTimer)
pre	this.pingNeeded != null
pre	init'ed(this.pingTimerLength)
pre	this.pingTimerSem != null
post	this.pingCountDown == 1
post	new Timer(startPingTimer#1) num objects == 1
post	this.pingTimer == &new Timer(startPingTimer#1)
unanalyzed	call on java.util.concurrent.atomic. AtomicBoolean:set
unanalyzed	call on java.util.TimerTask
test_vector	this.pingTimer: Addr_Set{null}, Inverse{null}

method	void pingTimerTask(Timer)
pre	this.pingNeeded != null
pre	(soft) this.cMyself != null
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) this.pingCountDown >= -2³¹+1
pre	(soft) init'ed(this.pingTimer)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.pingCountDownLength)
pre	(soft) this.pingTimerSem != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	java.lang.String:valueOf(...)._tainted == 0
post	this.cMyself == old this.cMyself
post	this.cMyself != null
post	possibly_updated(this.cMyself.myAwayReason)
post	this.currentSocketState == old this. currentSocketState
post	init'ed(this.currentSocketState)
post	this.got001 == old this.got001
post	this.lastLine == old this.lastLine
post	this.lastPingValue == One-of{old this. lastPingValue, &java.lang.String:valueOf(...)}
post	this.nNextKeyCMBool == old this.nNextKeyCMBool
post	this.nNextKeyPrefix == old this.nNextKeyPrefix
post	this.nNextKeyUser == old this.nNextKeyUser
post	this.pingCountDown == One-of{old this. pingCountDown, old this.pingCountDown - 1, this.pingCountDownLength}
post	init'ed(this.pingCountDown)
post	possibly_updated(this.pingTime)
post	this.pingTimer == old this.pingTimer
post	init'ed(this.pingTimer)
post	this.post005 == old this.post005
post	this.sNetworkName == old this.sNetworkName
post	this.sServerName == old this.sServerName
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.stringConverter)
post	this.triedAlt == old this.triedAlt
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	new IRCStringConverter(getIRCStringConverter#1) num objects == undefined
post	new IRCStringConverter(getIRCStringConverter#1) num objects == 0, if init'ed
post	new IRCStringConverter(getIRCStringConverter#1). limit == new IRCStringConverter(getIRCStringConvert er#1) num objects
post	new IRCStringConverter(updateCharArrays#1) num objects == new IRCStringConverter(getIRCStringConv erter#1) num objects
post	new IRCStringConverter(updateCharArrays#1).limit == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1).length == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1)[...] == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2).length == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2)[...] == new IRCStringConverter(getIRCStringConverter#1) num objects
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).limit)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).lowercase)
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == undefined
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == null
post	new IRCStringConverter(getIRCStringConverter#1). uppercase == new IRCStringConverter(getIRCStringCon verter#1).lowercase
post	new IRCStringConverter(updateCharArrays#1). lowercase == new IRCStringConverter(getIRCStringCon verter#1).lowercase
post	new IRCStringConverter(updateCharArrays#1). uppercase == new IRCStringConverter(getIRCStringCon verter#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.concurrent.atomic. AtomicBoolean:get
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.concurrent.atomic. AtomicBoolean:set
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on doSendString
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:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on setAwayReason
unanalyzed	call on java.util.LinkedList
unanalyzed	call on getListModeQueue
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.lang.System:currentTimeMillis
test_vector	this.pingCountDown: {2..2³²-1}, {-2³¹+1..1}
test_vector	this.pingTimer: Addr_Set{null}, Inverse{null}
test_vector	call(...)@519: {1}, {0}
test_vector	java.lang.Object:equals(...)@1879: {0}, {1}
test_vector	java.util.concurrent.atomic.AtomicBoolean:get(... )@1935: {0}, {1}

call too complex - analysis skipped Info call on void disconnect(String)

method	long getServerLag()
pre	init'ed(this.serverLag)
post	return_value == this.serverLag
post	init'ed(return_value)

method	long getPingTime(bool)
pre	init'ed(this.pingTime)
presumption	java.lang.System:currentTimeMillis(...)@1917 - this.pingTime in {-2⁶³.. 2⁶⁴-1}
post	init'ed(return_value)
test_vector	actualTime: {0}, {1}

method	void setPingNeeded(bool)
pre	this.pingNeeded != null

method	bool getPingNeeded()
pre	this.pingNeeded != null
post	init'ed(return_value)

method	ClientInfo getMyself()
pre	init'ed(this.cMyself)
post	return_value == this.cMyself
post	init'ed(return_value)

method	String getMyNickname()
pre	this.cMyself != null
pre	init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.cMyself.sNickname)
pre	(soft) init'ed(this.sThinkNickname)
post	return_value == One-of{this.sThinkNickname, this.cMyself.sNickname}
post	init'ed(return_value)
test_vector	this.cMyself.bIsFake: {0}, {1}

method	String getMyUsername()
pre	this.me != null
pre	init'ed(this.me.username)
post	return_value == this.me.username
post	init'ed(return_value)

method	void addClient(ClientInfo)
pre	client != null
pre	client.sNickname != null
pre	init'ed(this.stringConverter)
pre	this.hClientList != null
pre	(soft) this.stringConverter.lowercase != null
pre	(soft) init'ed(this.stringConverter.lowercase[...])
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	this.stringConverter != null
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). 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).length == 127
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
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

method	void removeClient(ClientInfo)
pre	init'ed(this.cMyself)
pre	(soft) client != null
pre	(soft) client.sNickname != null
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.hClientList != null
pre	(soft) this.stringConverter.lowercase != null
pre	(soft) init'ed(this.stringConverter.lowercase[...])
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	init'ed(this.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 getNickname
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
test_vector	client == this.cMyself: {1}, {0}

method	void forceRemoveClient(ClientInfo)
pre	client != null
pre	client.sNickname != null
pre	init'ed(this.stringConverter)
pre	this.hClientList != null
pre	(soft) this.stringConverter.lowercase != null
pre	(soft) init'ed(this.stringConverter.lowercase[...])
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	this.stringConverter != null
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). 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).length == 127
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
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

method	int knownClients()
pre	this.hClientList != null
post	init'ed(return_value)

method	Collection getClients()
pre	this.hClientList != null
post	init'ed(return_value)

method	void clearClients()
pre	init'ed(this.stringConverter)
pre	this.cMyself != null
pre	this.cMyself.sNickname != null
pre	this.hClientList != null
pre	(soft) this.stringConverter.lowercase != null
pre	(soft) init'ed(this.stringConverter.lowercase[...])
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	this.stringConverter != null
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). 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).length == 127
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on getNickname
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:put

method	void addChannel(ChannelInfo)
pre	channel != null
pre	channel.sName != null
pre	init'ed(this.stringConverter)
pre	this.hChannelList != null
pre	(soft) this.stringConverter.lowercase != null
pre	(soft) init'ed(this.stringConverter.lowercase[...])
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	this.stringConverter != null
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

method	void removeChannel(ChannelInfo)
pre	channel != null
pre	channel.sName != null
pre	init'ed(this.stringConverter)
pre	this.hChannelList != null
pre	(soft) this.stringConverter.lowercase != null
pre	(soft) init'ed(this.stringConverter.lowercase[...])
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
post	this.stringConverter != null
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

method	int knownChannels()
pre	this.hChannelList != null
post	init'ed(return_value)

method	Collection getChannels()
pre	this.hChannelList != null
post	init'ed(return_value)

method	void clearChannels()
pre	this.hChannelList != null