EtchedLineBorder.java

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


Filter Options
Annotation Kind:
pre
presumption
post
unanalyzed
test_vector


  • com.dmdirc.installer.ui.EtchedLineBorder$1__static_init

    • Kind Annotation Text
    pre(soft) init'ed(com.dmdirc.installer.ui. EtchedLineBorder$BorderSide__static_init.new EtchedLineBorder$BorderSide[](EtchedLineBorder$Bor derSide__static_init#3)[...])
    presumptioncom.dmdirc.installer.ui.EtchedLineBorder_ BorderSide:ordinal(...)@75 - values(...).length in range
    presumptioncom.dmdirc.installer.ui.EtchedLineBorder_ BorderSide:ordinal(...)@75 in {0,1}
    postnew int[](EtchedLineBorder$1__static_init#1) num objects == 1

  • void com.dmdirc.installer.ui.EtchedLineBorder$BorderSide(String, int)

    • Kind Annotation Text

  • com.dmdirc.installer.ui.EtchedLineBorder$BorderSide__static_init

    • Kind Annotation Text
    post$VALUES == &new EtchedLineBorder$BorderSide[](E tchedLineBorder$BorderSide__static_init#3)
    post$VALUES.length == 2
    post$VALUES[0] == &new EtchedLineBorder$BorderSide( EtchedLineBorder$BorderSide__static_init#1)
    post$VALUES[1] == &new EtchedLineBorder$BorderSide( EtchedLineBorder$BorderSide__static_init#2)
    postBOTTOM == &new EtchedLineBorder$BorderSide(Etch edLineBorder$BorderSide__static_init#2)
    postTOP == &new EtchedLineBorder$BorderSide(EtchedL ineBorder$BorderSide__static_init#1)
    postnew EtchedLineBorder$BorderSide(EtchedLineBorder$Bo rderSide__static_init#1) num objects == 1
    postnew EtchedLineBorder$BorderSide(EtchedLineBorder$Bo rderSide__static_init#2) num objects == 1
    postnew EtchedLineBorder$BorderSide[](EtchedLineBorder$ BorderSide__static_init#3) num objects == 1
    unanalyzedcall on java.lang.Enum

  • void com.dmdirc.installer.ui.EtchedLineBorder(int, EtchedLineBorder$BorderSide)

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

  • com.dmdirc.installer.ui.EtchedLineBorder__static_init

    • Kind Annotation Text

  • void paintBorder(Component, Graphics, int, int, int, int)

    • Kind Annotation Text
    pre(soft) height <= 232-6
    pre(soft) init'ed(com.dmdirc.installer.ui. EtchedLineBorder$1__static_init.new int[](EtchedLineBorder$1__static_init#1)[...])
    pre(soft) width <= 232-6
    preg != null
    preinit'ed(this.etchType)
    prethis.side != null
    prex <= 231
    prey <= 231
    presumptioncom.dmdirc.installer.ui.EtchedLineBorder_ BorderSide:ordinal(...)@75 in {0,1}
    presumptioncom.dmdirc.installer.ui.EtchedLineBorder_ BorderSide:ordinal(...)@88 in {0,1}
    test_vectorcom.dmdirc.installer.ui.EtchedLineBorder$1__static_ init.new int[](EtchedLineBorder$1__static_ init#1)[...]: {1}, {2}, {-231..0, 3..232-1}
    test_vectorthis.etchType: {-231..0, 2.. 232-1}, {1}

  • EtchedLineBorder$BorderSide valueOf(String)

    • Kind Annotation Text
    postinit'ed(return_value)

  • EtchedLineBorder$BorderSide[] values()

    • Kind Annotation Text
    pre(soft) init'ed($VALUES[...])
    postnew EtchedLineBorder$BorderSide[](values#1) num objects == 1
    postreturn_value == &amp;new EtchedLineBorder$BorderSid e[](values#1)
    postreturn_value.length == 2
    postreturn_value[...] == One-of{$VALUES[...], undefined}