Messages

Last Msg First Msg

method	com.dmdirc.addons.dcc.DCCSend__static_init
post	SENDS == &new ArrayList(DCCSend__static_ init#1)
post	new ArrayList(DCCSend__static_init#1) num objects == 1

method	DCCSend$TransferType[] values()
pre	(soft) init'ed($VALUES[...])
post	return_value == &new DCCSend$TransferType[](val ues#1)
post	new DCCSend$TransferType[](values#1) num objects == 1
post	return_value.length == 2
post	return_value[...] == One-of{$VALUES[...], undefined}

method	DCCSend$TransferType valueOf(String)
post	init'ed(return_value)

method

void com.dmdirc.addons.dcc.DCCSend$TransferType(St ring, int)

method	com.dmdirc.addons.dcc.DCCSend$TransferType__ static_init
post	$VALUES == &new DCCSend$TransferType[](DCCSend$ TransferType__static_init#3)
post	RECEIVE == &new DCCSend$TransferType(DCCSend$Tr ansferType__static_init#2)
post	$VALUES[1] == &new DCCSend$TransferType(DCCSend $TransferType__static_init#2)
post	SEND == &new DCCSend$TransferType(DCCSend$Trans ferType__static_init#1)
post	$VALUES[0] == &new DCCSend$TransferType(DCCSend $TransferType__static_init#1)
post	new DCCSend$TransferType(DCCSend$TransferType__ static_init#1) num objects == 1
post	new DCCSend$TransferType(DCCSend$TransferType__ static_init#2) num objects == 1
post	new DCCSend$TransferType[](DCCSend$TransferType__ static_init#3) num objects == 1
post	$VALUES.length == 2
unanalyzed	call on java.lang.Enum

method	void com.dmdirc.addons.dcc.DCCSend()
post	this.address == 0
post	this.listen == 0
post	this.port == 0
post	this.running == 0
post	this.turbo == 0
post	this.blockSize == 1_024
post	this.filename == &""
post	this.token == &""
post	this.serverListeningSem == &new Semaphore(DCC#2)
post	this.serverSocketSem == &new Semaphore(DCC#1)
post	this.size == -1
post	this.transferType == &com.dmdirc.addons.dcc. DCCSend$TransferType__static_init.new DCCSend$TransferType(DCCSend$TransferType__static_ init#2)
post	new Semaphore(DCC#1) num objects == 1
post	new Semaphore(DCC#2) num objects == 1
unanalyzed	call on java.util.concurrent.Semaphore
unanalyzed	call on java.util.List:add
unanalyzed	call on java.lang.Throwable:__curr_excep_obj

method	void com.dmdirc.addons.dcc.DCCSend(int)
post	this.address == 0
post	this.listen == 0
post	this.port == 0
post	this.running == 0
post	this.turbo == 0
post	this.blockSize == blockSize
post	init'ed(this.blockSize)
post	this.filename == &""
post	this.token == &""
post	this.serverListeningSem == &new Semaphore(DCC#2)
post	this.serverSocketSem == &new Semaphore(DCC#1)
post	this.size == -1
post	this.transferType == &com.dmdirc.addons.dcc. DCCSend$TransferType__static_init.new DCCSend$TransferType(DCCSend$TransferType__static_ init#2)
post	new Semaphore(DCC#1) num objects == 1
post	new Semaphore(DCC#2) num objects == 1
unanalyzed	call on java.util.concurrent.Semaphore

method	void reset()
pre	init'ed(this.filename)
pre	init'ed(this.startpos)
pre	this.serverSocketSem != null
pre	init'ed(this.transferType)
pre	(soft) init'ed(this.fileIn)
pre	(soft) init'ed(this.serverSocket)
pre	(soft) init'ed(this.socket)
pre	(soft) this.serverListeningSem != null
post	this.fileIn == One-of{old this.fileIn, &new DataInputStream(setFileName#2), null}
post	init'ed(this.fileIn)
post	this.filename == old this.filename
post	init'ed(this.filename)
post	possibly_updated(this.in)
post	possibly_updated(this.out)
post	this.readSize == One-of{old this.startpos, old this.readSize}
post	this.serverSocket == null
post	this.socket == null
post	init'ed(this.startpos)
post	this.transferFile == One-of{old this.transferFile, &new File(setFileName#1)}
post	new DataInputStream(setFileName#2) num objects <= 1
post	new File(setFileName#1) num objects <= 1
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:remove
unanalyzed	call on java.io.File
unanalyzed	call on java.io.DataInputStream:skipBytes
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.DataInputStream
unanalyzed	call on java.io.DataOutputStream:close
unanalyzed	call on java.io.DataInputStream:close
unanalyzed	call on socketClosed
unanalyzed	call on java.util.concurrent.Semaphore:release
unanalyzed	call on java.util.concurrent.Semaphore:tryAcquire
unanalyzed	call on java.lang.Thread:sleep
unanalyzed	call on java.net.ServerSocket:isClosed
unanalyzed	call on java.net.ServerSocket:close
unanalyzed	call on java.net.Socket:isClosed
unanalyzed	call on java.net.Socket:close
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.String:format
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on getType
unanalyzed	call on com.dmdirc.util.MapList:containsKey
unanalyzed	call on com.dmdirc.util.MapList:get
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on trigger
unanalyzed	call on getArity
unanalyzed	call on com.dmdirc.interfaces.ActionListener:proces sEvent
unanalyzed	call on javax.swing.JLabel:setText
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on setIcon
unanalyzed	call on java.lang.Math:floor
unanalyzed	call on javax.swing.JProgressBar:setValue
unanalyzed	call on java.lang.Double:valueOf
unanalyzed	call on isWindowClosing
unanalyzed	call on addLine

method	List getSends()
post	return_value == &new ArrayList(getSends#1)
post	new ArrayList(getSends#1) num objects == 1

method

void removeFromSends()

method	void setFileName(String)
pre	init'ed(this.transferType)
post	this.fileIn == One-of{old this.fileIn, &new DataInputStream(setFileName#2), null}
post	this.filename == filename
post	init'ed(this.filename)
post	this.transferFile == One-of{old this.transferFile, &new File(setFileName#1)}
post	new DataInputStream(setFileName#2) num objects <= 1
post	new File(setFileName#1) num objects <= 1

method	String getFileName()
pre	init'ed(this.filename)
post	return_value == this.filename
post	init'ed(return_value)

method	String getShortFileName()
pre	init'ed(this.filename)
post	init'ed(return_value)

method	void setType(DCCSend$TransferType)
post	this.transferType == type
post	init'ed(this.transferType)

method	DCCSend$TransferType getType()
pre	init'ed(this.transferType)
post	return_value == this.transferType
post	init'ed(return_value)

method	void setTurbo(bool)
post	this.turbo == turbo
post	init'ed(this.turbo)

method	bool isTurbo()
pre	init'ed(this.turbo)
post	return_value == this.turbo
post	init'ed(return_value)

method	void setToken(String)
post	this.token == token
post	init'ed(this.token)

method	String getToken()
pre	init'ed(this.token)
post	return_value == this.token
post	init'ed(return_value)

method	String makeToken()
pre	init'ed(this.filename)
post	java.lang.Integer:toString(...)._tainted == 0
post	return_value == &java.lang.Integer:toString(... )
post	this.token == &java.lang.Integer:toString(...)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.lang.String:equals

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into unique

Prev Msg Next Msg

method	DCCSend findByToken(String)
presumption	java.util.Iterator:next(...)@241 != null
presumption	send.token@241 != null
post	init'ed(return_value)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayList
test_vector	token: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:equals(...)@242: {0}, {1}
test_vector	java.lang.String:isEmpty(...)@240: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@241: {0}, {1}

method	void setFileSize(long)
post	this.size == size
post	init'ed(this.size)

method	long getFileSize()
pre	init'ed(this.size)
post	return_value == this.size
post	init'ed(return_value)

method	int setFileStart(int)
pre	init'ed(this.transferType)
pre	(soft) init'ed(this.fileIn)
post	init'ed(return_value)
post	this.readSize == One-of{startpos, old this.readSize}
post	init'ed(this.startpos)
test_vector	this.fileIn: Addr_Set{null}, Inverse{null}

method	int getFileStart()
pre	init'ed(this.startpos)
post	return_value == this.startpos
post	init'ed(return_value)

method	void setHandler(DCCSendInterface)
post	this.handler == handler
post	init'ed(this.handler)

method	void socketOpened()
pre	init'ed(this.handler)
pre	(soft) init'ed(this.in)
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.filename)
pre	(soft) this.socket != null
pre	(soft) init'ed(this.startpos)
pre	(soft) init'ed(this.transferType)
post	this.fileOut == One-of{old this.fileOut, &new DataOutputStream(socketOpened#2)}
post	this.handler.timeStarted == old this.handler. timeStarted
post	this.in in Addr_Set{null,&new DataInputStream(s ocketOpened#5)}
post	this.out in Addr_Set{null,&new DataOutputStream (socketOpened#4)}
post	this.transferFile == One-of{&new File(socketOpened#1), old this.transferFile}
post	new DataInputStream(socketOpened#5) num objects <= 1
post	new DataOutputStream(socketOpened#2) num objects <= 1
post	new DataOutputStream(socketOpened#4) num objects <= 1
post	new File(socketOpened#1) num objects <= 1
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:remove
unanalyzed	call on java.io.DataOutputStream:close
unanalyzed	call on java.io.DataInputStream:close
unanalyzed	call on socketClosed
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.String:format
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on getType
unanalyzed	call on com.dmdirc.util.MapList:containsKey
unanalyzed	call on com.dmdirc.util.MapList:get
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on trigger
unanalyzed	call on getArity
unanalyzed	call on com.dmdirc.interfaces.ActionListener:proces sEvent
unanalyzed	call on javax.swing.JLabel:setText
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on setIcon
unanalyzed	call on java.lang.Math:floor
unanalyzed	call on javax.swing.JProgressBar:setValue
unanalyzed	call on java.lang.Double:valueOf
unanalyzed	call on isWindowClosing
test_vector	this.handler: Addr_Set{null}, Inverse{null}

call too complex - analysis skipped Info call on void socketOpened(DCCSend)

method	void socketClosed()
pre	init'ed(this.in)
pre	init'ed(this.out)
pre	init'ed(this.handler)
post	this.in == null
post	this.out == null
test_vector	this.in: Addr_Set{null}, Inverse{null}
test_vector	this.out: Addr_Set{null}, Inverse{null}
test_vector	this.handler: Addr_Set{null}, Inverse{null}

call too complex - analysis skipped Info call on void socketClosed(DCCSend)

method	bool handleSocket()
pre	init'ed(this.out)
pre	(soft) this.readSize in {-6_442_450_943.. 6_442_450_943}
pre	(soft) this.blockSize >= 0
pre	(soft) this.fileIn != null
pre	(soft) this.fileOut != null
pre	(soft) init'ed(this.handler)
pre	(soft) init'ed(this.in)
pre	(soft) init'ed(this.size)
pre	(soft) init'ed(this.transferType)
pre	(soft) init'ed(this.turbo)
post	init'ed(return_value)
post	possibly_updated(this.handler.transferCount)
post	init'ed(this.readSize)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.io.DataOutputStream:close
unanalyzed	call on java.io.DataInputStream:close
unanalyzed	call on java.io.DataInputStream:read
unanalyzed	call on dataTransfered
unanalyzed	call on java.io.DataOutputStream:write
unanalyzed	call on java.io.DataOutputStream:flush
unanalyzed	call on java.io.DataInputStream:readInt
unanalyzed	call on java.io.DataOutputStream:writeInt
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.String:format
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on getType
unanalyzed	call on com.dmdirc.util.MapList:containsKey
unanalyzed	call on com.dmdirc.util.MapList:get
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on trigger
unanalyzed	call on getArity
unanalyzed	call on com.dmdirc.interfaces.ActionListener:proces sEvent
unanalyzed	call on javax.swing.JLabel:setText
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on updateSpeedAndTime
unanalyzed	call on java.lang.Math:floor
unanalyzed	call on javax.swing.JProgressBar:setValue
unanalyzed	call on java.lang.Double:valueOf
unanalyzed	call on java.lang.Integer:valueOf
test_vector	this.in: Inverse{null}, Addr_Set{null}
test_vector	this.out: Addr_Set{null}, Inverse{null}

method	bool handleReceive()
pre	(soft) this.readSize in {-6_442_450_943.. 6_442_450_943}
pre	(soft) this.blockSize >= 0
pre	(soft) this.fileOut != null
pre	(soft) init'ed(this.handler)
pre	(soft) this.in != null
pre	(soft) this.out != null
pre	(soft) init'ed(this.size)
presumption	this.readSize + java.io.DataInputStream:read(... )@367 in {-2³¹..2³²-1}
post	init'ed(return_value)
post	this.handler.transferCount == old this.handler. transferCount
post	this.readSize in {-6_442_450_943..6_442_450_943}
test_vector	this.handler: Addr_Set{null}, Inverse{null}
test_vector	java.io.DataInputStream:read(...)@367: {0}, {1..2³²-1}, {-2³¹..-1}

call too complex - analysis skipped Info call on void dataTransfered(DCCSend, int)

method	bool handleSend()
pre	(soft) init'ed(this.readSize)
pre	(soft) this.blockSize >= 0
pre	(soft) this.fileIn != null
pre	(soft) init'ed(this.handler)
pre	(soft) this.in != null
pre	(soft) this.out != null
pre	(soft) init'ed(this.size)
pre	(soft) init'ed(this.turbo)
presumption	this.readSize + java.io.DataInputStream:read(... )@401 in {-2⁶³.. 2⁶⁴-1}
post	init'ed(return_value)
post	this.handler.transferCount == old this.handler. transferCount
post	init'ed(this.readSize)
test_vector	this.handler: Addr_Set{null}, Inverse{null}
test_vector	this.turbo: {1}, {0}
test_vector	java.io.DataInputStream:read(...)@401: {0}, {1..2³²-1}, {-2³¹..-1}
test_vector	java.io.DataInputStream:readInt(...)@429: {-2³¹..0}, {1..2³²-1}

call too complex - analysis skipped Info call on void dataTransfered(DCCSend, int)