IRCParser.java

IRCParser.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void addChannel(ChannelInfo)

Kind	Annotation Text
pre	(soft) init'ed(this.stringConverter.lowercase[...])
pre	(soft) this.stringConverter.lowercase != null
pre	channel != null
pre	channel.sName != null
pre	init'ed(this.stringConverter)
pre	this.hChannelList != 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	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.stringConverter != null
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray

void addClient(ClientInfo)

Kind	Annotation Text
pre	(soft) init'ed(this.stringConverter.lowercase[...])
pre	(soft) this.stringConverter.lowercase != null
pre	client != null
pre	client.sNickname != null
pre	init'ed(this.stringConverter)
pre	this.hClientList != 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 == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.stringConverter != null
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray

bool callConnectError(ParserError)

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

bool callDataIn(String)

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

bool callDataOut(String, bool)

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

bool callDebugInfo(int, String)

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

bool callDebugInfo(int, String, Object[])

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

bool callErrorInfo(ParserError)

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

bool callPingFailed()

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

bool callPingSent()

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

bool callPingSuccess()

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

bool callPost005()

Kind	Annotation Text
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	init'ed(this.post005)
post	init'ed(return_value)
post	this.post005 == 1
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
test_vector	this.post005: {0}, {1}

bool callServerError(String)

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

bool callSocketClosed()

Kind	Annotation Text
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
post	init'ed(return_value)
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

void checkClientTrusted(X509Certificate[], String)

Kind	Annotation Text

void checkServerTrusted(X509Certificate[], String)

Kind	Annotation Text

void clearChannels()

Kind	Annotation Text
pre	this.hChannelList != null

void clearClients()

Kind	Annotation Text
pre	(soft) init'ed(this.stringConverter.lowercase[...])
pre	(soft) this.stringConverter.lowercase != null
pre	init'ed(this.stringConverter)
pre	this.cMyself != null
pre	this.cMyself.sNickname != null
pre	this.hClientList != 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 == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.stringConverter != null
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
unanalyzed	call on getNickname
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.util.Map:put

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

Kind	Annotation Text

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

Kind	Annotation Text

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

Kind	Annotation Text

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

Kind	Annotation Text

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

