method

com.dmdirc.parser.irc.Logging__static_init

method	Logging$LogLevel[] values()
pre	(soft) init'ed($VALUES[...])
post	return_value == &new Logging$LogLevel[](values# 1)
post	new Logging$LogLevel[](values#1) num objects == 1
post	return_value.length == 6
post	return_value[...] == One-of{$VALUES[...], undefined}

method	Logging$LogLevel valueOf(String)
post	init'ed(return_value)

method	com.dmdirc.parser.irc.Logging$LogLevel__static_ init
post	$VALUES == &new Logging$LogLevel[](Logging$LogL evel__static_init#7)
post	DEBUG == &new Logging$LogLevel(Logging$LogLevel __static_init#2)
post	$VALUES[1] == &new Logging$LogLevel(Logging$Log Level__static_init#2)
post	ERROR == &new Logging$LogLevel(Logging$LogLevel __static_init#5)
post	$VALUES[4] == &new Logging$LogLevel(Logging$Log Level__static_init#5)
post	FATAL == &new Logging$LogLevel(Logging$LogLevel __static_init#6)
post	$VALUES[5] == &new Logging$LogLevel(Logging$Log Level__static_init#6)
post	INFO == &new Logging$LogLevel(Logging$LogLevel_ _static_init#3)
post	$VALUES[2] == &new Logging$LogLevel(Logging$Log Level__static_init#3)
post	TRACE == &new Logging$LogLevel(Logging$LogLevel __static_init#1)
post	$VALUES[0] == &new Logging$LogLevel(Logging$Log Level__static_init#1)
post	WARN == &new Logging$LogLevel(Logging$LogLevel_ _static_init#4)
post	$VALUES[3] == &new Logging$LogLevel(Logging$Log Level__static_init#4)
post	new Logging$LogLevel(Logging$LogLevel__static_ init#1) num objects == 1
post	new Logging$LogLevel(Logging$LogLevel__static_ init#2) num objects == 1
post	new Logging$LogLevel(Logging$LogLevel__static_ init#3) num objects == 1
post	new Logging$LogLevel(Logging$LogLevel__static_ init#4) num objects == 1
post	new Logging$LogLevel(Logging$LogLevel__static_ init#5) num objects == 1
post	new Logging$LogLevel(Logging$LogLevel__static_ init#6) num objects == 1
post	new Logging$LogLevel[](Logging$LogLevel__static_ init#7) num objects == 1
post	TRACE.checkMethodName == &"isTraceEnabled"
post	TRACE.methodName == &"trace"
post	DEBUG.checkMethodName == &"isDebugEnabled"
post	DEBUG.methodName == &"debug"
post	INFO.checkMethodName == &"isInfoEnabled"
post	INFO.methodName == &"info"
post	WARN.checkMethodName == &"isWarnEnabled"
post	WARN.methodName == &"warn"
post	ERROR.checkMethodName == &"isErrorEnabled"
post	ERROR.methodName == &"error"
post	FATAL.checkMethodName == &"isFatalEnabled"
post	FATAL.methodName == &"fatal"
post	$VALUES.length == 6
unanalyzed	call on java.lang.Enum

method	void com.dmdirc.parser.irc.Logging$LogLevel(String , int, String, String)
post	this.checkMethodName == checkMethodName
post	init'ed(this.checkMethodName)
post	this.methodName == methodName
post	init'ed(this.methodName)

method	String getMethodName()
post	return_value == this.methodName
post	init'ed(return_value)

method	String getCheckMethodName()
post	return_value == this.checkMethodName
post	init'ed(return_value)

method	Logging getLogging()
pre	init'ed(me)
post	me == One-of{old me, &new Logging(getLogging#1) }
post	me != null
post	return_value == me
post	new Logging(getLogging#1) num objects <= 1
post	init'ed(new Logging(getLogging#1).isAvailable)
post	init'ed(new Logging(getLogging#1).log)
unanalyzed	call on java.lang.Class:forName
unanalyzed	call on java.lang.Class:getMethod
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.reflect.Method:invoke
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
test_vector	me: Inverse{null}, Addr_Set{null}

method	void com.dmdirc.parser.irc.Logging()
presumption	java.lang.Class:getMethod(...)@104 != null
post	init'ed(this.isAvailable)
post	init'ed(this.log)
test_vector	java.lang.Class:forName(...)@100: Addr_Set{null}, Inverse{null}

method	bool levelEnabled(Logging$LogLevel)
pre	(soft) level != null
pre	(soft) this.log != null
presumption	java.lang.Class:getMethod(...)@124 != null
presumption	java.lang.Object:getClass(...)@124 != null
presumption	java.lang.reflect.Method:invoke(...)@125 != null
post	init'ed(return_value)
test_vector	this.isAvailable: {0}, {1}

method	void log(Logging$LogLevel, String)
pre	(soft) level != null
pre	(soft) this.log != null
unanalyzed	call on java.lang.Class:getMethod
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.reflect.Method:invoke
unanalyzed	call on java.lang.Throwable:__curr_excep_obj

method	void log(Logging$LogLevel, String, Throwable)
pre	(soft) level != null
pre	(soft) this.log != null
presumption	java.lang.Class:getMethod(...)@156 != null
presumption	java.lang.Class:getMethod(...)@159 != null
presumption	java.lang.Object:getClass(...)@156 != null
presumption	java.lang.Object:getClass(...)@159 != null
test_vector	this.isAvailable: {1}, {0}
test_vector	throwable: Inverse{null}, Addr_Set{null}