Messages

Last Msg First Msg

method	com.dmdirc.logger.ProgramError__static_init
post	writingSem == &new Semaphore(ProgramError__ static_init#1)
post	new Semaphore(ProgramError__static_init#1) num objects == 1

method	void com.dmdirc.logger.ProgramError(long, ErrorLevel, String, String[], Date)
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	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 == level
post	this.level != null
post	this.message == message
post	this.message != null
post	this.reportStatus == &com.dmdirc.logger. ErrorReportStatus__static_init.new ErrorReportStatu s(ErrorReportStatus__static_init#6)
post	init'ed(this.trace)

method	ErrorLevel getLevel()
post	return_value == this.level
post	init'ed(return_value)

method	String getMessage()
post	return_value == this.message
post	init'ed(return_value)

method	String[] getTrace()
pre	this.trace != null
pre	this.trace.length <= 2³²-1
post	init'ed(return_value)

method	Date getDate()
pre	this.date != null
post	return_value != null

method	ErrorReportStatus getReportStatus()
pre	init'ed(this.reportStatus)
post	return_value == this.reportStatus
post	init'ed(return_value)

method	ErrorFixedStatus getFixedStatus()
pre	init'ed(this.fixedStatus)
post	return_value == this.fixedStatus
post	init'ed(return_value)

method	void setReportStatus(ErrorReportStatus)
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 == One-of{old this.reportStatus, newStatus}
post	this.reportStatus != null
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.Arrays:equals
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on com.dmdirc.util.ListenerList:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:ordinal
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on javax.swing.JButton:setEnabled
unanalyzed	call on equals
unanalyzed	call on getReportStatus
unanalyzed	call on errorStatusChanged
test_vector	newStatus: Addr_Set{null}, Inverse{null}
test_vector	com.dmdirc.logger.ErrorReportStatus:equals(... )@184: {1}, {0}

method not available - call not analyzed Info call on bool com.dmdirc.logger.ErrorReportStatus:eq uals(Object)

method	void setFixedStatus(ErrorFixedStatus)
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 == One-of{old this.fixedStatus, newStatus}
post	this.fixedStatus != null
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.Arrays:equals
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on com.dmdirc.util.ListenerList:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:ordinal
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on javax.swing.JButton:setEnabled
unanalyzed	call on equals
unanalyzed	call on getReportStatus
unanalyzed	call on errorStatusChanged
test_vector	newStatus: Addr_Set{null}, Inverse{null}
test_vector	com.dmdirc.logger.ErrorFixedStatus:equals(... )@200: {1}, {0}

method not available - call not analyzed Info call on bool com.dmdirc.logger.ErrorFixedStatus:equ als(Object)

method	long getID()
post	return_value == this.id
post	init'ed(return_value)

method	void save()
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 == One-of{old errorDir, &new File(getErrorFile#1)}
post	errorDir != null
post	new File(getErrorFile#1) num objects <= 1
unanalyzed	call on java.util.Arrays:copyOf
unanalyzed	call on java.util.Date:clone
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.concurrent.Semaphore:acquireUnint erruptibly
unanalyzed	call on java.io.File:exists
unanalyzed	call on com.dmdirc.Main:getConfigDir
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.util.Date:getTime
unanalyzed	call on java.io.File:renameTo
unanalyzed	call on java.io.File:createNewFile
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on java.io.PrintStream:println
unanalyzed	call on java.io.IOException:printStackTrace
unanalyzed	call on java.io.OutputStream

method	OutputStream getErrorFile()
pre	init'ed(errorDir)
pre	this.date != null
presumption	java.lang.System.err != null
post	errorDir == One-of{old errorDir, &new File(getErrorFile#1)}
post	errorDir != null
post	return_value in Addr_Set{&new FileOutputStream( getErrorFile#8),&new NullOutputStream(getErrorF ile#9)}
post	new File(getErrorFile#1) num objects <= 1
post	new FileOutputStream(getErrorFile#8) num objects <= 1
post	new NullOutputStream(getErrorFile#9) num objects <= 1
unanalyzed	call on java.util.Date:clone
unanalyzed	call on java.io.OutputStream
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}

method not available - call not analyzed Info call on String com.dmdirc.Main:getConfigDir()

Prev Msg Next Msg

overflow

click for all messages in this file Low Prob.

check that i in {-2³¹-1..2³²-2}

Prev Msg Next Msg

method	void send()
pre	this.trace != null
pre	this.trace.length <= 2³²-1
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
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 java.util.Arrays:copyOf
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:equals
unanalyzed	call on getErrorManager
unanalyzed	call on fireErrorStatusChanged
unanalyzed	call on java.lang.Object:notifyAll
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on com.dmdirc.logger.ErrorFixedStatus:equals
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:matches
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.Arrays:equals
unanalyzed	call on com.dmdirc.util.ListenerList:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:ordinal
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on javax.swing.JButton:setEnabled
unanalyzed	call on equals
unanalyzed	call on getReportStatus
unanalyzed	call on errorStatusChanged
test_vector	java.lang.String:equalsIgnoreCase(...)@310: {1}, {0}
test_vector	java.util.List:isEmpty(...)@310: {1}, {0}

method not available - call not analyzed Info call on ConfigManager com.dmdirc.config. IdentityManager:getGlobalConfig()

method not available - call not analyzed Info call on String com.dmdirc.config.ConfigManager:getO ption(String, String)

method not available - call not analyzed Info call on List com.dmdirc.util.Downloader:getPage(Str ing, Map)

method	void checkResponses(List)
pre	response != null
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
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 == 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.fixedStatus != 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...
post	this.reportStatus != null
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:equals
unanalyzed	call on getErrorManager
unanalyzed	call on fireErrorStatusChanged
unanalyzed	call on java.lang.Object:notifyAll
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on com.dmdirc.logger.ErrorFixedStatus:equals
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.Arrays:equals
unanalyzed	call on com.dmdirc.util.ListenerList:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on com.dmdirc.logger.ErrorReportStatus:ordinal
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on javax.swing.JButton:setEnabled
unanalyzed	call on equals
unanalyzed	call on getReportStatus
unanalyzed	call on errorStatusChanged
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}

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

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

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

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

method	int hashCode()
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)

method not available - call not analyzed Info call on int com.dmdirc.logger.ErrorLevel:hashCode()

	method not available - call not analyzed	Info	call on ConfigManager com.dmdirc.config. IdentityManager:getGlobalConfig()
	method not available - call not analyzed	Info	call on String com.dmdirc.config.ConfigManager:getO ption(String, String)