Kind	Annotation Text
pre	(soft) com.dmdirc.parser.irc.callbacks. CallbackManager__static_init.new Class[](CallbackMa nager__static_init#1)[...] != null
post	init'ed(new ClientInfo(IRCParser#13).sNickname)
post	init'ed(new ServerInfo(IRCParser#2).isSSL)
post	init'ed(new ServerInfo(IRCParser#2).useSocksProxy)
post	init'ed(this.addLastLine)
post	init'ed(this.createFake)
post	java.lang.StringBuilder:toString(...)._tainted == 0
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(IRCParser#13).lModeQueue == &new LinkedList(ClientInfo#2)
post	new ClientInfo(IRCParser#13).myAwayReason == &""
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).myParser == this.myCallbackManager.myParser
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	new ClientInfo(IRCParser#13).sRealName == &""
post	new ClientInfo(resetState#1) num objects == 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 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	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 ServerInfo(IRCParser#2).host == &"irc.quakenet.org"
post	new ServerInfo(IRCParser#2).password == &""
post	new ServerInfo(IRCParser#2).port == 6_667
post	new ServerInfo(IRCParser#2).proxyHost == &"127.0.0.1"
post	new ServerInfo(IRCParser#2).proxyPass == &""
post	new ServerInfo(IRCParser#2).proxyPort == 1_080
post	new ServerInfo(IRCParser#2).proxyUser == &""
post	new TrustManager[](IRCParser#18) num objects == 1
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#2) num objects == 1
post	possibly_updated(this.stringConverter.lowercase[...])
post	possibly_updated(this.stringConverter.uppercase[...])
post	this.autoListMode == 1
post	this.bindIP == &""
post	this.cMyself == &new ClientInfo(resetState#1)
post	this.cMyself.bIsFake == 1
post	this.cMyself.lModeQueue == &new LinkedList(ClientInfo#2)
post	this.cMyself.myAwayReason == &""
post	this.cMyself.myChannelClientInfos == &new Hashtable(ClientInfo#1)
post	this.cMyself.myMap == &new HashMap(ClientInfo#3 )
post	this.cMyself.myParser == this.myCallbackManager. myParser
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 == null
post	this.cMyself.sNickname == undefined
post	this.cMyself.sRealName == &""
post	this.currentSocketState == &com.dmdirc.parser. irc.SocketState__static_init.new SocketState(Socket State__static_init#2)
post	this.disconnectOnFatal == 1
post	this.got001 == 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.lastLine == &""
post	this.lastPingValue == &""
post	this.me != null
post	this.me == One-of{&new MyInfo(IRCParser#1), myDetails}
post	this.myCallbackManager == &new CallbackManager( IRCParser#16)
post	this.myCallbackManager.callbackHash == &new Hashtable(CallbackManager#1)
post	this.myCallbackManager.myParser != null
post	this.myCallbackManager.myParser == this
post	this.myIgnoreList == &new RegexStringList(IRCPa rser#15)
post	this.myIgnoreList.ignoreInfo == &new ArrayList(RegexStringList#1)
post	this.myProcessingManager == &new ProcessingManager(IRCParser#17)
post	this.myProcessingManager.myParser == this.myCallbackManager.myParser
post	this.myProcessingManager.processHash == &new Hashtable(ProcessingManager#1)
post	this.myTrustManager == &new TrustManager[](IRCP arser#18)
post	this.myTrustManager.length == 1
post	this.myTrustManager[0] == &new IRCParser$1(IRCP arser#19)
post	this.nNextKeyCMBool == 1
post	this.nNextKeyPrefix == 1
post	this.nNextKeyUser == 1
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.post005 == 0
post	this.removeAfterCallback == 1
post	this.sNetworkName == &""
post	this.sServerName == &""
post	this.server != null
post	this.server == One-of{&new ServerInfo(IRCParser #2), serverDetails}
post	this.stringConverter == &new IRCStringConverter (updateCharArrays#1)
post	this.stringConverter.limit == 4
post	this.stringConverter.lowercase == &new char[](IRCStringConverter#1)
post	this.stringConverter.lowercase.length == 127
post	this.stringConverter.uppercase == &new char[](IRCStringConverter#2)
post	this.stringConverter.uppercase.length == 127
post	this.triedAlt == 0
post	this.trustAllCerts == &new TrustManager[](IRCPa rser#18)
unanalyzed	call on call
unanalyzed	call on callDebugInfo
unanalyzed	call on com.dmdirc.parser.irc.ClientInfo
unanalyzed	call on com.dmdirc.parser.irc.IRCProcessor
unanalyzed	call on doDebug
unanalyzed	call on handles
unanalyzed	call on java.lang.Class:asSubclass
unanalyzed	call on java.lang.Class:getName
unanalyzed	call on java.lang.Class:getPackage
unanalyzed	call on java.lang.Class:getSimpleName
unanalyzed	call on java.lang.Class:isAnnotationPresent
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.Package:getName
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toLowerCase
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.util.HashMap
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.util.Hashtable:containsKey
unanalyzed	call on java.util.Hashtable:put
unanalyzed	call on java.util.Hashtable:remove
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.Map:clear
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Timer:cancel
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on setFake
test_vector	myDetails: Addr_Set{null}, Inverse{null}
test_vector	serverDetails: Addr_Set{null}, Inverse{null}

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

Kind	Annotation Text

com.dmdirc.parser.irc.IRCParser__static_init

Kind	Annotation Text

void connect()

Kind	Annotation Text
pre	(soft) init'ed(com/dmdirc/parser/irc/IRCAuthenticat or.me)
pre	(soft) init'ed(this.bindIP)
pre	(soft) init'ed(this.myKeyManagers)
pre	(soft) init'ed(this.myTrustManager)
pre	(soft) init'ed(this.server.proxyPass)
pre	(soft) init'ed(this.server.proxyUser)
pre	(soft) this.server.proxyHost != null
pre	(soft) this.server.proxyPort in {1..2¹⁶-1}
pre	(soft) this.socket != null
pre	init'ed(this.pingTimer)
pre	init'ed(this.server.host)
pre	init'ed(this.server.isSSL)
pre	init'ed(this.server.useSocksProxy)
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	this.server.port in {1..2¹⁶-1}
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	init'ed(new ClientInfo(resetState#1).sNickname)
post	init'ed(new IRCAuthenticator(getIRCAuthenticator#1) .replies)
post	init'ed(this.myTrustManager)
post	new BufferedReader(connect#19) num objects == 1
post	new ClientInfo(resetState#1) num objects == 1
post	new ClientInfo(resetState#1).bIsFake == 1
post	new ClientInfo(resetState#1).lModeQueue == &new LinkedList(ClientInfo#2)
post	new ClientInfo(resetState#1).myAwayReason == &""
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 != null
post	new ClientInfo(resetState#1).myParser == this
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	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	new IRCStringConverter(updateCharArrays#1) num objects == 1
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 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	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects == 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.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.in == &new BufferedReader(connect#19)
post	this.lastLine == &""
post	this.myTrustManager == One-of{old this. myTrustManager, this.trustAllCerts}
post	this.nNextKeyCMBool == 1
post	this.nNextKeyPrefix == 1
post	this.nNextKeyUser == 1
post	this.out == &new PrintWriter(connect#18)
post	this.pingTimer == null
post	this.post005 == 0
post	this.sNetworkName == &""
post	this.sServerName == &""
post	this.socket != null
post	this.stringConverter == &new IRCStringConverter (updateCharArrays#1)
post	this.triedAlt == 0
unanalyzed	call on call
unanalyzed	call on com.dmdirc.parser.irc.ClientInfo
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.net.Authenticator
unanalyzed	call on java.net.Authenticator:setDefault
unanalyzed	call on java.net.PasswordAuthentication
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.Map:clear
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:remove
unanalyzed	call on java.util.Timer:cancel
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on setFake
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}
test_vector	this.bindIP: Addr_Set{null}, Inverse{null}
test_vector	this.myTrustManager: Inverse{null}, Addr_Set{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}

void disconnect(String)

Kind	Annotation Text
pre	(soft) init'ed(this.got001)
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.socket)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) sReason != null
pre	(soft) this.cMyself != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
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
post	init'ed(java.lang.String:substring(...)._tainted)
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	init'ed(new ClientInfo(resetState#1).sHost)
post	init'ed(new ClientInfo(resetState#1).sIdent)
post	init'ed(new ClientInfo(resetState#1).sNickname)
post	init'ed(new ClientInfo(resetState#1).sRealName)
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 IRCStringConverter(updateCharArrays#1). limit)
post	init'ed(new IRCStringConverter(updateCharArrays#1). lowercase)
post	init'ed(new IRCStringConverter(updateCharArrays#1). uppercase)
post	init'ed(new char[](IRCStringConverter#1).length)
post	init'ed(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2).length)
post	init'ed(new char[](IRCStringConverter#2)[...])
post	new ClientInfo(resetState#1) num objects <= 1
post	new ClientInfo(resetState#1) num objects == 0
post	new HashMap(ClientInfo#3) num objects <= 1
post	new HashMap(ClientInfo#3) num objects == 0
post	new Hashtable(ClientInfo#1) num objects <= 1
post	new Hashtable(ClientInfo#1) num objects == 0
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	new IRCStringConverter(updateCharArrays#1) num objects <= 1
post	new IRCStringConverter(updateCharArrays#1) num objects == 0
post	new LinkedList(ClientInfo#2) num objects <= 1
post	new LinkedList(ClientInfo#2) num objects == 0
post	new char[](IRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#1) num objects == 0
post	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2) num objects == 0
post	possibly_updated(new ClientInfo(resetState#1). sHost)
post	possibly_updated(new ClientInfo(resetState#1). sIdent)
post	possibly_updated(new ClientInfo(resetState#1). sNickname)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	possibly_updated(this.cMyself.myAwayReason)
post	this.cMyself in Addr_Set{&new ClientInfo(resetS tate#1),&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.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
unanalyzed	call on call
unanalyzed	call on com.dmdirc.parser.irc.ClientInfo
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:clear
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.Timer:cancel
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on sendString
unanalyzed	call on setAwayReason
unanalyzed	call on setFake
test_vector	this.got001: {0}, {1}

void doSendString(String, bool)

Kind	Annotation Text
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	init'ed(this.out)
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	init'ed(new IRCStringConverter(getIRCStringConverte r#1).limit)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).lowercase)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).uppercase)
post	init'ed(new char[](IRCStringConverter#1).length)
post	init'ed(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2).length)
post	init'ed(new char[](IRCStringConverter#2)[...])
post	init'ed(this.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#2) num objects <= 1
post	possibly_updated(this.cMyself.myAwayReason)
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
unanalyzed	call on call
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
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}
test_vector	this.out: Addr_Set{null}, Inverse{null}

void finalize()

Kind	Annotation Text
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	(soft) this.socket != null
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get

void forceRemoveClient(ClientInfo)

Kind	Annotation Text
pre	(soft) init'ed(this.stringConverter.lowercase[...])
pre	(soft) this.stringConverter.lowercase != null
pre	client != null
pre	client.sNickname != null
pre	init'ed(this.stringConverter)
pre	this.hClientList != 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 == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.stringConverter != null
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray

Map get005()

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

X509Certificate[] getAcceptedIssuers()

Kind	Annotation Text
post	return_value == null

bool getAddLastLine()

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

bool getAutoListMode()

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

String getBindIP()

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

String getBoolChanModes()

Kind	Annotation Text
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	new String(getBoolChanModes#2) num objects == 1
post	return_value == &new String(getBoolChanModes#2)
test_vector	java.util.Iterator:hasNext(...)@1221: {0}, {1}

String getBoolChanModes005()

Kind	Annotation Text
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 - (int) (java.lang.Math:log(...)@1108/java.lang.Math:log(. ..)@1108) in {1..2³²-1}
presumption	java.util.Map:size(...)@1100 >= 1
post	new String(getBoolChanModes005#2) num objects == 1
post	return_value == &new String(getBoolChanModes005 #2)
test_vector	java.lang.Long:longValue(...)@1105: {-2⁶³..0}, {1.. 2⁶⁴-1}
test_vector	java.util.Iterator:hasNext(...)@1104: {0}, {1}

CallbackManager getCallbackManager()

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

ChannelInfo getChannelInfo(String)

Kind	Annotation Text
pre	(soft) init'ed(this.stringConverter.lowercase[...])
pre	(soft) this.stringConverter.lowercase != null
pre	init'ed(this.stringConverter)
pre	sWhat != null
pre	this.hChannelList != null
post	init'ed(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	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.stringConverter != null
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray
test_vector	java.util.Map:containsKey(...)@896: {0}, {1}

Collection getChannels()

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

ClientInfo getClientInfo(String)

Kind	Annotation Text
pre	(soft) init'ed(this.stringConverter.lowercase[...])
pre	(soft) this.stringConverter.lowercase != null
pre	init'ed(this.stringConverter)
pre	sHost != null
pre	this.hClientList != null
presumption	parseHost(...)@870 init'ed
post	init'ed(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 == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.stringConverter != null
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toCharArray
test_vector	java.util.Map:containsKey(...)@871: {0}, {1}

ClientInfo getClientInfoOrFake(String)

Kind	Annotation Text
pre	(soft) init'ed(this.stringConverter.lowercase[...])
pre	(soft) this.stringConverter.lowercase != null
pre	init'ed(this.stringConverter)
pre	sHost != null
pre	this.hClientList != null
presumption	parseHost(...)@882 init'ed
post	init'ed(return_value)
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 != null
post	new ClientInfo(getClientInfoOrFake#1).myParser == this
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 IRCStringConverter(getIRCStringConverter#1). limit == 4
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == &new char[](IRCStringConverter#1)
post	new IRCStringConverter(getIRCStringConverter#1). uppercase == &new char[](IRCStringConverter#2)
post	new LinkedList(ClientInfo#2) num objects <= 1
post	new char[](IRCStringConverter#1) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.stringConverter != null
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.util.LinkedList
test_vector	java.util.Map:containsKey(...)@883: {0}, {1}

Collection getClients()

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

bool getCreateFake()

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

TrustManager[] getDefaultTrustManager()

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

bool getDisconnectOnFatal()

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

String getIRCD(bool)

Kind	Annotation Text
pre	(soft) this.sNetworkName != null
pre	this.h005Info != 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}

IRCStringConverter getIRCStringConverter()

Kind	Annotation Text
pre	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	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	return_value != null
post	return_value == One-of{old this.stringConverter, &new IRCStringConverter(getIRCStringConverter# 1)}
post	this.stringConverter == return_value
test_vector	this.stringConverter: Inverse{null}, Addr_Set{null}

RegexStringList getIgnoreList()

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

String getLastLine()

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

String getListChanModes()

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

int getLocalPort()

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

int getMaxLength(int)

Kind	Annotation Text
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
pre	init'ed(this.cMyself.bIsFake)
pre	nLength <= 2_147_484_153
pre	this.cMyself != 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 call
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
test_vector	this.cMyself.bIsFake: {0}, {1}

int getMaxLength(String, String)

Kind	Annotation Text
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
pre	init'ed(this.cMyself.bIsFake)
pre	this.cMyself != null
presumption	java.lang.String:length(...)@1512 <= 2_147_484_153
presumption	java.lang.String:length(...)@1513 + length in {0..2_147_484_153}
presumption	java.lang.String:length(...)@1513 <= 2_147_484_153
post	return_value <= 2_147_484_153
unanalyzed	call on call
unanalyzed	call on isFake
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on toString
test_vector	sTarget: Addr_Set{null}, Inverse{null}
test_vector	sType: Addr_Set{null}, Inverse{null}

int getMaxListModes(char)

Kind	Annotation Text
pre	(soft) init'ed(this.lastLine)
pre	(soft) this.sNetworkName != null
pre	this.h005Info != null
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
presumption	java.util.Map:get(...)@1555 != null
post	init'ed(return_value)
unanalyzed	call on call
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:matches
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
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}

String getMyNickname()

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

String getMyUsername()

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

ClientInfo getMyself()

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

String getNetworkName()

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

String getOtherModeString(byte)

Kind	Annotation Text
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}

String getParam(String)

Kind	Annotation Text
pre	(soft) line != null
post	return_value == null
post	return_value == undefined

int getPingCountDownLength()

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

bool getPingNeeded()

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

long getPingTime(bool)

Kind	Annotation Text
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}

long getPingTimerLength()

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

String getPrefixModes()

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

ProcessingManager getProcessingManager()

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

bool getRemoveAfterCallback()

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

long getServerLag()

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

String getServerName()

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

String getSetOnlyChanModes()

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

String getSetUnsetChanModes()

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

SocketState getSocketState()

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

TrustManager[] getTrustManager()

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

String getUserModeString()

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

void handleConnectException(Exception)

Kind	Annotation Text
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	new ClientInfo(resetState#1) num objects == 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	possibly_updated(this.stringConverter.lowercase[...])
post	possibly_updated(this.stringConverter.uppercase[...])
post	this.cMyself == &new ClientInfo(resetState#1)
post	this.cMyself.bIsFake == 1
post	this.cMyself.lModeQueue == &new LinkedList(ClientInfo#2)
post	this.cMyself.myAwayReason == &""
post	this.cMyself.myChannelClientInfos == &new Hashtable(ClientInfo#1)
post	this.cMyself.myMap == &new HashMap(ClientInfo#3 )
post	this.cMyself.myParser != null
post	this.cMyself.myParser == this
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 == null
post	this.cMyself.sNickname == undefined
post	this.cMyself.sRealName == &""
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 == &new IRCStringConverter (updateCharArrays#1)
post	this.stringConverter.limit == 4
post	this.stringConverter.lowercase == &new char[](IRCStringConverter#1)
post	this.stringConverter.lowercase.length == 127
post	this.stringConverter.uppercase == &new char[](IRCStringConverter#2)
post	this.stringConverter.uppercase.length == 127
post	this.triedAlt == 0
unanalyzed	call on call
unanalyzed	call on com.dmdirc.parser.irc.ClientInfo
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.Map:clear
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Timer:cancel
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on setFake

bool isReady()

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

bool isUserSettable(Character)

Kind	Annotation Text
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}

bool isValidChannelName(String)

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

void joinChannel(String)

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

void joinChannel(String, String)

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

void joinChannel(String, String, bool)

Kind	Annotation Text
pre	(soft) init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.cMyself.sNickname)
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.sThinkNickname)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) sKey != null
pre	(soft) this.cMyself != null
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
presumption	java.util.Map:get(...)@1447 != null
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).limit)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).lowercase)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).uppercase)
post	init'ed(new char[](IRCStringConverter#1).length)
post	init'ed(new char[](IRCStringConverter#2).length)
post	init'ed(this.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	new IRCStringConverter(getIRCStringConverter#1) num objects == 0
post	new char[](IRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#1) num objects == 0
post	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2) num objects == 0
post	possibly_updated(java.lang.String:substring(...)._ tainted)
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	possibly_updated(this.cMyself.myAwayReason)
unanalyzed	call on call
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on getNickname
unanalyzed	call on isFake
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:isEmpty
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on setAwayReason
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}

void joinChannel(String, bool)

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

int knownChannels()

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

int knownClients()

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

void onPostErrorInfo(ParserError, bool)

Kind	Annotation Text
pre	(soft) init'ed(this.cMyself)
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) init'ed(this.disconnectOnFatal)
pre	(soft) init'ed(this.pingTimer)
pre	(soft) init'ed(this.stringConverter)
pre	errorInfo != null
pre	init'ed(errorInfo.errorLevel)
post	new IRCStringConverter(getIRCStringConverter#1) num objects == 0, if init'ed
post	new IRCStringConverter(getIRCStringConverter#1) num objects == undefined
post	new IRCStringConverter(getIRCStringConverter#1). limit == new IRCStringConverter(getIRCStringConvert er#1) num objects
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == null
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == undefined
post	new IRCStringConverter(getIRCStringConverter#1). uppercase == new IRCStringConverter(getIRCStringCon verter#1).lowercase
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 IRCStringConverter(updateCharArrays#1). lowercase == new IRCStringConverter(getIRCStringCon verter#1).lowercase
post	new IRCStringConverter(updateCharArrays#1). uppercase == new IRCStringConverter(getIRCStringCon verter#1).lowercase
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	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
test_vector	errorInfo.errorLevel mod 2: {0}, {1}
test_vector	this.disconnectOnFatal: {0}, {1}

void parseChanModes()

Kind	Annotation Text
pre	(soft) this.hPrefixModes != null
pre	(soft) this.sNetworkName != null
pre	init'ed(this.lastLine)
pre	this.h005Info != null
pre	this.hChanModesBool != null
pre	this.hChanModesOther != null
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != 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 call
unanalyzed	call on callDebugInfo
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.String:matches
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
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}

void parseChanPrefix()

Kind	Annotation Text
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	this.h005Info != null
pre	this.hChanPrefix != null
presumption	java.util.Map:get(...)@1328 != null
unanalyzed	call on call
unanalyzed	call on callDebugInfo
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
test_vector	java.util.Map:containsKey(...)@1327: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1341: {1}, {0}

void parsePrefixModes()

Kind	Annotation Text
pre	init'ed(this.lastLine)
pre	this.h005Info != null
pre	this.hPrefixMap != null
pre	this.hPrefixModes != null
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
presumption	java.util.Map:get(...)@1353 != null
post	this.nNextKeyPrefix <= 2⁶⁴-2
unanalyzed	call on call
unanalyzed	call on callDebugInfo
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
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}

void parseUserModes()

Kind	Annotation Text
pre	(soft) this.myCallbackManager != null
pre	(soft) this.myCallbackManager.callbackHash != null
pre	this.h005Info != null
pre	this.hUserModes != null
presumption	java.util.Map:get(...)@1300 != null
post	this.nNextKeyUser <= 2⁶⁴-2
unanalyzed	call on call
unanalyzed	call on callDebugInfo
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
test_vector	java.util.Map:containsKey(...)@1299: {0}, {1}
test_vector	java.util.Map:containsKey(...)@1314: {1}, {0}

void partChannel(String, String)

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

void pingTimerTask(Timer)

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

void processLine(String)

Kind	Annotation Text
pre	(soft) init'ed(this...lastLine)
pre	(soft) init'ed(this.currentSocketState)
pre	(soft) init'ed(this.got001)
pre	(soft) init'ed(this.lastLine)
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.pingTime)
pre	(soft) init'ed(this.post005)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this...myCallbackManager != null
pre	(soft) this...myCallbackManager.callbackHash != null
pre	(soft) this.cMyself != null
pre	(soft) this.hChanModesOther != null
pre	(soft) this.hChannelList != null
pre	(soft) this.lastPingValue != null
pre	(soft) this.myProcessingManager != null
pre	(soft) this.myProcessingManager.myParser != null
pre	(soft) this.myProcessingManager.processHash != null
pre	this.myCallbackManager != null
pre	this.myCallbackManager.callbackHash != null
pre	this.pingNeeded != null
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	init'ed(new IRCStringConverter(getIRCStringConverte r#1).limit)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).lowercase)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).uppercase)
post	init'ed(new char[](IRCStringConverter#1).length)
post	init'ed(new char[](IRCStringConverter#2).length)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#2) num objects <= 1
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
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)
unanalyzed	call on call
unanalyzed	call on callErrorInfo
unanalyzed	call on doSendString
unanalyzed	call on getCallbackManager
unanalyzed	call on getCallbackType
unanalyzed	call on getLastLine
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.Exception:getMessage
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.Hashtable:containsKey
unanalyzed	call on java.util.Hashtable:get
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on java.util.concurrent.atomic. AtomicBoolean:set
unanalyzed	call on process
unanalyzed	call on setAwayReason
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: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@997: {1}, {0}
test_vector	java.lang.String:equalsIgnoreCase(...)@999: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@999: {1}, {0}
test_vector	java.lang.String:isEmpty(...)@1000: {1}, {0}
test_vector	java.lang.String:isEmpty(...)@1037: {1}, {0}
test_vector	this.got001: {0}, {1}
test_vector	this.post005: {1}, {0}

void quit(String)

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

void removeChannel(ChannelInfo)

Kind	Annotation Text
pre	(soft) init'ed(this.stringConverter.lowercase[...])
pre	(soft) this.stringConverter.lowercase != null
pre	channel != null
pre	channel.sName != null
pre	init'ed(this.stringConverter)
pre	this.hChannelList != 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	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.stringConverter != null
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray

void removeClient(ClientInfo)

Kind	Annotation Text
pre	(soft) client != null
pre	(soft) client.sNickname != null
pre	(soft) init'ed(this.stringConverter)
pre	(soft) init'ed(this.stringConverter.lowercase[...])
pre	(soft) this.hClientList != null
pre	(soft) this.stringConverter.lowercase != null
pre	init'ed(this.cMyself)
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	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.stringConverter == One-of{old this. stringConverter, &new IRCStringConverter(getIRC StringConverter#1)}
unanalyzed	call on getNickname
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.util.Map:remove
test_vector	client == this.cMyself: {1}, {0}

void resetState()

Kind	Annotation Text
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	new ClientInfo(resetState#1) num objects == 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 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 LinkedList(ClientInfo#2) num objects == 1
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects == 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.cMyself == &new ClientInfo(resetState#1)
post	this.cMyself.bIsFake == 1
post	this.cMyself.lModeQueue == &new LinkedList(ClientInfo#2)
post	this.cMyself.myAwayReason == &""
post	this.cMyself.myChannelClientInfos == &new Hashtable(ClientInfo#1)
post	this.cMyself.myMap == &new HashMap(ClientInfo#3 )
post	this.cMyself.myParser != null
post	this.cMyself.myParser == this
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 == null
post	this.cMyself.sNickname == undefined
post	this.cMyself.sRealName == &""
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 == &new IRCStringConverter (updateCharArrays#1)
post	this.triedAlt == 0
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Hashtable
unanalyzed	call on java.util.LinkedList
test_vector	this.pingTimer: Addr_Set{null}, Inverse{null}

void run()

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

void sendAction(String, String)

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

void sendCTCP(String, String, String)

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

void sendCTCPReply(String, String, String)

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

void sendConnectionStrings()

Kind	Annotation Text
pre	(soft) init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
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	init'ed(this.currentSocketState)
pre	init'ed(this.me.nickname)
pre	init'ed(this.me.realname)
pre	init'ed(this.me.username)
pre	init'ed(this.server.host)
pre	this.me != null
pre	this.server != null
pre	this.server.password != null
presumption	java.net.InetAddress:getLocalHost(...)@720 != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).limit)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).lowercase)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).uppercase)
post	init'ed(new char[](IRCStringConverter#1).length)
post	init'ed(new char[](IRCStringConverter#2).length)
post	init'ed(this.me.nickname)
post	init'ed(this.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#1) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	new char[](IRCStringConverter#2) num objects <= 1
post	new char[](IRCStringConverter#2) num objects == new IRCStringConverter(getIRCStringConverter#1) num objects
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	possibly_updated(this.cMyself.myAwayReason)
post	this.me.nickname == old 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)}
unanalyzed	call on call
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on getNickname
unanalyzed	call on isFake
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on setAwayReason
test_vector	java.lang.String:isEmpty(...)@714: {1}, {0}

void sendLine(String)

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

void sendMessage(String, String)

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

void sendNotice(String, String)

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

void sendString(String)

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

void setAddLastLine(bool)

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

void setAutoListMode(bool)

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

void setBindIP(String)

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

void setCreateFake(bool)

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

void setDisconnectOnFatal(bool)

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

void setIgnoreList(RegexStringList)

Kind	Annotation Text
post	init'ed(this.myIgnoreList)
post	this.myIgnoreList == ignoreList

void setKeyManagers(KeyManager[])

Kind	Annotation Text
post	init'ed(this.myKeyManagers)
post	this.myKeyManagers == newKeyManagers

void setNickname(String)

Kind	Annotation Text
pre	(soft) init'ed(this.cMyself.bIsFake)
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.stringConverter)
pre	(soft) this.cMyself != null
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	init'ed(this.currentSocketState)
post	init'ed(java.lang.String:substring(...)._tainted)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).limit)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).lowercase)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).uppercase)
post	init'ed(new char[](IRCStringConverter#1).length)
post	init'ed(new char[](IRCStringConverter#2).length)
post	init'ed(this.stringConverter)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#1) num objects <= 1
post	new char[](IRCStringConverter#2) num objects <= 1
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	possibly_updated(this.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)}
unanalyzed	call on call
unanalyzed	call on doSendString
unanalyzed	call on getListModeQueue
unanalyzed	call on java.io.PrintWriter:printf
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.LinkedList:contains
unanalyzed	call on java.util.LinkedList:offer
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Queue:offer
unanalyzed	call on setAwayReason
test_vector	java.lang.String:equals(...)@1489: {0}, {1}
test_vector	this.cMyself.bIsFake: {1}, {0}

void setPingCountDownLength(int)

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

void setPingNeeded(bool)

Kind	Annotation Text
pre	this.pingNeeded != null

void setPingTimerLength(long)

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

void setRemoveAfterCallback(bool)

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

void setTrustManager(TrustManager[])

Kind	Annotation Text
post	init'ed(this.myTrustManager)
post	this.myTrustManager == newTrustManager

void startPingTimer()

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

String[] tokeniseLine(String)

Kind	Annotation Text
presumption	java.lang.String:indexOf(...)@848 <= 2³²-3
post	init'ed(java.lang.String:split(...)._tainted)
post	init'ed(java.lang.String:substring(...)._tainted)
post	java.lang.String:split(...)[...] == null
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
post	return_value in Addr_Set{&java.lang. String:split(...),&new String[](tokeniseLine#2) ,&new String[](tokeniseLine#1)}
test_vector	java.lang.String:indexOf(...)@848: {-2³¹. .-1}, {0..2³²-3}
test_vector	line: Inverse{null}, Addr_Set{null}

void updateCharArrays(byte)

Kind	Annotation Text
post	new IRCStringConverter(updateCharArrays#1) num objects == 1
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects == 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.stringConverter == &new IRCStringConverter (updateCharArrays#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)