ConfigTarget.java

ConfigTarget.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

com.dmdirc.config.ConfigTarget$1__static_init

Kind	Annotation Text
pre	(soft) init'ed(com.dmdirc.config.ConfigTarget$TYPE_ _static_init.new ConfigTarget$TYPE[](ConfigTarget$T YPE__static_init#9)[...])
presumption	com.dmdirc.config.ConfigTarget_TYPE:ordinal(... )@174 - values(...).length in range
presumption	com.dmdirc.config.ConfigTarget_TYPE:ordinal(... )@174 in {0..7}
post	new int[](ConfigTarget$1__static_init#1) num objects == 1

void com.dmdirc.config.ConfigTarget$TYPE(String, int)

Kind	Annotation Text

com.dmdirc.config.ConfigTarget$TYPE__static_init

Kind	Annotation Text
post	$VALUES == &new ConfigTarget$TYPE[](ConfigTarge t$TYPE__static_init#9)
post	$VALUES.length == 8
post	$VALUES[0] == &new ConfigTarget$TYPE(ConfigTarg et$TYPE__static_init#1)
post	$VALUES[1] == &new ConfigTarget$TYPE(ConfigTarg et$TYPE__static_init#2)
post	$VALUES[2] == &new ConfigTarget$TYPE(ConfigTarg et$TYPE__static_init#3)
post	$VALUES[3] == &new ConfigTarget$TYPE(ConfigTarg et$TYPE__static_init#4)
post	$VALUES[4] == &new ConfigTarget$TYPE(ConfigTarg et$TYPE__static_init#5)
post	$VALUES[5] == &new ConfigTarget$TYPE(ConfigTarg et$TYPE__static_init#6)
post	$VALUES[6] == &new ConfigTarget$TYPE(ConfigTarg et$TYPE__static_init#7)
post	$VALUES[7] == &new ConfigTarget$TYPE(ConfigTarg et$TYPE__static_init#8)
post	CHANNEL == &new ConfigTarget$TYPE(ConfigTarget$ TYPE__static_init#8)
post	GLOBAL == &new ConfigTarget$TYPE(ConfigTarget$T YPE__static_init#2)
post	GLOBALDEFAULT == &new ConfigTarget$TYPE(ConfigT arget$TYPE__static_init#1)
post	IRCD == &new ConfigTarget$TYPE(ConfigTarget$TYP E__static_init#5)
post	NETWORK == &new ConfigTarget$TYPE(ConfigTarget$ TYPE__static_init#6)
post	PROFILE == &new ConfigTarget$TYPE(ConfigTarget$ TYPE__static_init#4)
post	SERVER == &new ConfigTarget$TYPE(ConfigTarget$T YPE__static_init#7)
post	THEME == &new ConfigTarget$TYPE(ConfigTarget$TY PE__static_init#3)
post	new ConfigTarget$TYPE(ConfigTarget$TYPE__static_ init#1) num objects == 1
post	new ConfigTarget$TYPE(ConfigTarget$TYPE__static_ init#2) num objects == 1
post	new ConfigTarget$TYPE(ConfigTarget$TYPE__static_ init#3) num objects == 1
post	new ConfigTarget$TYPE(ConfigTarget$TYPE__static_ init#4) num objects == 1
post	new ConfigTarget$TYPE(ConfigTarget$TYPE__static_ init#5) num objects == 1
post	new ConfigTarget$TYPE(ConfigTarget$TYPE__static_ init#6) num objects == 1
post	new ConfigTarget$TYPE(ConfigTarget$TYPE__static_ init#7) num objects == 1
post	new ConfigTarget$TYPE(ConfigTarget$TYPE__static_ init#8) num objects == 1
post	new ConfigTarget$TYPE[](ConfigTarget$TYPE__static_ init#9) num objects == 1
unanalyzed	call on java.lang.Enum

void com.dmdirc.config.ConfigTarget()

Kind	Annotation Text
post	this.order == 50_000
post	this.type == &com.dmdirc.config. ConfigTarget$TYPE__static_init.new ConfigTarget$TYP E(ConfigTarget$TYPE__static_init#2)

com.dmdirc.config.ConfigTarget__static_init

Kind	Annotation Text

int compareTo(Object)

Kind	Annotation Text
pre	(soft) init'ed(target.order)
pre	(soft) init'ed(this.order)
pre	(soft) target.order - this.order in {-2³¹..2³²-1}
pre	init'ed(target.type)
pre	target != null
pre	this.type != null
post	init'ed(return_value)
test_vector	com.dmdirc.config.ConfigTarget_TYPE:equals(... )@228: {0}, {1}

bool equals(Object)

Kind	Annotation Text
pre	(soft) init'ed(obj.data)
pre	(soft) init'ed(obj.type)
pre	(soft) init'ed(this.type)
pre	(soft) this.data != null
post	init'ed(return_value)
test_vector	java.lang.String:equals(...)@212: {0}, {1}
test_vector	this.type == obj.type: {0}, {1}

String getData()

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

int getOrder()

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

ConfigTarget$TYPE getType()

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

String getTypeName()

Kind	Annotation Text
pre	(soft) init'ed(com.dmdirc.config.ConfigTarget$1__ static_init.new int[](ConfigTarget$1__static_init#1 )[...])
pre	this.type != null
presumption	com.dmdirc.config.ConfigTarget_TYPE:ordinal(... )@174 in {0..7}
post	return_value in Addr_Set{&"globaldefault", &"theme",&"profile",&"ircd", &"network",&"server",&"channel", &"global"}
test_vector	com.dmdirc.config.ConfigTarget$1__static_init.new int[](ConfigTarget$1__static_init#1)[...]: {1}, {2}, {3}, {4}, {5}, {6}, {7}, {-2³¹..0, 8..2³²-1}

int hashCode()

Kind	Annotation Text
pre	this.data != null
pre	this.type != null
presumption	com.dmdirc.config.ConfigTarget_TYPE:ordinal(... )@206 + java.lang.String:hashCode(...)@206 in {-2³¹..2³²-1}
post	init'ed(return_value)

void setChannel(String)

Kind	Annotation Text
post	init'ed(this.data)
post	this.data == channel
post	this.type == &com.dmdirc.config. ConfigTarget$TYPE__static_init.new ConfigTarget$TYP E(ConfigTarget$TYPE__static_init#8)

void setGlobal()

Kind	Annotation Text
post	this.data == &""
post	this.type == &com.dmdirc.config. ConfigTarget$TYPE__static_init.new ConfigTarget$TYP E(ConfigTarget$TYPE__static_init#2)

void setGlobalDefault()

Kind	Annotation Text
post	this.data == &""
post	this.type == &com.dmdirc.config. ConfigTarget$TYPE__static_init.new ConfigTarget$TYP E(ConfigTarget$TYPE__static_init#1)

void setIrcd(String)

Kind	Annotation Text
post	init'ed(this.data)
post	this.data == ircd
post	this.type == &com.dmdirc.config. ConfigTarget$TYPE__static_init.new ConfigTarget$TYP E(ConfigTarget$TYPE__static_init#5)

void setNetwork(String)

Kind	Annotation Text
post	init'ed(this.data)
post	this.data == network
post	this.type == &com.dmdirc.config. ConfigTarget$TYPE__static_init.new ConfigTarget$TYP E(ConfigTarget$TYPE__static_init#6)

void setOrder(int)

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

void setProfile()

Kind	Annotation Text
post	this.data == &""
post	this.type == &com.dmdirc.config. ConfigTarget$TYPE__static_init.new ConfigTarget$TYP E(ConfigTarget$TYPE__static_init#4)

void setServer(String)

Kind	Annotation Text
post	init'ed(this.data)
post	this.data == server
post	this.type == &com.dmdirc.config. ConfigTarget$TYPE__static_init.new ConfigTarget$TYP E(ConfigTarget$TYPE__static_init#7)

void setTheme()

Kind	Annotation Text
post	this.data == &""
post	this.type == &com.dmdirc.config. ConfigTarget$TYPE__static_init.new ConfigTarget$TYP E(ConfigTarget$TYPE__static_init#3)

String toString()

Kind	Annotation Text
pre	(soft) init'ed(com.dmdirc.config.ConfigTarget$1__ static_init.new int[](ConfigTarget$1__static_init#1 )[...])
pre	(soft) init'ed(this.data)
pre	this.type != null
presumption	com.dmdirc.config.ConfigTarget_TYPE:ordinal(... )@242 in {0..7}
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value in Addr_Set{&"Global defaults",&"Theme",&"Profile",&java. lang.StringBuilder:toString(...),&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...)...
test_vector	com.dmdirc.config.ConfigTarget$1__static_init.new int[](ConfigTarget$1__static_init#1)[...]: {1}, {2}, {3}, {4}, {5}, {6}, {7}, {-2³¹..0, 8..2³²-1}

ConfigTarget$TYPE valueOf(String)

Kind	Annotation Text
post	init'ed(return_value)

ConfigTarget$TYPE[] values()

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