ErrorLevel.java

ErrorLevel.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void com.dmdirc.logger.ErrorLevel(String, int, String, Icon)

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

com.dmdirc.logger.ErrorLevel__static_init

Kind	Annotation Text
post	"error"._tainted == 0
post	"info"._tainted == 0
post	"warning"._tainted == 0
post	$VALUES == &new ErrorLevel[](ErrorLevel__ static_init#6)
post	$VALUES.length == 5
post	$VALUES[0] == &new ErrorLevel(ErrorLevel__ static_init#1)
post	$VALUES[1] == &new ErrorLevel(ErrorLevel__ static_init#2)
post	$VALUES[2] == &new ErrorLevel(ErrorLevel__ static_init#3)
post	$VALUES[3] == &new ErrorLevel(ErrorLevel__ static_init#4)
post	$VALUES[4] == &new ErrorLevel(ErrorLevel__ static_init#5)
post	FATAL == &new ErrorLevel(ErrorLevel__static_ init#1)
post	FATAL.value == &"Fatal"
post	HIGH == &new ErrorLevel(ErrorLevel__static_ init#2)
post	HIGH.value == &"High"
post	LOW == &new ErrorLevel(ErrorLevel__static_ init#4)
post	LOW.value == &"Low"
post	MEDIUM == &new ErrorLevel(ErrorLevel__static_ init#3)
post	MEDIUM.value == &"Medium"
post	UNKNOWN == &new ErrorLevel(ErrorLevel__static_ init#5)
post	UNKNOWN.value == &"Unknown"
post	init'ed(FATAL.icon)
post	init'ed(HIGH.icon)
post	init'ed(LOW.icon)
post	init'ed(MEDIUM.icon)
post	init'ed(UNKNOWN.icon)
post	new ErrorLevel(ErrorLevel__static_init#1) num objects == 1
post	new ErrorLevel(ErrorLevel__static_init#2) num objects == 1
post	new ErrorLevel(ErrorLevel__static_init#3) num objects == 1
post	new ErrorLevel(ErrorLevel__static_init#4) num objects == 1
post	new ErrorLevel(ErrorLevel__static_init#5) num objects == 1
post	new ErrorLevel[](ErrorLevel__static_init#6) num objects == 1
unanalyzed	call on com.dmdirc.config.ConfigManager:getOption
unanalyzed	call on com.dmdirc.config.ConfigManager:hasOptionSt ring
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.util.URLBuilder:buildURL
unanalyzed	call on java.awt.Image:getScaledInstance
unanalyzed	call on java.awt.Toolkit:getDefaultToolkit
unanalyzed	call on java.awt.Toolkit:getImage
unanalyzed	call on java.lang.ClassLoader:getResource
unanalyzed	call on java.lang.Enum
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.Thread:currentThread
unanalyzed	call on java.lang.Thread:getContextClassLoader
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on javax.swing.ImageIcon

Icon getIcon()

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

bool moreImportant(ErrorLevel)

Kind	Annotation Text
post	init'ed(return_value)
test_vector	level: Inverse{null}, Addr_Set{null}

String toString()

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

ErrorLevel valueOf(String)

Kind	Annotation Text
post	init'ed(return_value)

ErrorLevel[] values()

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