DCCEvents.java

DCCEvents.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void com.dmdirc.addons.dcc.actions.DCCEvents(String, int, String[], Class[])

Kind	Annotation Text
post	init'ed(this.argNames)
post	init'ed(this.argTypes)
post	this.argNames == argNames
post	this.argTypes == argTypes

com.dmdirc.addons.dcc.actions.DCCEvents__static_init

Kind	Annotation Text
presumption	init'ed(java.lang.Integer.TYPE)
post	$VALUES == &new DCCEvents[](DCCEvents__static_ init#34)
post	$VALUES.length == 11
post	$VALUES[0] == &new DCCEvents(DCCEvents__static_ init#1)
post	$VALUES[10] == &new DCCEvents(DCCEvents__ static_init#31)
post	$VALUES[1] == &new DCCEvents(DCCEvents__static_ init#4)
post	$VALUES[2] == &new DCCEvents(DCCEvents__static_ init#7)
post	$VALUES[3] == &new DCCEvents(DCCEvents__static_ init#10)
post	$VALUES[4] == &new DCCEvents(DCCEvents__static_ init#13)
post	$VALUES[5] == &new DCCEvents(DCCEvents__static_ init#16)
post	$VALUES[6] == &new DCCEvents(DCCEvents__static_ init#19)
post	$VALUES[7] == &new DCCEvents(DCCEvents__static_ init#22)
post	$VALUES[8] == &new DCCEvents(DCCEvents__static_ init#25)
post	$VALUES[9] == &new DCCEvents(DCCEvents__static_ init#28)
post	DCC_CHAT_MESSAGE == &new DCCEvents(DCCEvents__ static_init#7)
post	DCC_CHAT_MESSAGE.argNames == &new String[](DCCEvents__static_init#8)
post	DCC_CHAT_MESSAGE.argNames.length == 3
post	DCC_CHAT_MESSAGE.argNames[0] == &"DCCChatWindow "
post	DCC_CHAT_MESSAGE.argNames[1] == &"Nickname"
post	DCC_CHAT_MESSAGE.argNames[2] == &"Message"
post	DCC_CHAT_MESSAGE.argTypes == &new Class[](DCCEvents__static_init#9)
post	DCC_CHAT_MESSAGE.argTypes.length == 3
post	DCC_CHAT_REQUEST == &new DCCEvents(DCCEvents__ static_init#1)
post	DCC_CHAT_REQUEST.argNames == &new String[](DCCEvents__static_init#2)
post	DCC_CHAT_REQUEST.argNames.length == 2
post	DCC_CHAT_REQUEST.argNames[0] == &"server"
post	DCC_CHAT_REQUEST.argNames[1] == &"client"
post	DCC_CHAT_REQUEST.argTypes == &new Class[](DCCEvents__static_init#3)
post	DCC_CHAT_REQUEST.argTypes.length == 2
post	DCC_CHAT_REQUEST_SENT == &new DCCEvents(DCCEven ts__static_init#4)
post	DCC_CHAT_REQUEST_SENT.argNames == &new String[](DCCEvents__static_init#5)
post	DCC_CHAT_REQUEST_SENT.argNames.length == 2
post	DCC_CHAT_REQUEST_SENT.argNames[0] == &"server"
post	DCC_CHAT_REQUEST_SENT.argNames[1] == &"client"
post	DCC_CHAT_REQUEST_SENT.argTypes == &new Class[](DCCEvents__static_init#6)
post	DCC_CHAT_REQUEST_SENT.argTypes.length == 2
post	DCC_CHAT_SELFMESSAGE == &new DCCEvents(DCCEvent s__static_init#10)
post	DCC_CHAT_SELFMESSAGE.argNames == &new String[](DCCEvents__static_init#11)
post	DCC_CHAT_SELFMESSAGE.argNames.length == 2
post	DCC_CHAT_SELFMESSAGE.argNames[0] == &"DCCChatWindow"
post	DCC_CHAT_SELFMESSAGE.argNames[1] == &"Message"
post	DCC_CHAT_SELFMESSAGE.argTypes == &new Class[](DCCEvents__static_init#12)
post	DCC_CHAT_SELFMESSAGE.argTypes.length == 2
post	DCC_CHAT_SOCKETCLOSED == &new DCCEvents(DCCEven ts__static_init#13)
post	DCC_CHAT_SOCKETCLOSED.argNames == &new String[](DCCEvents__static_init#14)
post	DCC_CHAT_SOCKETCLOSED.argNames.length == 1
post	DCC_CHAT_SOCKETCLOSED.argNames[0] == &"DCCChatWindow"
post	DCC_CHAT_SOCKETCLOSED.argTypes == &new Class[](DCCEvents__static_init#15)
post	DCC_CHAT_SOCKETCLOSED.argTypes.length == 1
post	DCC_CHAT_SOCKETOPENED == &new DCCEvents(DCCEven ts__static_init#16)
post	DCC_CHAT_SOCKETOPENED.argNames == &new String[](DCCEvents__static_init#17)
post	DCC_CHAT_SOCKETOPENED.argNames.length == 1
post	DCC_CHAT_SOCKETOPENED.argNames[0] == &"DCCChatWindow"
post	DCC_CHAT_SOCKETOPENED.argTypes == &new Class[](DCCEvents__static_init#18)
post	DCC_CHAT_SOCKETOPENED.argTypes.length == 1
post	DCC_SEND_DATATRANSFERED == &new DCCEvents(DCCEvents__static_init#25)
post	DCC_SEND_DATATRANSFERED.argNames == &new String[](DCCEvents__static_init#26)
post	DCC_SEND_DATATRANSFERED.argNames.length == 2
post	DCC_SEND_DATATRANSFERED.argNames[0] == &"DCCSendWindow"
post	DCC_SEND_DATATRANSFERED.argNames[1] == &"Bytes Transfered"
post	DCC_SEND_DATATRANSFERED.argTypes == &new Class[](DCCEvents__static_init#27)
post	DCC_SEND_DATATRANSFERED.argTypes.length == 2
post	DCC_SEND_DATATRANSFERED.argTypes[1] == java.lang.Integer.TYPE
post	DCC_SEND_REQUEST == &new DCCEvents(DCCEvents__ static_init#28)
post	DCC_SEND_REQUEST.argNames == &new String[](DCCEvents__static_init#29)
post	DCC_SEND_REQUEST.argNames.length == 3
post	DCC_SEND_REQUEST.argNames[0] == &"server"
post	DCC_SEND_REQUEST.argNames[1] == &"client"
post	DCC_SEND_REQUEST.argNames[2] == &"file"
post	DCC_SEND_REQUEST.argTypes == &new Class[](DCCEvents__static_init#30)
post	DCC_SEND_REQUEST.argTypes.length == 3
post	DCC_SEND_REQUEST_SENT == &new DCCEvents(DCCEven ts__static_init#31)
post	DCC_SEND_REQUEST_SENT.argNames == &new String[](DCCEvents__static_init#32)
post	DCC_SEND_REQUEST_SENT.argNames.length == 3
post	DCC_SEND_REQUEST_SENT.argNames[0] == &"server"
post	DCC_SEND_REQUEST_SENT.argNames[1] == &"client"
post	DCC_SEND_REQUEST_SENT.argNames[2] == &"file"
post	DCC_SEND_REQUEST_SENT.argTypes == &new Class[](DCCEvents__static_init#33)
post	DCC_SEND_REQUEST_SENT.argTypes.length == 3
post	DCC_SEND_SOCKETCLOSED == &new DCCEvents(DCCEven ts__static_init#19)
post	DCC_SEND_SOCKETCLOSED.argNames == &new String[](DCCEvents__static_init#20)
post	DCC_SEND_SOCKETCLOSED.argNames.length == 1
post	DCC_SEND_SOCKETCLOSED.argNames[0] == &"DCCSendWindow"
post	DCC_SEND_SOCKETCLOSED.argTypes == &new Class[](DCCEvents__static_init#21)
post	DCC_SEND_SOCKETCLOSED.argTypes.length == 1
post	DCC_SEND_SOCKETOPENED == &new DCCEvents(DCCEven ts__static_init#22)
post	DCC_SEND_SOCKETOPENED.argNames == &new String[](DCCEvents__static_init#23)
post	DCC_SEND_SOCKETOPENED.argNames.length == 1
post	DCC_SEND_SOCKETOPENED.argNames[0] == &"DCCSendWindow"
post	DCC_SEND_SOCKETOPENED.argTypes == &new Class[](DCCEvents__static_init#24)
post	DCC_SEND_SOCKETOPENED.argTypes.length == 1
post	init'ed(DCC_SEND_DATATRANSFERED.argTypes[1])
post	new Class[](DCCEvents__static_init#12) num objects == 1
post	new Class[](DCCEvents__static_init#15) num objects == 1
post	new Class[](DCCEvents__static_init#18) num objects == 1
post	new Class[](DCCEvents__static_init#21) num objects == 1
post	new Class[](DCCEvents__static_init#24) num objects == 1
post	new Class[](DCCEvents__static_init#27) num objects == 1
post	new Class[](DCCEvents__static_init#3) num objects == 1
post	new Class[](DCCEvents__static_init#30) num objects == 1
post	new Class[](DCCEvents__static_init#33) num objects == 1
post	new Class[](DCCEvents__static_init#6) num objects == 1
post	new Class[](DCCEvents__static_init#9) num objects == 1
post	new DCCEvents(DCCEvents__static_init#1) num objects == 1
post	new DCCEvents(DCCEvents__static_init#10) num objects == 1
post	new DCCEvents(DCCEvents__static_init#13) num objects == 1
post	new DCCEvents(DCCEvents__static_init#16) num objects == 1
post	new DCCEvents(DCCEvents__static_init#19) num objects == 1
post	new DCCEvents(DCCEvents__static_init#22) num objects == 1
post	new DCCEvents(DCCEvents__static_init#25) num objects == 1
post	new DCCEvents(DCCEvents__static_init#28) num objects == 1
post	new DCCEvents(DCCEvents__static_init#31) num objects == 1
post	new DCCEvents(DCCEvents__static_init#4) num objects == 1
post	new DCCEvents(DCCEvents__static_init#7) num objects == 1
post	new DCCEvents[](DCCEvents__static_init#34) num objects == 1
post	new String[](DCCEvents__static_init#11) num objects == 1
post	new String[](DCCEvents__static_init#14) num objects == 1
post	new String[](DCCEvents__static_init#17) num objects == 1
post	new String[](DCCEvents__static_init#2) num objects == 1
post	new String[](DCCEvents__static_init#20) num objects == 1
post	new String[](DCCEvents__static_init#23) num objects == 1
post	new String[](DCCEvents__static_init#26) num objects == 1
post	new String[](DCCEvents__static_init#29) num objects == 1
post	new String[](DCCEvents__static_init#32) num objects == 1
post	new String[](DCCEvents__static_init#5) num objects == 1
post	new String[](DCCEvents__static_init#8) num objects == 1
unanalyzed	call on java.lang.Enum

String[] getArgNames()

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

Class[] getArgTypes()

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

int getArity()

Kind	Annotation Text
pre	this.argNames != null
pre	this.argNames.length <= 2³²-1
post	return_value == this.argNames.length
post	return_value >= 0

String getGroup()

Kind	Annotation Text
post	return_value == &"DCC Events"

DCCEvents valueOf(String)

Kind	Annotation Text
post	init'ed(return_value)

DCCEvents[] values()

Kind	Annotation Text
pre	(soft) init'ed($VALUES[...])
post	new DCCEvents[](values#1) num objects == 1
post	return_value == &new DCCEvents[](values#1)
post	return_value.length == 11
post	return_value[...] == One-of{$VALUES[...], undefined}