ProgramError.java

ProgramError.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void checkResponses(List)

Kind	Annotation Text
pre	(soft) init'ed(com.dmdirc.ui.FatalErrorDialog$4__ static_init.new int[](FatalErrorDialog$4__static_in it#1)[...])
pre	(soft) this.fixedStatus != null
pre	(soft) this.reportStatus != null
pre	response != null
presumption	java.util.List:get(...)@322 != null
presumption	java.util.List:get(...)@335 != null
presumption	java.util.List:size(...)@322 >= -2³¹+1
post	this.fixedStatus != null
post	this.fixedStatus == One-of{old this.fixedStatus, &com.dmdirc.logger.ErrorFixedStatus__static_ init.new ErrorFixedStatus(ErrorFixedStatus__static_ init#1), &com.dmdirc.logger.ErrorFixedStatus__s tatic_init.new ErrorFixedStatus(ErrorFixedStatus...
post	this.reportStatus != null
post	this.reportStatus == One-of{old this.reportStatus, &com.dmdirc.logger.ErrorReportStatus__static_ init.new ErrorReportStatus(ErrorReportStatus__ static_init#4), &com.dmdirc.logger. ErrorReportStatus__static_init.new ErrorReportStatu s(ErrorRepo...
unanalyzed	call on com.dmdirc.logger.ErrorFixedStatus:equals
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:equals
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:ordinal
unanalyzed	call on com.dmdirc.util.ListenerList:get
unanalyzed	call on equals
unanalyzed	call on errorStatusChanged
unanalyzed	call on fireErrorStatusChanged
unanalyzed	call on getErrorManager
unanalyzed	call on getReportStatus
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.Object:notifyAll
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.Arrays:equals
unanalyzed	call on java.util.List:iterator
unanalyzed	call on javax.swing.JButton:setEnabled
unanalyzed	call on javax.swing.JButton:setText
test_vector	java.lang.String:equalsIgnoreCase(...)@322: {0}, {1}
test_vector	java.lang.String:matches(...)@336: {0}, {1}
test_vector	java.lang.String:matches(...)@338: {0}, {1}
test_vector	java.lang.String:matches(...)@340: {0}, {1}
test_vector	java.lang.String:matches(...)@342: {0}, {1}
test_vector	java.util.List:isEmpty(...)@322: {1}, {0}
test_vector	java.util.List:size(...)@330: {-2³¹..0, 2..2³²-1}, {1}

void com.dmdirc.logger.ProgramError(long, ErrorLevel, String, String[], Date)

Kind	Annotation Text
pre	date != null
pre	id >= 0
pre	level != null
pre	message != null
pre	trace != null
pre	trace.length <= 2³²-1
presumption	java.lang.String:isEmpty(...)@103 == 0
post	init'ed(this.trace)
post	this.date != null
post	this.fixedStatus == &com.dmdirc.logger. ErrorFixedStatus__static_init.new ErrorFixedStatus( ErrorFixedStatus__static_init#7)
post	this.id == id
post	this.id >= 0
post	this.level != null
post	this.level == level
post	this.message != null
post	this.message == message
post	this.reportStatus == &com.dmdirc.logger. ErrorReportStatus__static_init.new ErrorReportStatu s(ErrorReportStatus__static_init#6)

com.dmdirc.logger.ProgramError__static_init

Kind	Annotation Text
post	new Semaphore(ProgramError__static_init#1) num objects == 1
post	writingSem == &new Semaphore(ProgramError__ static_init#1)

bool equals(Object)

Kind	Annotation Text
pre	(soft) this.message != null
post	init'ed(return_value)
test_vector	java.lang.String:equals(...)@403: {1}, {0}
test_vector	java.util.Arrays:equals(...)@407: {1}, {0}
test_vector	obj: Inverse{null}, Addr_Set{null}
test_vector	this.level == obj.level: {1}, {0}

Date getDate()

Kind	Annotation Text
pre	this.date != null
post	return_value != null

OutputStream getErrorFile()

Kind	Annotation Text
pre	init'ed(errorDir)
pre	this.date != null
presumption	java.lang.System.err != null
post	errorDir != null
post	errorDir == One-of{old errorDir, &new File(getErrorFile#1)}
post	new File(getErrorFile#1) num objects <= 1
post	new FileOutputStream(getErrorFile#8) num objects <= 1
post	new NullOutputStream(getErrorFile#9) num objects <= 1
post	return_value in Addr_Set{&new FileOutputStream( getErrorFile#8),&new NullOutputStream(getErrorF ile#9)}
unanalyzed	call on java.io.OutputStream
unanalyzed	call on java.util.Date:clone
test_vector	errorDir: Addr_Set{null}, Inverse{null}
test_vector	java.io.File:exists(...)@245: {1}, {0}
test_vector	java.io.File:exists(...)@247: {1}, {0}
test_vector	java.io.File:exists(...)@256: {0}, {1}

ErrorFixedStatus getFixedStatus()

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

long getID()

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

ErrorLevel getLevel()

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

String getMessage()

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

ErrorReportStatus getReportStatus()

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

String getSourceLine()

Kind	Annotation Text
pre	(soft) this.trace[0] != null
pre	(soft) this.trace[...] != null
pre	this.trace != null
pre	this.trace.length in {1..2³²-1}
post	return_value != null
test_vector	java.lang.String:startsWith(...)@372: {0}, {1}

String[] getTrace()

Kind	Annotation Text
pre	this.trace != null
pre	this.trace.length <= 2³²-1
post	init'ed(return_value)

int hashCode()

Kind	Annotation Text
pre	this.level != null
pre	this.message != null
presumption	(com.dmdirc.logger.ErrorLevel:hashCode(...)@41867 + java.lang.String:hashCode(...)@419)67 + java.util.Arrays:hashCode(...)@420 in {-2_149_588_989..4_292_861_954}
presumption	com.dmdirc.logger.ErrorLevel:hashCode(...)@418 in {-65_539_622..33_486_689}
presumption	com.dmdirc.logger.ErrorLevel:hashCode(...)@418*67 + java.lang.String:hashCode(...)@419 in {-96_187_407..96_124_561}
post	init'ed(return_value)

bool isValidSource()

Kind	Annotation Text
pre	(soft) this.trace[0] != null
pre	(soft) this.trace[...] != null
pre	this.trace != null
pre	this.trace.length in {1..2³²-1}
post	init'ed(return_value)
unanalyzed	call on java.lang.String:startsWith

void save()

Kind	Annotation Text
pre	init'ed(errorDir)
pre	this.date != null
pre	this.trace != null
pre	this.trace.length <= 2³²-1
presumption	arr$.length <= 2³²-1
presumption	java.util.Arrays:copyOf(...)@148 != null
post	errorDir != null
post	errorDir == One-of{old errorDir, &new File(getErrorFile#1)}
post	new File(getErrorFile#1) num objects <= 1
unanalyzed	call on com.dmdirc.Main:getConfigDir
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:createNewFile
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.io.File:renameTo
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.IOException:printStackTrace
unanalyzed	call on java.io.OutputStream
unanalyzed	call on java.io.PrintStream:println
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.Arrays:copyOf
unanalyzed	call on java.util.Date:clone
unanalyzed	call on java.util.Date:getTime
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.util.concurrent.Semaphore:release

void send()

Kind	Annotation Text
pre	(soft) init'ed(com.dmdirc.ui.FatalErrorDialog$4__ static_init.new int[](FatalErrorDialog$4__static_in it#1)[...])
pre	(soft) this.fixedStatus != null
pre	(soft) this.reportStatus != null
pre	this.trace != null
pre	this.trace.length <= 2³²-1
presumption	com.dmdirc.config.IdentityManager:getGlobalConfig(. ..)@287 != null
presumption	com.dmdirc.util.Downloader:getPage(...)@300 != null
presumption	java.util.List:get(...)@310 != null
presumption	java.util.List:size(...)@310 >= -2³¹+1
presumption	this.fixedStatus@294 != null
presumption	this.reportStatus@294 != null
post	this.fixedStatus != null
post	this.reportStatus != null
unanalyzed	call on com.dmdirc.logger.ErrorFixedStatus:equals
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:equals
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:ordinal
unanalyzed	call on com.dmdirc.util.ListenerList:get
unanalyzed	call on equals
unanalyzed	call on errorStatusChanged
unanalyzed	call on fireErrorStatusChanged
unanalyzed	call on getErrorManager
unanalyzed	call on getReportStatus
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.Object:notifyAll
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:matches
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.Arrays:copyOf
unanalyzed	call on java.util.Arrays:equals
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:size
unanalyzed	call on javax.swing.JButton:setEnabled
unanalyzed	call on javax.swing.JButton:setText
test_vector	java.lang.String:equalsIgnoreCase(...)@310: {1}, {0}
test_vector	java.util.List:isEmpty(...)@310: {1}, {0}

void setFixedStatus(ErrorFixedStatus)

Kind	Annotation Text
pre	(soft) init'ed(com.dmdirc.ui.FatalErrorDialog$4__ static_init.new int[](FatalErrorDialog$4__static_in it#1)[...])
pre	(soft) this.fixedStatus != null
pre	(soft) this.reportStatus != null
post	this.fixedStatus != null
post	this.fixedStatus == One-of{old this.fixedStatus, newStatus}
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:ordinal
unanalyzed	call on com.dmdirc.util.ListenerList:get
unanalyzed	call on equals
unanalyzed	call on errorStatusChanged
unanalyzed	call on getReportStatus
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.Arrays:equals
unanalyzed	call on java.util.List:iterator
unanalyzed	call on javax.swing.JButton:setEnabled
unanalyzed	call on javax.swing.JButton:setText
test_vector	com.dmdirc.logger.ErrorFixedStatus:equals(... )@200: {1}, {0}
test_vector	newStatus: Addr_Set{null}, Inverse{null}

void setReportStatus(ErrorReportStatus)

Kind	Annotation Text
pre	(soft) init'ed(com.dmdirc.ui.FatalErrorDialog$4__ static_init.new int[](FatalErrorDialog$4__static_in it#1)[...])
pre	(soft) this.reportStatus != null
post	this.reportStatus != null
post	this.reportStatus == One-of{old this.reportStatus, newStatus}
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:ordinal
unanalyzed	call on com.dmdirc.util.ListenerList:get
unanalyzed	call on equals
unanalyzed	call on errorStatusChanged
unanalyzed	call on getReportStatus
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.Arrays:equals
unanalyzed	call on java.util.List:iterator
unanalyzed	call on javax.swing.JButton:setEnabled
unanalyzed	call on javax.swing.JButton:setText
test_vector	com.dmdirc.logger.ErrorReportStatus:equals(... )@184: {1}, {0}
test_vector	newStatus: Addr_Set{null}, Inverse{null}

String toString()

Kind	Annotation Text
pre	init'ed(this.reportStatus)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &java.lang.StringBuilder:toStri ng(...)