AliasPanel.java

AliasPanel.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void actionPerformed(ActionEvent)

Kind	Annotation Text
pre	this.argumentComponent != null
pre	this.argumentNumber != null
presumption	init'ed(com.dmdirc.actions.CoreActionComparison. INT_LESS)
presumption	javax.swing.JSpinner:getModel(...)@187 != null
presumption	javax.swing.JSpinner:getModel(...)@192 != null
presumption	javax.swing.JSpinner:getModel(...)@193 != null
presumption	javax.swing.JSpinner:getModel(...)@195 != null
presumption	javax.swing.SpinnerModel:getValue(...)@192 != null
test_vector	java.lang.Object:equals(...)@192: {0}, {1}
test_vector	javax.swing.JComboBox:getSelectedIndex(...)@188: {-2³¹..0}, {1..2³²-1}

void clear()

Kind	Annotation Text
pre	(soft) this.command.validator != null
pre	this.argumentComponent != null
pre	this.argumentNumber != null
pre	this.command != null
pre	this.command.errorIcon != null
pre	this.command.textField != null
pre	this.response != null
post	this.alias == null
unanalyzed	call on com.dmdirc.addons.ui_swing.components. validating.ValidatingJTextField:firePropertyChange
unanalyzed	call on com.dmdirc.config.prefs.validator. ValidationResponse:getFailureReason
unanalyzed	call on com.dmdirc.config.prefs.validator. ValidationResponse:isFailure
unanalyzed	call on com.dmdirc.config.prefs.validator. Validator:validate
unanalyzed	call on javax.swing.JLabel:isVisible
unanalyzed	call on javax.swing.JLabel:setToolTipText
unanalyzed	call on javax.swing.JLabel:setVisible
unanalyzed	call on javax.swing.JTextField:getText
unanalyzed	call on javax.swing.JTextField:isEnabled
unanalyzed	call on javax.swing.JTextField:setEnabled
unanalyzed	call on javax.swing.JTextField:setText

com.dmdirc.addons.ui_swing.dialogs.aliases.AliasPanel$1__static_init

