Messages

Last Msg First Msg

method

com.dmdirc.addons.ui_swing.components. reorderablelist.ArrayListTransferHandler__static_in it

method	void com.dmdirc.addons.ui_swing.components. reorderablelist.ArrayListTransferHandler()
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
post	this.addIndex == -1
post	init'ed(this.localArrayListFlavor)
post	this.serialArrayListFlavor == &new DataFlavor(ArrayListTransferHandler#3)
post	new DataFlavor(ArrayListTransferHandler#1) num objects <= 1
post	new DataFlavor(ArrayListTransferHandler#3) num objects == 1

method not available - call not analyzed Info call on void com.dmdirc.logger.Logger:userError(Err orLevel, String)

method	bool importData(JComponent, Transferable)
pre	t != null
pre	(soft) comp != null
pre	(soft) init'ed(this.indices)
pre	(soft) this.indices.length in {1..2³²}
pre	(soft) init'ed(this.indices[0])
pre	(soft) init'ed(this.indices[...])
pre	(soft) init'ed(this.localArrayListFlavor)
pre	(soft) this.sourceList != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	java.awt.datatransfer.Transferable:getTransferData( ...)@86 != null
presumption	java.awt.datatransfer.Transferable:getTransferData( ...)@88 != null
presumption	java.awt.datatransfer.Transferable:getTransferDataF lavors(...).length@80 <= 2³²-1
presumption	java.awt.datatransfer.Transferable:getTransferDataF lavors(...).length@85 <= 2³²-1
presumption	java.awt.datatransfer.Transferable:getTransferDataF lavors(...).length@87 <= 2³²-1
presumption	java.awt.datatransfer.Transferable:getTransferDataF lavors(...)@80 != null
presumption	java.awt.datatransfer.Transferable:getTransferDataF lavors(...)@85 != null
presumption	java.awt.datatransfer.Transferable:getTransferDataF lavors(...)@87 != null
presumption	java.awt.datatransfer.Transferable:getTransferDataF lavors(...)[...]@80 != null
presumption	java.awt.datatransfer.Transferable:getTransferDataF lavors(...)[...]@85 != null
presumption	java.awt.datatransfer.Transferable:getTransferDataF lavors(...)[...]@87 != null
post	init'ed(return_value)
post	possibly_updated(this.addCount)
post	possibly_updated(this.addIndex)
post	this.indices == One-of{old this.indices, null}
post	init'ed(this.indices)
unanalyzed	call on java.awt.datatransfer.DataFlavor:equals
unanalyzed	call on javax.swing.JList:instanceof
unanalyzed	call on javax.swing.JList:getModel
unanalyzed	call on javax.swing.DefaultListModel:instanceof
unanalyzed	call on javax.swing.JList:getSelectedIndex
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on javax.swing.DefaultListModel:getSize
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on javax.swing.DefaultListModel:add

method not available - call not analyzed Info call on void com.dmdirc.logger.Logger:userError(Err orLevel, String)

method	bool doImport(JList, List)
pre	target != null
pre	this.sourceList != null
pre	(soft) init'ed(this.indices)
pre	(soft) this.indices.length in {1..2³²}
pre	(soft) init'ed(this.indices[0])
pre	(soft) init'ed(this.indices[...])
pre	(soft) transferList != null
presumption	java.util.List:size(...)@131 + index in {-2³²..2³²-1}
presumption	javax.swing.DefaultListModel:getSize(...)@117 <= 2³²-2
presumption	javax.swing.JList:getModel(...)@116 != null
presumption	javax.swing.JList:getSelectedIndex(...)@110 <= 2³²-3
post	return_value == 1
post	possibly_updated(this.addCount)
post	possibly_updated(this.addIndex)
post	this.indices == One-of{null, old this.indices}
post	init'ed(this.indices)
test_vector	this.indices: Addr_Set{null}, Inverse{null}
test_vector	java.lang.Object:equals(...)@111: {0}, {1}
test_vector	javax.swing.JList:getSelectedIndex(...)@110: {0..2³²-3}, {-2³¹..-1}

method	void exportDone(JComponent, Transferable, int)
pre	(soft) init'ed(this.addCount)
pre	(soft) this.addIndex != 2³²-2
pre	(soft) init'ed(this.indices)
pre	(soft) this.indices[...] in {-2³¹+1..2³²-2}
pre	(soft) this.indices.length <= 2³²-1
pre	(soft) this.sourceList != null
presumption	javax.swing.JList:getModel(...)@143 != null
post	this.addCount == 0
post	this.addIndex == -1
post	this.indices == null
post	init'ed(this.indices[...])
test_vector	action: {-2³¹..1, 3..2³²-1}, {2}
test_vector	this.addCount: {-2³¹..0}, {1..2³²-1}
test_vector	this.indices: Addr_Set{null}, Inverse{null}

method	bool hasLocalArrayListFlavor(DataFlavor[])
pre	init'ed(this.localArrayListFlavor)
pre	(soft) transferFlavors != null
pre	(soft) transferFlavors.length <= 2³²-1
pre	(soft) transferFlavors[...] != null
post	init'ed(return_value)
test_vector	this.localArrayListFlavor: Inverse{null}, Addr_Set{null}
test_vector	java.awt.datatransfer.DataFlavor:equals(...)@175: {0}, {1}

method	bool hasSerialArrayListFlavor(DataFlavor[])
pre	(soft) transferFlavors != null
pre	(soft) transferFlavors.length <= 2³²-1
pre	(soft) transferFlavors[...] != null
post	init'ed(return_value)
test_vector	this.serialArrayListFlavor: Inverse{null}, Addr_Set{null}
test_vector	java.awt.datatransfer.DataFlavor:equals(...)@196: {0}, {1}

method	bool canImport(JComponent, DataFlavor[])
pre	(soft) init'ed(this.localArrayListFlavor)
pre	(soft) transferFlavors != null
pre	(soft) transferFlavors.length <= 2³²-1
pre	(soft) transferFlavors[...] != null
post	init'ed(return_value)
unanalyzed	call on java.awt.datatransfer.DataFlavor:equals

method	Transferable createTransferable(JComponent)
presumption	values.length@228 <= 2³²-1
presumption	values[i]@228 != null
post	return_value in Addr_Set{null,&new ArrayListTransferable(createTransferable#2)}
post	possibly_updated(this.indices)
post	this.sourceList == One-of{c, old this.sourceList}
post	new ArrayList(createTransferable#1) num objects <= 1
post	new ArrayListTransferable(createTransferable#2) num objects <= 1
post	new ArrayListTransferable(createTransferable#2). data == &new ArrayList(createTransferable#1)
post	new ArrayListTransferable(createTransferable#2). localArrayListFlavor in Addr_Set{null,&new DataFlavor(ArrayListTransferable#1)}
post	new ArrayListTransferable(createTransferable#2). serialArrayListFlavor == &new DataFlavor(ArrayL istTransferable#3)
post	new DataFlavor(ArrayListTransferable#1) num objects <= 1
post	new DataFlavor(ArrayListTransferable#3) num objects <= 1
unanalyzed	call on java.awt.datatransfer.DataFlavor
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.ClassNotFoundException:getMessage
unanalyzed	call on com.dmdirc.logger.Logger:userError
test_vector	javax.swing.JList:getSelectedValues(...)@228: Addr_Set{null}, Inverse{null}
test_vector	values.length@228: {1..2³²-1}, {0}

Prev Msg Next Msg

test always goes same way

click for all messages in this file Low Prob.

Test predetermined because str != null

Prev Msg Next Msg

Prev Msg Next Msg

dead code

click for all messages in this file Low Prob.

Dead code here because str != null

Prev Msg Next Msg

method	int getSourceActions(JComponent)
post	return_value == 3