| method | void com.dmdirc.addons.ui_swing.dialogs.updater. UpdateTableModel() |
| presumption | java.text.NumberFormat:getNumberInstance(...)@70 != null |
| post | this.enabled == &new HashMap(setUpdates#2) |
| post | this.formatter != null |
| post | this.updates == &new ArrayList(setUpdates#1) |
| post | new ArrayList(setUpdates#1) num objects == 1 |
| post | new HashMap(setUpdates#2) num objects == 1 |
| unanalyzed | call on java.util.Map:put |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on com.dmdirc.updater.Update:addUpdateListener |
| unanalyzed | call on java.util.HashMap |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on java.lang.Boolean:valueOf |
| unanalyzed | call on com.dmdirc.addons.ui_swing.dialogs.updater. UpdateTableModel:fireTableDataChanged |
| unanalyzed | call on javax.swing.table.AbstractTableModel |
| unanalyzed | call on java.text.NumberFormat:getNumberInstance |
| unanalyzed | call on java.text.NumberFormat:setMaximumFractionDi gits |
| unanalyzed | call on java.text.NumberFormat:setMinimumFractionDi gits |
| method | void com.dmdirc.addons.ui_swing.dialogs.updater. UpdateTableModel(List) |
| pre | updates != null |
| presumption | java.text.NumberFormat:getNumberInstance(...)@70 != null |
| post | this.enabled == &new HashMap(setUpdates#2) |
| post | this.formatter != null |
| post | this.updates == &new ArrayList(setUpdates#1) |
| post | new ArrayList(setUpdates#1) num objects == 1 |
| post | new HashMap(setUpdates#2) num objects == 1 |
| unanalyzed | call on java.util.Map:put |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on com.dmdirc.updater.Update:addUpdateListener |
| unanalyzed | call on java.util.HashMap |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on java.lang.Boolean:valueOf |
| unanalyzed | call on com.dmdirc.addons.ui_swing.dialogs.updater. UpdateTableModel:fireTableDataChanged |
| method | Object getValueAt(int, int) |
| pre | columnIndex in {0..3} |
| pre | rowIndex in {0..232-2} |
| pre | this.updates != null |
| pre | (soft) this.enabled != null |
| pre | (soft) this.formatter != null |
| presumption | com.dmdirc.updater.Update:getStatus(...)@164 != null |
| presumption | init'ed(com.dmdirc.updater.UpdateStatus. DOWNLOADING) |
| presumption | java.util.List:get(...)@160 != null |
| presumption | java.util.List:get(...)@162 != null |
| presumption | java.util.List:get(...)@164 != null |
| presumption | java.util.List:get(...)@165 != null |
| presumption | java.util.List:get(...)@168 != null |
| presumption | java.util.List:size(...)@149 >= 1 |
| presumption | java.util.List:size(...)@149 - rowIndex in {1..232-1} |
| post | java.lang.StringBuilder:toString(...)._tainted == 0 |
| post | init'ed(return_value) |
| test_vector | columnIndex: {0}, {1}, {2}, {3} |
| test_vector | com.dmdirc.updater.UpdateStatus:equals(...)@164: {0}, {1} |