Messages

Last Msg First Msg

method

com.dmdirc.addons.dcc.DCC__static_init

method	void com.dmdirc.addons.dcc.DCC()
post	this.address == 0
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	new Semaphore(DCC#1) num objects == 1
post	new Semaphore(DCC#2) num objects == 1

method	void connect()
pre	(soft) init'ed(this.address)
pre	(soft) init'ed(this.port)
pre	(soft) init'ed(this.listen)
pre	(soft) this.serverSocket != null
post	this.address == One-of{old this.address, 0}
post	init'ed(this.address)
post	possibly_updated(this.fileOut)
post	this.handler.timeStarted == old this.handler. timeStarted
post	possibly_updated(this.in)
post	this.myThread == One-of{old this.myThread, &new Thread(connect#2)}
post	possibly_updated(this.out)
post	init'ed(this.port)
post	this.socket == One-of{old this.socket, &new Socket(connect#1)}
post	possibly_updated(this.transferFile)
post	new BufferedReader(socketOpened#2) num objects <= 1
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	new PrintWriter(socketOpened#1) num objects <= 1
post	new Socket(connect#1) num objects <= 1
post	new Thread(connect#2) num objects <= 1
unanalyzed	call on socketClosed
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.net.Socket:getOutputStream
unanalyzed	call on java.io.PrintWriter
unanalyzed	call on java.net.Socket:getInputStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on socketOpened
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 addLine
unanalyzed	call on setIcon
unanalyzed	call on java.util.List:remove
unanalyzed	call on java.io.DataOutputStream:close
unanalyzed	call on java.io.DataInputStream:close
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.DataInputStream
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.DataOutputStream
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.String:format
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on javax.swing.JLabel:setText
unanalyzed	call on java.lang.System:currentTimeMillis
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.listen: {0}, {1}

method	void listen()
pre	this.serverSocketSem != null
pre	(soft) init'ed(this.address)
pre	(soft) init'ed(this.port)
post	this.address == One-of{old this.address, 0}
post	init'ed(this.address)
post	possibly_updated(this.fileOut)
post	this.handler.timeStarted == old this.handler. timeStarted
post	possibly_updated(this.in)
post	this.listen == 1
post	new ServerSocket(listen#1) num objects == 1
post	this.myThread == One-of{old this.myThread, &new Thread(connect#2)}
post	possibly_updated(this.out)
post	init'ed(this.port)
post	this.serverSocket == &new ServerSocket(listen#1 )
post	this.socket == old this.socket
post	possibly_updated(this.transferFile)
post	new BufferedReader(socketOpened#2) num objects == 0
post	new DataInputStream(socketOpened#5) num objects == 0
post	new DataOutputStream(socketOpened#2) num objects == 0
post	new DataOutputStream(socketOpened#4) num objects == 0
post	new File(socketOpened#1) num objects == 0
post	new PrintWriter(socketOpened#1) num objects == 0
post	new Socket(connect#1) num objects == 0
post	new Thread(connect#2) num objects <= 1
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on socketClosed
unanalyzed	call on java.net.Socket:getOutputStream
unanalyzed	call on java.io.PrintWriter
unanalyzed	call on java.net.Socket:getInputStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on socketOpened
unanalyzed	call on java.net.ServerSocket:getLocalPort
unanalyzed	call on java.net.Socket
unanalyzed	call on java.lang.Thread
unanalyzed	call on java.lang.Thread:start
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 addLine
unanalyzed	call on setIcon
unanalyzed	call on java.util.List:remove
unanalyzed	call on java.io.DataOutputStream:close
unanalyzed	call on java.io.DataInputStream:close
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.DataInputStream
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.DataOutputStream
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.String:format
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on javax.swing.JLabel:setText
unanalyzed	call on java.lang.System:currentTimeMillis
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

method	void listen(int, int)
pre	(soft) endPort <= 2³²-2
pre	(soft) init'ed(this.address)
pre	(soft) init'ed(this.port)
pre	(soft) this.serverSocket != null
pre	(soft) startPort <= 2³²-2
pre	(soft) this.serverSocketSem != null
post	this.address == One-of{old this.address, 0}
post	init'ed(this.address)
post	possibly_updated(this.fileOut)
post	this.handler.timeStarted == old this.handler. timeStarted
post	possibly_updated(this.in)
post	this.listen == 1
post	this.myThread == One-of{old this.myThread, &new Thread(connect#2)}
post	possibly_updated(this.out)
post	init'ed(this.port)
post	this.serverSocket == One-of{old this.serverSocket, &new ServerSocket(listen#1)}
post	this.serverSocket != null
post	this.socket == old this.socket
post	possibly_updated(this.transferFile)
post	new BufferedReader(socketOpened#2) num objects == 0
post	new DataInputStream(socketOpened#5) num objects == 0
post	new DataOutputStream(socketOpened#2) num objects == 0
post	new DataOutputStream(socketOpened#4) num objects == 0
post	new File(socketOpened#1) num objects == 0
post	new PrintWriter(socketOpened#1) num objects == 0
post	new ServerSocket(listen#1) num objects <= 1
post	new Socket(connect#1) num objects == 0
post	new Thread(connect#2) num objects <= 1
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on socketClosed
unanalyzed	call on java.net.Socket:getOutputStream
unanalyzed	call on java.io.PrintWriter
unanalyzed	call on java.net.Socket:getInputStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on socketOpened
unanalyzed	call on java.net.ServerSocket:getLocalPort
unanalyzed	call on java.net.Socket
unanalyzed	call on java.lang.Thread
unanalyzed	call on java.lang.Thread:start
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 addLine
unanalyzed	call on setIcon
unanalyzed	call on java.util.List:remove
unanalyzed	call on java.io.DataOutputStream:close
unanalyzed	call on java.io.DataInputStream:close
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.DataInputStream
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.DataOutputStream
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.String:format
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on javax.swing.JLabel:setText
unanalyzed	call on java.lang.System:currentTimeMillis
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

method	void run()
pre	init'ed(this.running)
pre	(soft) init'ed(this.serverSocket)
pre	(soft) init'ed(this.socket)
pre	(soft) init'ed(this.myThread)
pre	(soft) this.serverListeningSem != null
pre	(soft) this.serverSocketSem != null
presumption	this.serverSocket@177 != null
post	possibly_updated(this.fileOut)
post	possibly_updated(this.handler.timeStarted)
post	possibly_updated(this.handler.transferCount)
post	possibly_updated(this.in)
post	possibly_updated(this.out)
post	possibly_updated(this.readSize)
post	init'ed(this.running)
post	init'ed(this.serverSocket)
post	init'ed(this.socket)
post	possibly_updated(this.transferFile)
post	init'ed(new BufferedReader(socketOpened#2) num objects)
post	init'ed(new DataInputStream(socketOpened#5) num objects)
post	init'ed(new DataOutputStream(socketOpened#2) num objects)
post	init'ed(new DataOutputStream(socketOpened#4) num objects)
post	init'ed(new File(socketOpened#1) num objects)
post	init'ed(new PrintWriter(socketOpened#1) num objects)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
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 socketClosed
unanalyzed	call on java.io.BufferedReader:readLine
unanalyzed	call on handleChatMessage
unanalyzed	call on java.net.Socket:getOutputStream
unanalyzed	call on java.io.PrintWriter
unanalyzed	call on java.net.Socket:getInputStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on socketOpened
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 addLine
unanalyzed	call on setIcon
unanalyzed	call on java.util.List:remove
unanalyzed	call on java.io.DataOutputStream:close
unanalyzed	call on java.io.DataInputStream:close
unanalyzed	call on com.dmdirc.ui.interfaces.InputWindow:getTra nscoder
unanalyzed	call on com.dmdirc.util.StringTranscoder:encode
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 handleReceive
unanalyzed	call on java.io.DataOutputStream:writeInt
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.DataInputStream
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.DataOutputStream
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.String:format
unanalyzed	call on javax.swing.JButton:setText
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 isWindowClosing
unanalyzed	call on java.lang.Integer:valueOf
test_vector	this.running: {0}, {1}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into ioe

Prev Msg Next Msg

method	void close()
pre	this.serverSocketSem != null
pre	(soft) init'ed(this.serverSocket)
pre	(soft) init'ed(this.socket)
pre	(soft) this.serverListeningSem != null
post	possibly_updated(this.in)
post	possibly_updated(this.out)
post	this.serverSocket == null
post	this.socket == null
unanalyzed	call on socketClosed
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 addLine
unanalyzed	call on setIcon
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 java.lang.Long:valueOf
unanalyzed	call on java.lang.String:format
unanalyzed	call on javax.swing.JButton:setText
unanalyzed	call on javax.swing.JLabel:setText
unanalyzed	call on java.lang.System:currentTimeMillis
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	java.net.ServerSocket:isClosed(...)@212: {1}, {0}
test_vector	java.net.Socket:isClosed(...)@227: {1}, {0}
test_vector	java.util.concurrent.Semaphore:tryAcquire(... )@202: {1}, {0}

method

void socketOpened()

method

void socketClosed()

method	bool isWriteable()
post	return_value == 0

method	void setAddress(long, int)
post	this.address == address
post	init'ed(this.address)
post	this.port == port
post	init'ed(this.port)

method	bool isListenSocket()
pre	init'ed(this.listen)
post	return_value == this.listen
post	init'ed(return_value)

method	String getHost()
pre	init'ed(this.address)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuilder:toStri ng(...)

method	int getPort()
pre	init'ed(this.port)
post	return_value == this.port
post	init'ed(return_value)

method	long ipToLong(String)
pre	ip != null
post	return_value == 0

Prev Msg Next Msg

use of default init

click for all messages in this file Low Prob.

check if init'ed(bits.length)

test always goes same way

Low Prob.

Test predetermined because bits.length == 0

Prev Msg Next Msg

Prev Msg Next Msg

dead code

click for all messages in this file Low Prob.

Dead code here because bits.length == 0

Prev Msg Next Msg

method	String longToIP(long)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuilder:toStri ng(...)