ThemeIdentity.java


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


Filter Options
Annotation Kind:
pre
presumption
post
unanalyzed
test_vector


  • void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)

  • Kind Annotation Text
    presumptionthis.myTarget@59 != null
    postinit'ed(this.theme)
    postthis.myTarget != null
    postthis.theme == theme

  • com.dmdirc.ui.themes.ThemeIdentity__static_init

  • Kind Annotation Text

  • String getName()

  • Kind Annotation Text
    postjava.lang.StringBuilder:toString(...)._tainted == 0
    postreturn_value == &java.lang.StringBuilder:toStri ng(...)

  • String getOption(String, String)

  • Kind Annotation Text
    pre(soft) this.theme != null
    pre(soft) this.theme.file != null
    postinit'ed(return_value)
    unanalyzedcall on java.io.File:getName
    unanalyzedcall on java.lang.String:length
    unanalyzedcall on java.lang.String:substring
    test_vectorcom.dmdirc.config.Identity:getOption(...)@80: Inverse{null}, Addr_Set{null}

  • bool hasOption(String, String)

  • Kind Annotation Text
    predomain != null
    postinit'ed(return_value)
    test_vectorjava.lang.String:equalsIgnoreCase(...)@68: {0}, {1}
    test_vectorjava.lang.String:equalsIgnoreCase(...)@68: {1}, {0}