PopupMenuItem.java

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


Filter Options
Annotation Kind:
pre
presumption
post
unanalyzed
test_vector


  • void com.dmdirc.commandparser.PopupMenuItem()

    • Kind Annotation Text
    postthis.divider == 1
    postthis.submenu == null

  • void com.dmdirc.commandparser.PopupMenuItem(String, PopupMenu)

    • Kind Annotation Text
    postinit'ed(this.name)
    postinit'ed(this.submenu)
    postthis.divider == 0
    postthis.name == name
    postthis.submenu == submenu

  • void com.dmdirc.commandparser.PopupMenuItem(String, String)

    • Kind Annotation Text
    postinit'ed(this.command)
    postinit'ed(this.name)
    postthis.command == command
    postthis.divider == 0
    postthis.name == name
    postthis.submenu == null

  • com.dmdirc.commandparser.PopupMenuItem__static_init

    • Kind Annotation Text

  • String getCommand(Object[])

    • Kind Annotation Text
    preinit'ed(com/dmdirc/commandparser/CommandManager. commandChar)
    preinit'ed(this.command)
    postjava.lang.StringBuilder:toString(...)._tainted == 0
    postreturn_value == &java.lang.StringBuilder:toStri ng(...)

  • String getName()

    • Kind Annotation Text
    preinit'ed(this.name)
    postinit'ed(return_value)
    postreturn_value == this.name

  • PopupMenu getSubMenu()

    • Kind Annotation Text
    preinit'ed(this.submenu)
    postinit'ed(return_value)
    postreturn_value == this.submenu

  • bool isDivider()

    • Kind Annotation Text
    preinit'ed(this.divider)
    postinit'ed(return_value)
    postreturn_value == this.divider

  • bool isSubMenu()

    • Kind Annotation Text
    preinit'ed(this.submenu)
    postinit'ed(return_value)