| Kind |
Annotation Text |
| pre | (soft) init'ed(this.lastWord) |
| pre | (soft) this.tabCount <= 232-2 |
| pre | (soft) this.window != null |
| pre | init'ed(this.lastPosition) |
| pre | original != null |
| pre | this.tabCompleter != null |
| presumption | com.dmdirc.ui.input.TabCompleter:complete(...)@67 != null |
| presumption | com.dmdirc.ui.input.TabCompleterResult:getBestSubst ring(...)@92 != null |
| presumption | com.dmdirc.ui.input.TabCompleterResult:getResults(. ..)@84 != null |
| presumption | java.awt.Toolkit:getDefaultToolkit(...)@78 != null |
| presumption | java.util.List:get(...)@84 != null |
| presumption | start + java.lang.String:length(...)@86 in {-231..232-1} |
| presumption | start + java.lang.String:length(...)@98 in {-231..232-1} |
| post | init'ed(java.lang.String:substring(...)._tainted) |
| post | init'ed(this.lastPosition) |
| post | init'ed(this.lastWord) |
| post | java.lang.String:substring(...)._tainted == original._tainted |
| post | new TabCompletionResult(getResult#1) num objects <= 1 |
| post | new TabCompletionResult(getResult#4) num objects <= 1 |
| post | return_value in Addr_Set{null,&new TabCompletionResult(getResult#4),&new TabCompletionResult(getResult#1)} |
| post | this.lastPosition == One-of{old this.lastPosition, start} |
| post | this.lastWord == One-of{old this.lastWord, &java.lang.String:substring(...)} |
| post | this.tabCount == One-of{old this.tabCount + 1, 1} |
| post | this.tabCount >= -231+1 |
| test_vector | com.dmdirc.ui.input.TabCompleterResult:getResultCou nt(...)@77: {-231..-1, 1..232-1}, {0} |
| test_vector | com.dmdirc.ui.input.TabCompleterResult:getResultCou nt(...)@81: {-231..0, 2..232-1}, {1} |
| test_vector | java.lang.String:equals(...)@69: {0}, {1} |
| test_vector | java.lang.String:equalsIgnoreCase(...)@93: {0}, {1} |
| test_vector | this.lastPosition - start: {-6_442_450_943..-1, 1..6_442_450_943}, {0} |