Messages

Last Msg First Msg

method

com.dmdirc.parser.irc.ProcessQuit__static_init

method	void process(String, String[])
pre	token != null
pre	token.length <= 2³²
pre	(soft) init'ed(this.myParser.stringConverter)
pre	(soft) this.myParser != null
pre	(soft) init'ed(this.myParser.cMyself)
pre	(soft) this.myParser.cMyself.sNickname != null
pre	(soft) this.myParser.hChannelList != null
pre	(soft) this.myParser.hClientList != null
pre	(soft) this.myParser.myCallbackManager != null
pre	(soft) this.myParser.myCallbackManager. callbackHash != null
pre	(soft) init'ed(this.myParser.removeAfterCallback)
pre	(soft) this.myParser.stringConverter.lowercase != null
pre	(soft) init'ed(this.myParser.stringConverter. lowercase[...])
pre	(soft) token[0] != null
pre	(soft) init'ed(token[...])
presumption	iChannel.hChannelUserList@57 != null
presumption	iChannel.myParser.hClientList@57 != null
presumption	iChannel.myParser.stringConverter.lowercase@58 != null
presumption	iChannel.myParser@57 != null
presumption	iChannel.sName@57 != null
presumption	iClient.sHost != null
presumption	iClient.sNickname != null
presumption	java.util.ArrayList:iterator(...)@57 != null
presumption	java.util.Iterator:next(...)@57 != null
presumption	this.myParser.stringConverter.lowercase@56 != null
presumption	this.myParser.stringConverter.lowercase@63 != null
post	init'ed(this.myParser.stringConverter)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1) num objects)
post	new IRCStringConverter(getIRCStringConverter#1) num objects <= 1
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).limit)
post	new IRCStringConverter(getIRCStringConverter#1). limit == 4
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).lowercase)
post	new IRCStringConverter(getIRCStringConverter#1). lowercase == &new char[](IRCStringConverter#1)
post	init'ed(new IRCStringConverter(getIRCStringConverte r#1).uppercase)
post	new IRCStringConverter(getIRCStringConverter#1). uppercase == &new char[](IRCStringConverter#2)
post	init'ed(new char[](IRCStringConverter#1) num objects)
post	new char[](IRCStringConverter#1) num objects <= 1
post	init'ed(new char[](IRCStringConverter#1).length)
post	new char[](IRCStringConverter#1).length == 127
post	init'ed(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	init'ed(new char[](IRCStringConverter#2) num objects)
post	new char[](IRCStringConverter#2) num objects <= 1
post	init'ed(new char[](IRCStringConverter#2).length)
post	new char[](IRCStringConverter#2).length == 127
post	init'ed(new char[](IRCStringConverter#2)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
unanalyzed	call on getCallbackManager
unanalyzed	call on getCallbackType
unanalyzed	call on call
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.util.Map:get
unanalyzed	call on getClientInfo
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.Map:values
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on getClient
unanalyzed	call on getChannel
unanalyzed	call on getName
unanalyzed	call on java.lang.String:toCharArray
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String
unanalyzed	call on java.util.Map:remove
unanalyzed	call on java.util.Map:isEmpty
unanalyzed	call on getNickname
unanalyzed	call on forceRemoveClient
unanalyzed	call on java.util.Map:clear
unanalyzed	call on addClient
unanalyzed	call on java.util.Map:put
unanalyzed	call on parseHost
test_vector	this.myParser.removeAfterCallback: {0}, {1}
test_vector	token.length: {2}, {0,1}, {3..2³²}
test_vector	java.lang.String:isEmpty(...)@49: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@57: {0}, {1}

method	bool callChannelQuit(ChannelInfo, ChannelClientInf o, String)
pre	this.myParser != null
pre	this.myParser.myCallbackManager != null
pre	this.myParser.myCallbackManager.callbackHash != null
presumption	getCallbackManager(...)@90 init'ed
post	init'ed(return_value)
unanalyzed	call on getCallbackManager
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.util.Map:get

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that getCallbackType(...) != null

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

Prev Msg Next Msg

method	bool callQuit(ClientInfo, String)
pre	this.myParser != null
pre	this.myParser.myCallbackManager != null
pre	this.myParser.myCallbackManager.callbackHash != null
presumption	getCallbackManager(...)@102 init'ed
post	init'ed(return_value)
unanalyzed	call on getCallbackManager
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.util.Map:get

method	String[] handles()
post	return_value == &new String[](handles#1)
post	new String[](handles#1) num objects == 1
post	return_value.length == 1
post	return_value[0] == &"QUIT"

method	void com.dmdirc.parser.irc.ProcessQuit(IRCParser, ProcessingManager)
post	this.myManager == manager
post	init'ed(this.myManager)
post	this.myParser == parser
post	init'ed(this.myParser)