//# 3 errors, 265 messages
//#
/*
    //#IRCDocumentSearcher.java:1:1: class: com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher
    //#IRCDocumentSearcher.java:1:1: method: com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init
 * Copyright (c) 2006-2009 Chris Smith, Shane Mc Cormack, Gregory Holmes
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 * SOFTWARE.
 */

package com.dmdirc.addons.ui_swing.textpane;

import java.util.ArrayList;
import java.util.List;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

/**
 * Searches the textpane for specified phrases.
 */
public class IRCDocumentSearcher {

    /** Document to search. */
    private final IRCDocument document;

    /** Phrase to search for. */
    private final String phrase;
    
    /** Textpane position. */
    private LinePosition position;
    
    /** Case sensitive? */
    private final boolean caseSensitive;

    /**
     * Constructs a new IRC Document searcher.
     * 
     * @param phrase Phrase to search for
     * @param document Document to search
     * @param caseSensitive Whether or not this searcher is case sensitive
     */
    public IRCDocumentSearcher(final String phrase, final IRCDocument document,
            final boolean caseSensitive) {
    //#IRCDocumentSearcher.java:55: method: void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)
    //#input(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): caseSensitive
    //#input(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): com/dmdirc/addons/ui_swing/textpane/Line.__Descendant_Table[com/dmdirc/addons/ui_swing/textpane/Line]
    //#input(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): com/dmdirc/addons/ui_swing/textpane/Line.__Descendant_Table[others]
    //#input(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): com/dmdirc/addons/ui_swing/textpane/Line.__Dispatch_Table.getLength()I
    //#input(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): document
    //#input(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): document.lines
    //#input(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): phrase
    //#input(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): this
    //#output(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1) num objects
    //#output(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1).__Tag
    //#output(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1).endLine
    //#output(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1).endPos
    //#output(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1).startLine
    //#output(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1).startPos
    //#output(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): this.caseSensitive
    //#output(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): this.document
    //#output(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): this.phrase
    //#output(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): this.position
    //#new obj(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1)
    //#pre[2] (void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): document != null
    //#pre[3] (void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): document.lines != null
    //#presumption(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): java.util.List:size(...)@78 in {-2_147_483_647..4_294_967_295}
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): this.caseSensitive == caseSensitive
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): init'ed(this.caseSensitive)
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): this.document == document
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): this.document != null
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): this.phrase == phrase
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): init'ed(this.phrase)
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): this.position == &new LinePosition(getEndPosition#1)
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1) num objects == 1
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1).__Tag == com/dmdirc/addons/ui_swing/textpane/LinePosition
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1).endLine <= 4_294_967_294
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1).startLine == new LinePosition(getEndPosition#1).endLine
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): init'ed(new LinePosition(getEndPosition#1).endPos)
    //#post(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): new LinePosition(getEndPosition#1).startPos == new LinePosition(getEndPosition#1).endPos
    //#unanalyzed(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): Effects-of-calling:java.util.List:size
    //#unanalyzed(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): Effects-of-calling:java.util.List:get
    //#unanalyzed(void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)): Effects-of-calling:java.lang.String:length
        this.phrase = phrase;
        this.document = document;
        this.position = getEndPosition();
        this.caseSensitive = caseSensitive;
    }
    //#IRCDocumentSearcher.java:60: end of method: void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher(String, IRCDocument, bool)

    /**
     * Returns the end position in the document.
     * 
     * @return End position
     */
    private LinePosition getEndPosition() {
        final int documentSize = document.getNumLines() - 1;
    //#IRCDocumentSearcher.java:68: method: LinePosition com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.getEndPosition()
    //#input(LinePosition getEndPosition()): com/dmdirc/addons/ui_swing/textpane/Line.__Descendant_Table[com/dmdirc/addons/ui_swing/textpane/Line]
    //#input(LinePosition getEndPosition()): com/dmdirc/addons/ui_swing/textpane/Line.__Descendant_Table[others]
    //#input(LinePosition getEndPosition()): com/dmdirc/addons/ui_swing/textpane/Line.__Dispatch_Table.getLength()I
    //#input(LinePosition getEndPosition()): this
    //#input(LinePosition getEndPosition()): this.document
    //#input(LinePosition getEndPosition()): this.document.lines
    //#output(LinePosition getEndPosition()): new LinePosition(getEndPosition#1) num objects
    //#output(LinePosition getEndPosition()): return_value.__Tag
    //#output(LinePosition getEndPosition()): return_value.endLine
    //#output(LinePosition getEndPosition()): return_value.endPos
    //#output(LinePosition getEndPosition()): return_value.startLine
    //#output(LinePosition getEndPosition()): return_value.startPos
    //#output(LinePosition getEndPosition()): return_value
    //#new obj(LinePosition getEndPosition()): new LinePosition(getEndPosition#1)
    //#pre[2] (LinePosition getEndPosition()): this.document != null
    //#pre[3] (LinePosition getEndPosition()): this.document.lines != null
    //#presumption(LinePosition getEndPosition()): getLine(...).lineParts != null
    //#presumption(LinePosition getEndPosition()): getLine(...).lineParts.length <= 4_294_967_295
    //#presumption(LinePosition getEndPosition()): getLine(...).lineParts[0..4_294_967_295] != null
    //#presumption(LinePosition getEndPosition()): java.util.List:get(...)@89 != null
    //#presumption(LinePosition getEndPosition()): java.util.List:get(...)@89.__Tag == com/dmdirc/addons/ui_swing/textpane/Line
    //#presumption(LinePosition getEndPosition()): java.util.List:size(...)@78 >= -2_147_483_647
    //#presumption(LinePosition getEndPosition()): java.util.List:size(...)@78 in {-2_147_483_647..4_294_967_295}
    //#post(LinePosition getEndPosition()): return_value == &new LinePosition(getEndPosition#1)
    //#post(LinePosition getEndPosition()): new LinePosition(getEndPosition#1) num objects == 1
    //#post(LinePosition getEndPosition()): return_value.__Tag == com/dmdirc/addons/ui_swing/textpane/LinePosition
    //#post(LinePosition getEndPosition()): return_value.endLine <= 4_294_967_294
    //#post(LinePosition getEndPosition()): return_value.startLine == return_value.endLine
    //#post(LinePosition getEndPosition()): init'ed(return_value.endPos)
    //#post(LinePosition getEndPosition()): return_value.startPos == return_value.endPos
    //#unanalyzed(LinePosition getEndPosition()): Effects-of-calling:java.util.List:size
    //#unanalyzed(LinePosition getEndPosition()): Effects-of-calling:java.util.List:get
    //#unanalyzed(LinePosition getEndPosition()): Effects-of-calling:java.lang.String:length
    //#test_vector(LinePosition getEndPosition()): java.util.List:size(...)@78: {-2_147_483_647..0}, {1..4_294_967_295}
        final int lineLength;
        if (documentSize >= 0) {
            lineLength = document.getLine(documentSize).getLength();
        } else {
            lineLength = 0;
        }

        return new LinePosition(documentSize, lineLength, documentSize,
    //#IRCDocumentSearcher.java:76: end of method: LinePosition com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.getEndPosition()
                lineLength);
    }
    
    /**
     * Sets the position of the current match
     * 
     * @param position New match position
     */
    public void setPosition(final LinePosition position) {
        this.position = position;
    //#IRCDocumentSearcher.java:86: method: void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.setPosition(LinePosition)
    //#input(void setPosition(LinePosition)): position
    //#input(void setPosition(LinePosition)): this
    //#output(void setPosition(LinePosition)): this.position
    //#post(void setPosition(LinePosition)): this.position == position
    //#post(void setPosition(LinePosition)): init'ed(this.position)
    }
    //#IRCDocumentSearcher.java:87: end of method: void com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.setPosition(LinePosition)

    /**
     * Searches up in the document.
     * 
     * @return Line position of the next match
     */
    public LinePosition searchUp() {
        if (position == null) {
    //#IRCDocumentSearcher.java:95: method: LinePosition com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.searchUp()
    //#input(LinePosition searchUp()): ""._tainted
    //#input(LinePosition searchUp()): "(?i)"._tainted
    //#input(LinePosition searchUp()): "\E"._tainted
    //#input(LinePosition searchUp()): "\Q"._tainted
    //#input(LinePosition searchUp()): com/dmdirc/addons/ui_swing/textpane/Line.__Descendant_Table[com/dmdirc/addons/ui_swing/textpane/Line]
    //#input(LinePosition searchUp()): com/dmdirc/addons/ui_swing/textpane/Line.__Descendant_Table[others]
    //#input(LinePosition searchUp()): com/dmdirc/addons/ui_swing/textpane/Line.__Dispatch_Table.getLength()I
    //#input(LinePosition searchUp()): com/dmdirc/addons/ui_swing/textpane/Line.__Dispatch_Table.getText()Ljava/lang/String;
    //#input(LinePosition searchUp()): com/dmdirc/addons/ui_swing/textpane/LinePosition.__Descendant_Table[com/dmdirc/addons/ui_swing/textpane/LinePosition]
    //#input(LinePosition searchUp()): com/dmdirc/addons/ui_swing/textpane/LinePosition.__Descendant_Table[others]
    //#input(LinePosition searchUp()): com/dmdirc/addons/ui_swing/textpane/LinePosition.__Dispatch_Table.getEndLine()I
    //#input(LinePosition searchUp()): com/dmdirc/addons/ui_swing/textpane/LinePosition.__Dispatch_Table.getEndPos()I
    //#input(LinePosition searchUp()): this
    //#input(LinePosition searchUp()): this.caseSensitive
    //#input(LinePosition searchUp()): this.document
    //#input(LinePosition searchUp()): this.document.lines
    //#input(LinePosition searchUp()): this.phrase
    //#input(LinePosition searchUp()): this.phrase._tainted
    //#input(LinePosition searchUp()): this.position
    //#input(LinePosition searchUp()): this.position.__Tag
    //#input(LinePosition searchUp()): this.position.endLine
    //#input(LinePosition searchUp()): this.position.endPos
    //#output(LinePosition searchUp()): new LinePosition(getEndPosition#1) num objects
    //#output(LinePosition searchUp()): new LinePosition(getEndPosition#1).__Tag
    //#output(LinePosition searchUp()): new LinePosition(getEndPosition#1).endLine
    //#output(LinePosition searchUp()): new LinePosition(getEndPosition#1).endPos
    //#output(LinePosition searchUp()): new LinePosition(getEndPosition#1).startLine
    //#output(LinePosition searchUp()): new LinePosition(getEndPosition#1).startPos
    //#output(LinePosition searchUp()): return_value
    //#output(LinePosition searchUp()): this.position
    //#new obj(LinePosition searchUp()): new LinePosition(getEndPosition#1)
    //#pre[1] (LinePosition searchUp()): init'ed(this.position)
    //#pre[4] (LinePosition searchUp()): this.document != null
    //#pre[5] (LinePosition searchUp()): this.document.lines != null
    //#pre[8] (LinePosition searchUp()): (soft) this.position.__Tag == com/dmdirc/addons/ui_swing/textpane/LinePosition
    //#pre[9] (LinePosition searchUp()): (soft) init'ed(this.position.endLine)
    //#pre[10] (LinePosition searchUp()): (soft) init'ed(this.position.endPos)
    //#presumption(LinePosition searchUp()): getEndPosition(...)@96 init'ed
    //#presumption(LinePosition searchUp()): getLine(...).lineParts.length <= 4_294_967_295
    //#presumption(LinePosition searchUp()): java.util.List:get(...).__Tag@109 == com/dmdirc/addons/ui_swing/textpane/LinePosition
    //#presumption(LinePosition searchUp()): java.util.List:get(...).__Tag@111 == com/dmdirc/addons/ui_swing/textpane/LinePosition
    //#presumption(LinePosition searchUp()): java.util.List:get(...)@109 != null
    //#presumption(LinePosition searchUp()): java.util.List:get(...)@89 != null
    //#presumption(LinePosition searchUp()): java.util.List:get(...)@89.__Tag == com/dmdirc/addons/ui_swing/textpane/Line
    //#presumption(LinePosition searchUp()): java.util.List:size(...)@108 >= -2_147_483_647
    //#presumption(LinePosition searchUp()): java.util.List:size(...)@78 + line in {-2_147_483_647..8_589_934_590}
    //#post(LinePosition searchUp()): init'ed(return_value)
    //#post(LinePosition searchUp()): this.position == One-of{old this.position, &new LinePosition(getEndPosition#1)}
    //#post(LinePosition searchUp()): this.position != null
    //#post(LinePosition searchUp()): new LinePosition(getEndPosition#1) num objects <= 1
    //#post(LinePosition searchUp()): new LinePosition(getEndPosition#1).__Tag == com/dmdirc/addons/ui_swing/textpane/LinePosition
    //#post(LinePosition searchUp()): new LinePosition(getEndPosition#1).endLine <= 4_294_967_294
    //#post(LinePosition searchUp()): init'ed(new LinePosition(getEndPosition#1).endPos)
    //#post(LinePosition searchUp()): new LinePosition(getEndPosition#1).startLine <= 4_294_967_294
    //#post(LinePosition searchUp()): init'ed(new LinePosition(getEndPosition#1).startPos)
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.util.regex.Pattern:compile
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.util.regex.Pattern:matcher
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.util.regex.Matcher:find
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.util.regex.Matcher:start
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.util.regex.Matcher:end
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.util.List:add
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.util.List:size
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.util.List:get
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:com.dmdirc.ui.messages.Styliser:stipControlCodes
    //#unanalyzed(LinePosition searchUp()): Effects-of-calling:java.lang.String:length
    //#test_vector(LinePosition searchUp()): this.position: Inverse{null}, Addr_Set{null}
            position = getEndPosition();
        }
        
        int line = position.getEndLine();        
        for (int remaining = document.getNumLines(); remaining > 0; remaining--) {
            if (line < 0) {
                line = 0;
            }
              final String lineText = document.getLine(line).getText();
    //#IRCDocumentSearcher.java:104: ?!precondition failure
    //#    com/dmdirc/addons/ui_swing/textpane/Line.getText: this.lineParts != null
    //#    severity: HIGH
    //#    class: com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher
    //#    method: LinePosition searchUp()
    //#    basic block: bb_7
    //#    assertion: undefined != null
    //#    callee: String com/dmdirc/addons/ui_swing/textpane/Line.getText()
    //#    callee assertion: this.lineParts != null
    //#    callee file: Line.java
    //#    callee precondition index: [2]
    //#    callee srcpos: 103
    //#    VN: undefined
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null, Invalid}
    //#    Attribs:  Ptr  null in Bad
            
              final List<LinePosition> matches = searchLine(line, lineText);
            
             for (int i = matches.size() - 1; i >= 0; i--) {
                 if (position.getEndLine() != line
                         || matches.get(i).getEndPos() < position.getEndPos()) {
                     return matches.get(i);
                 }
             }
            
             line--;
            
             if (line < 0) {
                 line += document.getNumLines();
              }
            
        }

        return null;
    //#IRCDocumentSearcher.java:123: end of method: LinePosition com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.searchUp()
    }
    
    /**
     * Searches down in the document.
     * 
     * @return Line position of the next match
     */
    public LinePosition searchDown() {
        if (position == null) {
    //#IRCDocumentSearcher.java:132: method: LinePosition com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.searchDown()
    //#input(LinePosition searchDown()): ""._tainted
    //#input(LinePosition searchDown()): "(?i)"._tainted
    //#input(LinePosition searchDown()): "\E"._tainted
    //#input(LinePosition searchDown()): "\Q"._tainted
    //#input(LinePosition searchDown()): com/dmdirc/addons/ui_swing/textpane/Line.__Descendant_Table[com/dmdirc/addons/ui_swing/textpane/Line]
    //#input(LinePosition searchDown()): com/dmdirc/addons/ui_swing/textpane/Line.__Descendant_Table[others]
    //#input(LinePosition searchDown()): com/dmdirc/addons/ui_swing/textpane/Line.__Dispatch_Table.getLength()I
    //#input(LinePosition searchDown()): com/dmdirc/addons/ui_swing/textpane/Line.__Dispatch_Table.getText()Ljava/lang/String;
    //#input(LinePosition searchDown()): com/dmdirc/addons/ui_swing/textpane/LinePosition.__Descendant_Table[com/dmdirc/addons/ui_swing/textpane/LinePosition]
    //#input(LinePosition searchDown()): com/dmdirc/addons/ui_swing/textpane/LinePosition.__Descendant_Table[others]
    //#input(LinePosition searchDown()): com/dmdirc/addons/ui_swing/textpane/LinePosition.__Dispatch_Table.getStartLine()I
    //#input(LinePosition searchDown()): com/dmdirc/addons/ui_swing/textpane/LinePosition.__Dispatch_Table.getStartPos()I
    //#input(LinePosition searchDown()): this
    //#input(LinePosition searchDown()): this.caseSensitive
    //#input(LinePosition searchDown()): this.document
    //#input(LinePosition searchDown()): this.document.lines
    //#input(LinePosition searchDown()): this.phrase
    //#input(LinePosition searchDown()): this.phrase._tainted
    //#input(LinePosition searchDown()): this.position
    //#input(LinePosition searchDown()): this.position.__Tag
    //#input(LinePosition searchDown()): this.position.startLine
    //#input(LinePosition searchDown()): this.position.startPos
    //#output(LinePosition searchDown()): new LinePosition(getEndPosition#1) num objects
    //#output(LinePosition searchDown()): new LinePosition(getEndPosition#1).__Tag
    //#output(LinePosition searchDown()): new LinePosition(getEndPosition#1).endLine
    //#output(LinePosition searchDown()): new LinePosition(getEndPosition#1).endPos
    //#output(LinePosition searchDown()): new LinePosition(getEndPosition#1).startLine
    //#output(LinePosition searchDown()): new LinePosition(getEndPosition#1).startPos
    //#output(LinePosition searchDown()): return_value
    //#output(LinePosition searchDown()): this.position
    //#new obj(LinePosition searchDown()): new LinePosition(getEndPosition#1)
    //#pre[1] (LinePosition searchDown()): init'ed(this.position)
    //#pre[4] (LinePosition searchDown()): this.document != null
    //#pre[5] (LinePosition searchDown()): this.document.lines != null
    //#pre[8] (LinePosition searchDown()): (soft) this.position.__Tag == com/dmdirc/addons/ui_swing/textpane/LinePosition
    //#pre[9] (LinePosition searchDown()): (soft) init'ed(this.position.startLine)
    //#pre[10] (LinePosition searchDown()): (soft) init'ed(this.position.startPos)
    //#presumption(LinePosition searchDown()): line - java.util.List:size(...)@78 in {-2_147_483_649..4_294_967_294, 6_442_450_943}
    //#presumption(LinePosition searchDown()): getEndPosition(...)@133 init'ed
    //#presumption(LinePosition searchDown()): getLine(...).lineParts.length <= 4_294_967_295
    //#presumption(LinePosition searchDown()): java.util.Iterator:next(...).__Tag@145 == com/dmdirc/addons/ui_swing/textpane/LinePosition
    //#presumption(LinePosition searchDown()): java.util.Iterator:next(...)@145 != null
    //#presumption(LinePosition searchDown()): java.util.List:get(...)@89 != null
    //#presumption(LinePosition searchDown()): java.util.List:get(...)@89.__Tag == com/dmdirc/addons/ui_swing/textpane/Line
    //#post(LinePosition searchDown()): init'ed(return_value)
    //#post(LinePosition searchDown()): this.position == One-of{old this.position, &new LinePosition(getEndPosition#1)}
    //#post(LinePosition searchDown()): this.position != null
    //#post(LinePosition searchDown()): new LinePosition(getEndPosition#1) num objects <= 1
    //#post(LinePosition searchDown()): new LinePosition(getEndPosition#1).__Tag == com/dmdirc/addons/ui_swing/textpane/LinePosition
    //#post(LinePosition searchDown()): new LinePosition(getEndPosition#1).endLine <= 4_294_967_294
    //#post(LinePosition searchDown()): init'ed(new LinePosition(getEndPosition#1).endPos)
    //#post(LinePosition searchDown()): new LinePosition(getEndPosition#1).startLine <= 4_294_967_294
    //#post(LinePosition searchDown()): init'ed(new LinePosition(getEndPosition#1).startPos)
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.util.regex.Pattern:compile
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.util.regex.Pattern:matcher
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.util.regex.Matcher:find
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.util.regex.Matcher:start
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.util.regex.Matcher:end
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.util.List:add
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.util.List:size
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.util.List:get
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:com.dmdirc.ui.messages.Styliser:stipControlCodes
    //#unanalyzed(LinePosition searchDown()): Effects-of-calling:java.lang.String:length
    //#test_vector(LinePosition searchDown()): this.position: Inverse{null}, Addr_Set{null}
    //#test_vector(LinePosition searchDown()): java.util.Iterator:hasNext(...)@145: {0}, {1}
            position = getEndPosition();
        }
        
        int line = position.getStartLine();        
        for (int remaining = document.getNumLines(); remaining > 0; remaining--) {
            if (line < 0) {
                line = 0;
            }
             final String lineText = document.getLine(line).getText();
    //#IRCDocumentSearcher.java:141: ?!precondition failure
    //#    com/dmdirc/addons/ui_swing/textpane/Line.getText: this.lineParts != null
    //#    severity: HIGH
    //#    class: com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher
    //#    method: LinePosition searchDown()
    //#    basic block: bb_7
    //#    assertion: undefined != null
    //#    callee: String com/dmdirc/addons/ui_swing/textpane/Line.getText()
    //#    callee assertion: this.lineParts != null
    //#    callee file: Line.java
    //#    callee precondition index: [2]
    //#    callee srcpos: 103
    //#    VN: undefined
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null, Invalid}
    //#    Attribs:  Ptr  null in Bad

             final List<LinePosition> matches = searchLine(line, lineText);
            
             for (LinePosition match : matches) {
                 if (position.getStartLine() != line
                         || match.getStartPos() > position.getStartPos()) {
                     return match;
                 }
             }
            
             line++;
    //#IRCDocumentSearcher.java:152: ?overflow
    //#    line in {-2_147_483_649..4_294_967_294}
    //#    severity: LOW
    //#    class: com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher
    //#    method: LinePosition searchDown()
    //#    basic block: bb_13
    //#    assertion: line in {-2_147_483_649..4_294_967_294}
    //#    VN: line + 1
    //#    Expected: {-2_147_483_648..4_294_967_295, Invalid}
    //#    Bad: {4_294_967_296}
    //#    Attribs:  Int  Bad singleton  Bad > Exp
            
             if (line >= document.getNumLines()) {
                 line -= document.getNumLines();
                 }
        }

        return null;
    //#IRCDocumentSearcher.java:159: end of method: LinePosition com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.searchDown()
    }    

    /**
     * Searches a line and returns all matches on a line.
     * 
     * @param lineNum the line number of the line we're searching
     * @param line Line to search
     * @return List of matches
     */
    private List<LinePosition> searchLine(final int lineNum, final String line) {
        final List<LinePosition> matches = new ArrayList<LinePosition>();
    //#IRCDocumentSearcher.java:170: method: List com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.searchLine(int, String)
    //#input(List searchLine(int, String)): ""._tainted
    //#input(List searchLine(int, String)): "(?i)"._tainted
    //#input(List searchLine(int, String)): "\E"._tainted
    //#input(List searchLine(int, String)): "\Q"._tainted
    //#input(List searchLine(int, String)): line
    //#input(List searchLine(int, String)): lineNum
    //#input(List searchLine(int, String)): this
    //#input(List searchLine(int, String)): this.caseSensitive
    //#input(List searchLine(int, String)): this.phrase
    //#input(List searchLine(int, String)): this.phrase._tainted
    //#output(List searchLine(int, String)): new ArrayList(searchLine#1) num objects
    //#output(List searchLine(int, String)): return_value
    //#new obj(List searchLine(int, String)): new ArrayList(searchLine#1)
    //#presumption(List searchLine(int, String)): java.util.regex.Pattern:compile(...)@171 != null
    //#presumption(List searchLine(int, String)): java.util.regex.Pattern:matcher(...)@171 != null
    //#post(List searchLine(int, String)): return_value == &new ArrayList(searchLine#1)
    //#post(List searchLine(int, String)): new ArrayList(searchLine#1) num objects == 1
    //#test_vector(List searchLine(int, String)): java.util.regex.Matcher:find(...)@174: {0}, {1}
        final Matcher matcher = Pattern.compile((caseSensitive ? "" : "(?i)") +
                "\\Q" + phrase + "\\E").matcher(line);

        while (matcher.find()) {
            matches.add(new LinePosition(lineNum, matcher.start(), lineNum, matcher.end()));
        }

        return matches;
    //#IRCDocumentSearcher.java:178: end of method: List com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.searchLine(int, String)
    }

}
    //#output(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Descendant_Table[com/dmdirc/addons/ui_swing/textpane/IRCDocumentSearcher]
    //#output(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Dispatch_Table.getEndPosition()Lcom/dmdirc/addons/ui_swing/textpane/LinePosition;
    //#output(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Dispatch_Table.searchDown()Lcom/dmdirc/addons/ui_swing/textpane/LinePosition;
    //#output(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Dispatch_Table.searchLine(ILjava/lang/String;)Ljava/util/List;
    //#output(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Dispatch_Table.searchUp()Lcom/dmdirc/addons/ui_swing/textpane/LinePosition;
    //#output(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Dispatch_Table.setPosition(Lcom/dmdirc/addons/ui_swing/textpane/LinePosition;)V
    //#post(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Descendant_Table[com/dmdirc/addons/ui_swing/textpane/IRCDocumentSearcher] == &__Dispatch_Table
    //#post(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Dispatch_Table.getEndPosition()Lcom/dmdirc/addons/ui_swing/textpane/LinePosition; == &getEndPosition
    //#post(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Dispatch_Table.searchDown()Lcom/dmdirc/addons/ui_swing/textpane/LinePosition; == &searchDown
    //#post(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Dispatch_Table.searchLine(ILjava/lang/String;)Ljava/util/List; == &searchLine
    //#post(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Dispatch_Table.searchUp()Lcom/dmdirc/addons/ui_swing/textpane/LinePosition; == &searchUp
    //#post(com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init): __Dispatch_Table.setPosition(Lcom/dmdirc/addons/ui_swing/textpane/LinePosition;)V == &setPosition
    //#IRCDocumentSearcher.java:: end of method: com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher.com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher__static_init
    //#IRCDocumentSearcher.java:: end of class: com.dmdirc.addons.ui_swing.textpane.IRCDocumentSearcher