Kind	Annotation Text
presumption	com.dmdirc.actions.CoreActionComparison.INT_EQUALS != null
presumption	com.dmdirc.actions.CoreActionComparison.INT_ GREATER != null
presumption	com.dmdirc.actions.CoreActionComparison.INT_LESS != null
presumption	com.dmdirc.actions.CoreActionComparison:ordinal(... )@220 < com.dmdirc.actions.CoreActionComparison:val ues(...).length@220
presumption	com.dmdirc.actions.CoreActionComparison:ordinal(... )@220 >= 0
presumption	com.dmdirc.actions.CoreActionComparison:values(... ).length@220 >= 1
presumption	com.dmdirc.actions.CoreActionComparison:values(... )@220 != null
post	new int[](AliasPanel$1__static_init#1) num objects == 1

void com.dmdirc.addons.ui_swing.dialogs.aliases.AliasPanel()

Kind	Annotation Text
presumption	init'ed(com.dmdirc.actions.CoreActionComparison. INT_EQUALS)
presumption	init'ed(com.dmdirc.actions.CoreActionComparison. INT_GREATER)
presumption	init'ed(com.dmdirc.actions.CoreActionComparison. INT_LESS)
presumption	init'ed(java.lang.Boolean.TRUE)
post	new JComboBox(AliasPanel#6) num objects == 1
post	new JLabel(ValidatingJTextField#1) num objects == 1
post	new JSpinner(AliasPanel#8) num objects == 1
post	new JTextArea(AliasPanel#10) num objects == 1
post	new JTextField(ValidatingJTextField#1) num objects == 1
post	new ValidatingJTextField(AliasPanel#1) num objects == 1
post	new ValidatorChain(AliasPanel#2) num objects == 1
post	this.alias == null
post	this.argumentComponent == &new JComboBox(AliasP anel#6)
post	this.argumentNumber == &new JSpinner(AliasPanel #8)
post	this.command == &new ValidatingJTextField(Alias Panel#1)
post	this.command.errorIcon == &new JLabel(Validatin gJTextField#1)
post	this.command.textField == &new JTextField(Valid atingJTextField#1)
post	this.command.validator == &new ValidatorChain(A liasPanel#2)
post	this.response == &new JTextArea(AliasPanel#10)
unanalyzed	call on com.dmdirc.addons.ui_swing.components. validating.ValidatingJTextField:add
unanalyzed	call on com.dmdirc.addons.ui_swing.components. validating.ValidatingJTextField:firePropertyChange
unanalyzed	call on com.dmdirc.addons.ui_swing.components. validating.ValidatingJTextField:setLayout
unanalyzed	call on com.dmdirc.addons.ui_swing.dialogs.aliases. AliasPanel:add
unanalyzed	call on com.dmdirc.addons.ui_swing.dialogs.aliases. AliasPanel:setLayout
unanalyzed	call on com.dmdirc.config.prefs.validator. ValidationResponse:getFailureReason
unanalyzed	call on com.dmdirc.config.prefs.validator. ValidationResponse:isFailure
unanalyzed	call on com.dmdirc.config.prefs.validator. Validator:validate
unanalyzed	call on com.dmdirc.ui.IconManager:getIcon
unanalyzed	call on com.dmdirc.ui.IconManager:getIconManager
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on javax.swing.DefaultListCellRenderer
unanalyzed	call on javax.swing.JComboBox:setEnabled
unanalyzed	call on javax.swing.JComboBox:setSelectedItem
unanalyzed	call on javax.swing.JComponent
unanalyzed	call on javax.swing.JLabel
unanalyzed	call on javax.swing.JLabel:isVisible
unanalyzed	call on javax.swing.JLabel:setToolTipText
unanalyzed	call on javax.swing.JLabel:setVisible
unanalyzed	call on javax.swing.JScrollPane
unanalyzed	call on javax.swing.JSpinner:setEnabled
unanalyzed	call on javax.swing.JSpinner:setValue
unanalyzed	call on javax.swing.JTextArea:setEnabled
unanalyzed	call on javax.swing.JTextArea:setText
unanalyzed	call on javax.swing.JTextField
unanalyzed	call on javax.swing.JTextField:getDocument
unanalyzed	call on javax.swing.JTextField:getText
unanalyzed	call on javax.swing.JTextField:isEnabled
unanalyzed	call on javax.swing.JTextField:setEnabled
unanalyzed	call on javax.swing.JTextField:setText
unanalyzed	call on javax.swing.text.Document:addDocumentListen er
unanalyzed	call on net.miginfocom.swing.MigLayout

com.dmdirc.addons.ui_swing.dialogs.aliases.AliasPanel__static_init

Kind	Annotation Text

void focusCommand()

Kind	Annotation Text
pre	this.command != null
pre	this.command.textField != null
unanalyzed	call on javax.swing.JTextField:requestFocusInWindow

Alias getAlias()

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

ActionCondition getArguments()

Kind	Annotation Text
pre	(soft) init'ed(com.dmdirc.addons.ui_swing.dialogs. aliases.AliasPanel$1__static_init.new int[](AliasPanel$1__static_init#1)[...])
pre	(soft) this.argumentNumber != null
pre	this.argumentComponent != null
presumption	com.dmdirc.actions.CoreActionComparison:ordinal(... )@220 < com.dmdirc.actions.CoreActionComparison:val ues(...).length
presumption	com.dmdirc.actions.CoreActionComparison:ordinal(... )@220 >= 0
presumption	com.dmdirc.actions.CoreActionComparison:values(... ).length >= 1
presumption	init'ed(com.dmdirc.actions.CoreActionComparison. INT_EQUALS)
presumption	init'ed(com.dmdirc.actions.CoreActionComparison. INT_GREATER)
presumption	init'ed(com.dmdirc.actions.CoreActionComparison. INT_LESS)
presumption	init'ed(com.dmdirc.actions.CoreActionComponent. STRINGARRAY_LENGTH)
presumption	javax.swing.JComboBox:getSelectedItem(...)@220 != null
presumption	javax.swing.JSpinner:getValue(...)@222 != null
presumption	javax.swing.JSpinner:getValue(...)@227 != null
presumption	javax.swing.JSpinner:getValue(...)@232 != null
post	new ActionCondition(getArguments#1) num objects <= 1
post	new ActionCondition(getArguments#2) num objects <= 1
post	new ActionCondition(getArguments#3) num objects <= 1
post	return_value in Addr_Set{null,&new ActionCondition(getArguments#1),&new ActionCondition(getArguments#2),&new ActionCondition(getArguments#3)}
test_vector	com.dmdirc.addons.ui_swing.dialogs.aliases. AliasPanel$1__static_init.new int[](AliasPanel$1__ static_init#1)[...]: {1}, {2}, {3}, {-2³¹..0, 4..2³²-1}
test_vector	javax.swing.JComboBox:getSelectedItem(...)@217: Inverse{null}, Addr_Set{null}

String getCommand()

Kind	Annotation Text
pre	this.command != null
pre	this.command.textField != null
post	init'ed(return_value)
unanalyzed	call on javax.swing.JTextField:getText

Alias getNewAlias()

Kind	Annotation Text
pre	(soft) init'ed(com.dmdirc.addons.ui_swing.dialogs. aliases.AliasPanel$1__static_init.new int[](AliasPanel$1__static_init#1)[...])
pre	(soft) this.argumentNumber != null
pre	this.argumentComponent != null
pre	this.command != null
pre	this.command.textField != null
pre	this.response != null
presumption	com.dmdirc.actions.CoreActionComparison:values(... ).length >= 1
presumption	init'ed(com.dmdirc.actions.CoreActionComparison. STRING_EQUALS)
presumption	init'ed(com.dmdirc.actions.CoreActionComponent. STRING_STRING)
post	new Alias(getNewAlias#3) num objects == 1
post	return_value == &new Alias(getNewAlias#3)
unanalyzed	call on com.dmdirc.actions.ActionCondition
unanalyzed	call on com.dmdirc.actions.CoreActionComparison:ord inal
unanalyzed	call on java.lang.Object:toString
unanalyzed	call on java.lang.String:split
unanalyzed	call on javax.swing.JComboBox:getSelectedItem
unanalyzed	call on javax.swing.JSpinner:getValue
unanalyzed	call on javax.swing.JTextArea:getText
unanalyzed	call on javax.swing.JTextField:getText

String[] getResponse()

Kind	Annotation Text
pre	this.response != null
presumption	javax.swing.JTextArea:getText(...)@247 != null
post	java.lang.String:split(...)._tainted == 0
post	return_value == &java.lang.String:split(...)

void layoutComponents()

Kind	Annotation Text

void setAlias(Alias)

Kind	Annotation Text
pre	(soft) this.argumentComponent != null
pre	(soft) this.argumentNumber != null
pre	(soft) this.command != null
pre	(soft) this.command.errorIcon != null
pre	(soft) this.command.textField != null
pre	(soft) this.command.validator != null
pre	(soft) this.response != null
presumption	arr$.length@169 <= 2³²-1
presumption	com.dmdirc.actions.wrappers.Alias:getArguments(... )@150 != null
presumption	com.dmdirc.actions.wrappers.Alias:getResponse(... )@169 != null
presumption	init'ed(com.dmdirc.actions.CoreActionComparison. STRING_EQUALS)
presumption	java.lang.StringBuffer:length(...)@174 >= -2³¹+1
presumption	java.util.List:get(...)@158 != null
presumption	java.util.List:get(...)@161 != null
post	init'ed(this.alias)
post	this.alias == One-of{null, alias}
unanalyzed	call on com.dmdirc.addons.ui_swing.components. validating.ValidatingJTextField:firePropertyChange
unanalyzed	call on com.dmdirc.config.prefs.validator. ValidationResponse:getFailureReason
unanalyzed	call on com.dmdirc.config.prefs.validator. ValidationResponse:isFailure
unanalyzed	call on com.dmdirc.config.prefs.validator. Validator:validate
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on javax.swing.JComboBox:setEnabled
unanalyzed	call on javax.swing.JComboBox:setSelectedItem
unanalyzed	call on javax.swing.JLabel:isVisible
unanalyzed	call on javax.swing.JLabel:setToolTipText
unanalyzed	call on javax.swing.JLabel:setVisible
unanalyzed	call on javax.swing.JSpinner:setEnabled
unanalyzed	call on javax.swing.JSpinner:setValue
unanalyzed	call on javax.swing.JTextArea:setEnabled
unanalyzed	call on javax.swing.JTextArea:setText
unanalyzed	call on javax.swing.JTextField:getText
unanalyzed	call on javax.swing.JTextField:isEnabled
unanalyzed	call on javax.swing.JTextField:setEnabled
unanalyzed	call on javax.swing.JTextField:setText
test_vector	alias: Inverse{null}, Addr_Set{null}
test_vector	java.lang.StringBuffer:length(...)@173: {-2³¹..1}, {2..2³²-1}
test_vector	java.util.List:size(...)@153: {-2³¹..0, 2..2³²-1}, {1}