BashStyle.java


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


Filter Options
Annotation Kind:
pre
presumption
post
unanalyzed
test_vector


  • void com.dmdirc.addons.tabcompletion_bash.BashStyle(TabCompleter, InputWindow)

  • Kind Annotation Text
    postinit'ed(this.tabCompleter)
    postinit'ed(this.window)
    postthis.lastPosition == -1
    postthis.lastWord == &""
    postthis.tabCompleter == completer
    postthis.tabCount == 0
    postthis.window == window

  • com.dmdirc.addons.tabcompletion_bash.BashStyle__static_init

  • Kind Annotation Text

  • TabCompletionResult getResult(String, int, int, AdditionalTabTargets)

  • Kind Annotation Text
    pre(soft) init'ed(this.lastWord)
    pre(soft) this.tabCount <= 232-2
    pre(soft) this.window != null
    preinit'ed(this.lastPosition)
    preoriginal != null
    prethis.tabCompleter != null
    presumptioncom.dmdirc.ui.input.TabCompleter:complete(...)@67 != null
    presumptioncom.dmdirc.ui.input.TabCompleterResult:getBestSubst ring(...)@92 != null
    presumptioncom.dmdirc.ui.input.TabCompleterResult:getResults(. ..)@84 != null
    presumptionjava.awt.Toolkit:getDefaultToolkit(...)@78 != null
    presumptionjava.util.List:get(...)@84 != null
    presumptionstart + java.lang.String:length(...)@86 in {-231..232-1}
    presumptionstart + java.lang.String:length(...)@98 in {-231..232-1}
    postinit'ed(java.lang.String:substring(...)._tainted)
    postinit'ed(this.lastPosition)
    postinit'ed(this.lastWord)
    postjava.lang.String:substring(...)._tainted == original._tainted
    postnew TabCompletionResult(getResult#1) num objects <= 1
    postnew TabCompletionResult(getResult#4) num objects <= 1
    postreturn_value in Addr_Set{null,&amp;new TabCompletionResult(getResult#4),&amp;new TabCompletionResult(getResult#1)}
    postthis.lastPosition == One-of{old this.lastPosition, start}
    postthis.lastWord == One-of{old this.lastWord, &amp;java.lang.String:substring(...)}
    postthis.tabCount == One-of{old this.tabCount + 1, 1}
    postthis.tabCount >= -231+1
    test_vectorcom.dmdirc.ui.input.TabCompleterResult:getResultCou nt(...)@77: {-231..-1, 1..232-1}, {0}
    test_vectorcom.dmdirc.ui.input.TabCompleterResult:getResultCou nt(...)@81: {-231..0, 2..232-1}, {1}
    test_vectorjava.lang.String:equals(...)@69: {0}, {1}
    test_vectorjava.lang.String:equalsIgnoreCase(...)@93: {0}, {1}
    test_vectorthis.lastPosition - start: {-6_442_450_943..-1, 1..6_442_450_943}, {0}