DCCSend.java

DCCSend.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

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

Kind	Annotation Text

com.dmdirc.addons.dcc.DCCSend$TransferType__static_init

Kind	Annotation Text
post	$VALUES == &new DCCSend$TransferType[](DCCSend$ TransferType__static_init#3)
post	$VALUES.length == 2
post	$VALUES[0] == &new DCCSend$TransferType(DCCSend $TransferType__static_init#1)
post	$VALUES[1] == &new DCCSend$TransferType(DCCSend $TransferType__static_init#2)
post	RECEIVE == &new DCCSend$TransferType(DCCSend$Tr ansferType__static_init#2)
post	SEND == &new DCCSend$TransferType(DCCSend$Trans ferType__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
unanalyzed	call on java.lang.Enum

void com.dmdirc.addons.dcc.DCCSend()

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

void com.dmdirc.addons.dcc.DCCSend(int)

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

com.dmdirc.addons.dcc.DCCSend__static_init

Kind	Annotation Text
post	SENDS == &new ArrayList(DCCSend__static_ init#1)
post	new ArrayList(DCCSend__static_init#1) num objects == 1

DCCSend findByToken(String)

Kind	Annotation Text
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	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}
test_vector	token: Addr_Set{null}, Inverse{null}

String getFileName()

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

long getFileSize()

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

int getFileStart()

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

List getSends()

Kind	Annotation Text
post	new ArrayList(getSends#1) num objects == 1
post	return_value == &new ArrayList(getSends#1)

String getShortFileName()

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

String getToken()

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

DCCSend$TransferType getType()

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

bool handleReceive()

Kind	Annotation Text
pre	(soft) init'ed(this.handler)
pre	(soft) init'ed(this.size)
pre	(soft) this.blockSize >= 0
pre	(soft) this.fileOut != null
pre	(soft) this.in != null
pre	(soft) this.out != null
pre	(soft) this.readSize in {-6_442_450_943.. 6_442_450_943}
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	java.io.DataInputStream:read(...)@367: {0}, {1..2³²-1}, {-2³¹..-1}
test_vector	this.handler: Addr_Set{null}, Inverse{null}

bool handleSend()

Kind	Annotation Text
pre	(soft) init'ed(this.handler)
pre	(soft) init'ed(this.readSize)
pre	(soft) init'ed(this.size)
pre	(soft) init'ed(this.turbo)
pre	(soft) this.blockSize >= 0
pre	(soft) this.fileIn != null
pre	(soft) this.in != null
pre	(soft) this.out != null
presumption	this.readSize + java.io.DataInputStream:read(... )@401 in {-2⁶³.. 2⁶⁴-1}
post	init'ed(return_value)
post	init'ed(this.readSize)
post	this.handler.transferCount == old this.handler. transferCount
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}
test_vector	this.handler: Addr_Set{null}, Inverse{null}
test_vector	this.turbo: {1}, {0}

bool handleSocket()

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

bool isTurbo()

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

String makeToken()

Kind	Annotation Text
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.String:equals
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:iterator

void removeFromSends()

Kind	Annotation Text

void reset()

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

void setFileName(String)

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

void setFileSize(long)

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

int setFileStart(int)

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

void setHandler(DCCSendInterface)

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

void setToken(String)

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

void setTurbo(bool)

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

void setType(DCCSend$TransferType)

Kind	Annotation Text
post	init'ed(this.transferType)
post	this.transferType == type

void socketClosed()

Kind	Annotation Text
pre	init'ed(this.handler)
pre	init'ed(this.in)
pre	init'ed(this.out)
post	this.in == null
post	this.out == null
test_vector	this.handler: Addr_Set{null}, Inverse{null}
test_vector	this.in: Addr_Set{null}, Inverse{null}
test_vector	this.out: Addr_Set{null}, Inverse{null}

void socketOpened()

Kind	Annotation Text
pre	(soft) init'ed(this.filename)
pre	(soft) init'ed(this.in)
pre	(soft) init'ed(this.out)
pre	(soft) init'ed(this.startpos)
pre	(soft) init'ed(this.transferType)
pre	(soft) this.socket != null
pre	init'ed(this.handler)
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
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}
unanalyzed	call on com.dmdirc.interfaces.ActionListener:proces sEvent
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on com.dmdirc.util.MapList:containsKey
unanalyzed	call on com.dmdirc.util.MapList:get
unanalyzed	call on getArity
unanalyzed	call on getType
unanalyzed	call on isWindowClosing
unanalyzed	call on java.io.DataInputStream:close
unanalyzed	call on java.io.DataOutputStream:close
unanalyzed	call on java.lang.Double:valueOf
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.Math:floor
unanalyzed	call on java.lang.String:format
unanalyzed	call on java.lang.System:currentTimeMillis
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on java.util.List:remove
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on javax.swing.JLabel:setText
unanalyzed	call on javax.swing.JProgressBar:setValue
unanalyzed	call on setIcon
unanalyzed	call on socketClosed
unanalyzed	call on trigger
test_vector	this.handler: Addr_Set{null}, Inverse{null}

DCCSend$TransferType valueOf(String)

Kind	Annotation Text
post	init'ed(return_value)

DCCSend$TransferType[] values()

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