ErrorReportStatus.java

ErrorReportStatus.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.ErrorReportStatus(String, int, String, bool)

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

com.dmdirc.logger.ErrorReportStatus__static_init

Kind	Annotation Text
post	$VALUES == &new ErrorReportStatus[](ErrorReport Status__static_init#7)
post	$VALUES.length == 6
post	$VALUES[0] == &new ErrorReportStatus(ErrorRepor tStatus__static_init#1)
post	$VALUES[1] == &new ErrorReportStatus(ErrorRepor tStatus__static_init#2)
post	$VALUES[2] == &new ErrorReportStatus(ErrorRepor tStatus__static_init#3)
post	$VALUES[3] == &new ErrorReportStatus(ErrorRepor tStatus__static_init#4)
post	$VALUES[4] == &new ErrorReportStatus(ErrorRepor tStatus__static_init#5)
post	$VALUES[5] == &new ErrorReportStatus(ErrorRepor tStatus__static_init#6)
post	ERROR == &new ErrorReportStatus(ErrorReportStat us__static_init#4)
post	ERROR.terminal == 1
post	ERROR.value == &"Error sending"
post	FINISHED == &new ErrorReportStatus(ErrorReportS tatus__static_init#2)
post	FINISHED.terminal == 1
post	FINISHED.value == &"Finished"
post	NOT_APPLICABLE == &new ErrorReportStatus(ErrorR eportStatus__static_init#1)
post	NOT_APPLICABLE.terminal == 1
post	NOT_APPLICABLE.value == &"Not applicable"
post	QUEUED == &new ErrorReportStatus(ErrorReportSta tus__static_init#5)
post	QUEUED.terminal == 0
post	QUEUED.value == &"Queued"
post	SENDING == &new ErrorReportStatus(ErrorReportSt atus__static_init#3)
post	SENDING.terminal == 0
post	SENDING.value == &"Sending..."
post	WAITING == &new ErrorReportStatus(ErrorReportSt atus__static_init#6)
post	WAITING.terminal == 1
post	WAITING.value == &"Waiting"
post	new ErrorReportStatus(ErrorReportStatus__static_ init#1) num objects == 1
post	new ErrorReportStatus(ErrorReportStatus__static_ init#2) num objects == 1
post	new ErrorReportStatus(ErrorReportStatus__static_ init#3) num objects == 1
post	new ErrorReportStatus(ErrorReportStatus__static_ init#4) num objects == 1
post	new ErrorReportStatus(ErrorReportStatus__static_ init#5) num objects == 1
post	new ErrorReportStatus(ErrorReportStatus__static_ init#6) num objects == 1
post	new ErrorReportStatus[](ErrorReportStatus__static_ init#7) num objects == 1
unanalyzed	call on java.lang.Enum

bool isTerminal()

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

String toString()

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

ErrorReportStatus valueOf(String)

Kind	Annotation Text
post	init'ed(return_value)

ErrorReportStatus[] values()

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