ClientEvents.java

ClientEvents.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void com.dmdirc.actions.metatypes.ClientEvents(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.actions.metatypes.ClientEvents__static_init

Kind	Annotation Text
post	$VALUES == &new ClientEvents[](ClientEvents__ static_init#28)
post	$VALUES.length == 9
post	$VALUES[0] == &new ClientEvents(ClientEvents__ static_init#1)
post	$VALUES[1] == &new ClientEvents(ClientEvents__ static_init#4)
post	$VALUES[2] == &new ClientEvents(ClientEvents__ static_init#7)
post	$VALUES[3] == &new ClientEvents(ClientEvents__ static_init#10)
post	$VALUES[4] == &new ClientEvents(ClientEvents__ static_init#13)
post	$VALUES[5] == &new ClientEvents(ClientEvents__ static_init#16)
post	$VALUES[6] == &new ClientEvents(ClientEvents__ static_init#19)
post	$VALUES[7] == &new ClientEvents(ClientEvents__ static_init#22)
post	$VALUES[8] == &new ClientEvents(ClientEvents__ static_init#25)
post	CLIENT_EVENT == &new ClientEvents(ClientEvents_ _static_init#1)
post	CLIENT_EVENT.argNames == &new String[](ClientEv ents__static_init#2)
post	CLIENT_EVENT.argTypes == &new Class[](ClientEve nts__static_init#3)
post	CLIENT_EVENT_WITH_BUFFER == &new ClientEvents(ClientEvents__static_init#16)
post	CLIENT_EVENT_WITH_BUFFER.argNames == &new String[](ClientEvents__static_init#17)
post	CLIENT_EVENT_WITH_BUFFER.argNames.length == 2
post	CLIENT_EVENT_WITH_BUFFER.argNames[0] == &"origin"
post	CLIENT_EVENT_WITH_BUFFER.argNames[1] == &"buffer"
post	CLIENT_EVENT_WITH_BUFFER.argTypes == &new Class[](ClientEvents__static_init#18)
post	CLIENT_EVENT_WITH_BUFFER.argTypes.length == 2
post	CLIENT_EVENT_WITH_KEY == &new ClientEvents(Clie ntEvents__static_init#13)
post	CLIENT_EVENT_WITH_KEY.argNames == &new String[](ClientEvents__static_init#14)
post	CLIENT_EVENT_WITH_KEY.argNames.length == 1
post	CLIENT_EVENT_WITH_KEY.argNames[0] == &"key event"
post	CLIENT_EVENT_WITH_KEY.argTypes == &new Class[](ClientEvents__static_init#15)
post	CLIENT_EVENT_WITH_KEY.argTypes.length == 1
post	CLIENT_EVENT_WITH_PREFS == &new ClientEvents(ClientEvents__static_init#19)
post	CLIENT_EVENT_WITH_PREFS.argNames == &new String[](ClientEvents__static_init#20)
post	CLIENT_EVENT_WITH_PREFS.argNames.length == 1
post	CLIENT_EVENT_WITH_PREFS.argNames[0] == &"preferences manager"
post	CLIENT_EVENT_WITH_PREFS.argTypes == &new Class[](ClientEvents__static_init#21)
post	CLIENT_EVENT_WITH_PREFS.argTypes.length == 1
post	CLIENT_EVENT_WITH_STYLE == &new ClientEvents(ClientEvents__static_init#22)
post	CLIENT_EVENT_WITH_STYLE.argNames == &new String[](ClientEvents__static_init#23)
post	CLIENT_EVENT_WITH_STYLE.argNames.length == 3
post	CLIENT_EVENT_WITH_STYLE.argNames[0] == &"styled document"
post	CLIENT_EVENT_WITH_STYLE.argNames[1] == &"start offset"
post	CLIENT_EVENT_WITH_STYLE.argNames[2] == &"length"
post	CLIENT_EVENT_WITH_STYLE.argTypes == &new Class[](ClientEvents__static_init#24)
post	CLIENT_EVENT_WITH_STYLE.argTypes.length == 3
post	POPUP_EVENT == &new ClientEvents(ClientEvents__ static_init#10)
post	POPUP_EVENT.argNames == &new String[](ClientEve nts__static_init#11)
post	POPUP_EVENT.argNames.length == 3
post	POPUP_EVENT.argNames[0] == &"popup type"
post	POPUP_EVENT.argNames[1] == &"popup"
post	POPUP_EVENT.argNames[2] == &"configuration manager"
post	POPUP_EVENT.argTypes == &new Class[](ClientEven ts__static_init#12)
post	POPUP_EVENT.argTypes.length == 3
post	UNKNOWN_COMMAND == &new ClientEvents(ClientEven ts__static_init#25)
post	UNKNOWN_COMMAND.argNames == &new String[](ClientEvents__static_init#26)
post	UNKNOWN_COMMAND.argNames.length == 3
post	UNKNOWN_COMMAND.argNames[0] == &"source"
post	UNKNOWN_COMMAND.argNames[1] == &"command"
post	UNKNOWN_COMMAND.argNames[2] == &"arguments"
post	UNKNOWN_COMMAND.argTypes == &new Class[](ClientEvents__static_init#27)
post	UNKNOWN_COMMAND.argTypes.length == 3
post	WINDOW_EVENT == &new ClientEvents(ClientEvents_ _static_init#4)
post	WINDOW_EVENT.argNames == &new String[](ClientEv ents__static_init#5)
post	WINDOW_EVENT.argNames.length == 1
post	WINDOW_EVENT.argNames[0] == &"window"
post	WINDOW_EVENT.argTypes == &new Class[](ClientEve nts__static_init#6)
post	WINDOW_EVENT.argTypes.length == 1
post	WINDOW_EVENT_WITH_MESSAGE == &new ClientEvents(ClientEvents__static_init#7)
post	WINDOW_EVENT_WITH_MESSAGE.argNames == &new String[](ClientEvents__static_init#8)
post	WINDOW_EVENT_WITH_MESSAGE.argNames.length == 2
post	WINDOW_EVENT_WITH_MESSAGE.argNames[0] == &"window"
post	WINDOW_EVENT_WITH_MESSAGE.argNames[1] == &"message"
post	WINDOW_EVENT_WITH_MESSAGE.argTypes == &new Class[](ClientEvents__static_init#9)
post	WINDOW_EVENT_WITH_MESSAGE.argTypes.length == 2
post	init'ed(CLIENT_EVENT.argNames.length)
post	init'ed(CLIENT_EVENT.argTypes.length)
post	new Class[](ClientEvents__static_init#12) num objects == 1
post	new Class[](ClientEvents__static_init#15) num objects == 1
post	new Class[](ClientEvents__static_init#18) num objects == 1
post	new Class[](ClientEvents__static_init#21) num objects == 1
post	new Class[](ClientEvents__static_init#24) num objects == 1
post	new Class[](ClientEvents__static_init#27) num objects == 1
post	new Class[](ClientEvents__static_init#3) num objects == 1
post	new Class[](ClientEvents__static_init#6) num objects == 1
post	new Class[](ClientEvents__static_init#9) num objects == 1
post	new ClientEvents(ClientEvents__static_init#1) num objects == 1
post	new ClientEvents(ClientEvents__static_init#10) num objects == 1
post	new ClientEvents(ClientEvents__static_init#13) num objects == 1
post	new ClientEvents(ClientEvents__static_init#16) num objects == 1
post	new ClientEvents(ClientEvents__static_init#19) num objects == 1
post	new ClientEvents(ClientEvents__static_init#22) num objects == 1
post	new ClientEvents(ClientEvents__static_init#25) num objects == 1
post	new ClientEvents(ClientEvents__static_init#4) num objects == 1
post	new ClientEvents(ClientEvents__static_init#7) num objects == 1
post	new ClientEvents[](ClientEvents__static_init#28) num objects == 1
post	new String[](ClientEvents__static_init#11) num objects == 1
post	new String[](ClientEvents__static_init#14) num objects == 1
post	new String[](ClientEvents__static_init#17) num objects == 1
post	new String[](ClientEvents__static_init#2) num objects == 1
post	new String[](ClientEvents__static_init#20) num objects == 1
post	new String[](ClientEvents__static_init#23) num objects == 1
post	new String[](ClientEvents__static_init#26) num objects == 1
post	new String[](ClientEvents__static_init#5) num objects == 1
post	new String[](ClientEvents__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 == &"General Events"

ClientEvents valueOf(String)

Kind	Annotation Text
post	init'ed(return_value)

ClientEvents[] values()

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