MyInfo.java

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


Filter Options
Annotation Kind:
pre
presumption
post
unanalyzed
test_vector


  • void com.dmdirc.parser.irc.MyInfo()

    • Kind Annotation Text
    postjava.lang.StringBuilder:toString(...)._tainted == 0
    postthis.altNickname in Addr_Set{&java.lang. StringBuilder:toString(...),&"IRC-Parser"}
    postthis.nickname != null
    postthis.prependChar == 95
    postthis.realname in Addr_Set{&java.lang. StringBuilder:toString(...),&"DMDIrc IRCParser"}
    postthis.username != null
    test_vectorjava.lang.String:isEmpty(...)@59: {0}, {1}

  • com.dmdirc.parser.irc.MyInfo__static_init

    • Kind Annotation Text

  • String getAltNickname()

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

  • String getNickname()

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

  • char getPrependChar()

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

  • String getRealname()

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

  • String getUsername()

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

  • void setAltNickname(String)

    • Kind Annotation Text
    postthis.altNickname == One-of{old this.altNickname, newValue}
    test_vectorjava.lang.String:isEmpty(...)@96: {1}, {0}
    test_vectornewValue: Addr_Set{null}, Inverse{null}

  • void setNickname(String)

    • Kind Annotation Text
    postthis.nickname == One-of{old this.nickname, newValue}
    test_vectorjava.lang.String:isEmpty(...)@78: {1}, {0}
    test_vectornewValue: Addr_Set{null}, Inverse{null}

  • void setPrependChar(char)

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

  • void setRealname(String)

    • Kind Annotation Text
    postthis.realname == One-of{old this.realname, newValue}
    test_vectorjava.lang.String:isEmpty(...)@114: {1}, {0}
    test_vectornewValue: Addr_Set{null}, Inverse{null}

  • void setUsername(String)

    • Kind Annotation Text
    postthis.username == One-of{old this.username, newValue}
    test_vectorjava.lang.String:isEmpty(...)@132: {1}, {0}
    test_vectornewValue: Addr_Set{null}, Inverse{null}