ListScroller.java

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


Filter Options
Annotation Kind:
pre
presumption
post
unanalyzed
test_vector


  • void changeFocus(bool)

    • Kind Annotation Text
    pre(soft) this.model != null
    prethis.selectionModel != null
    presumptionjavax.swing.ListSelectionModel:getMinSelectionIndex (...)@90 >= -231+1
    presumptionjavax.swing.ListSelectionModel:getMinSelectionIndex (...)@93 <= 232-2
    unanalyzedcall on javax.swing.ListModel:getSize
    test_vectordirection: {0}, {1}

  • int changeFocusDown(int)

    • Kind Annotation Text
    preindex <= 232-2
    prethis.model != null
    postreturn_value == One-of{0, index + 1}
    postreturn_value >= -231+1

  • int changeFocusUp(int)

    • Kind Annotation Text
    pre(soft) this.model != null
    preindex >= -231+1
    presumptionjavax.swing.ListModel:getSize(...)@109 >= -231+1
    postreturn_value <= 232-2
    test_vectorindex: {0}, {-231+1..-2, 1..232-1}, {-1}

  • void com.dmdirc.addons.ui_swing.components.ListScroller(JList)

    • Kind Annotation Text
    prelist != null
    postinit'ed(this.model)
    postinit'ed(this.selectionModel)

  • void com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)

    • Kind Annotation Text
    postinit'ed(this.model)
    postinit'ed(this.selectionModel)
    postthis.model == model
    postthis.selectionModel == selectionModel

  • com.dmdirc.addons.ui_swing.components.ListScroller__static_init

    • Kind Annotation Text

  • void mouseWheelMoved(MouseWheelEvent)

    • Kind Annotation Text
    pre(soft) this.model != null
    pree != null
    prethis.selectionModel != null
    unanalyzedcall on javax.swing.ListModel:getSize
    unanalyzedcall on javax.swing.ListSelectionModel:getMinSelect ionIndex
    unanalyzedcall on javax.swing.ListSelectionModel:setSelection Interval
    test_vectorjava.awt.event.MouseWheelEvent:getWheelRotation(... )@72: {0..232-1}, {-231..-1}