PluginEvents.java

PluginEvents.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.PluginEvents(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.PluginEvents__static_init

Kind	Annotation Text
post	$VALUES == &new PluginEvents[](PluginEvents__ static_init#4)
post	$VALUES.length == 1
post	$VALUES[0] == &new PluginEvents(PluginEvents__ static_init#1)
post	PLUGIN_EVENT == &new PluginEvents(PluginEvents_ _static_init#1)
post	PLUGIN_EVENT.argNames == &new String[](PluginEv ents__static_init#2)
post	PLUGIN_EVENT.argNames.length == 1
post	PLUGIN_EVENT.argNames[0] == &"plugin"
post	PLUGIN_EVENT.argTypes == &new Class[](PluginEve nts__static_init#3)
post	PLUGIN_EVENT.argTypes.length == 1
post	new Class[](PluginEvents__static_init#3) num objects == 1
post	new PluginEvents(PluginEvents__static_init#1) num objects == 1
post	new PluginEvents[](PluginEvents__static_init#4) num objects == 1
post	new String[](PluginEvents__static_init#2) 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

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 == &"Plugin Events"

PluginEvents valueOf(String)

Kind	Annotation Text
post	init'ed(return_value)

PluginEvents[] values()

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