//# 3 errors, 76 messages
//#
/*
    //#Command.java:1:1: class: com.dmdirc.commandparser.commands.Command
    //#Command.java:1:1: method: com.dmdirc.commandparser.commands.Command.com.dmdirc.commandparser.commands.Command__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.commandparser.commands;

import com.dmdirc.commandparser.CommandManager;
import com.dmdirc.ui.interfaces.InputWindow;
import com.dmdirc.ui.messages.Styliser;

/**
 * Represents a generic command.
 *
 * @author chris
 */
public abstract class Command {
    //#Command.java:34: method: void com.dmdirc.commandparser.commands.Command.com.dmdirc.commandparser.commands.Command()
    //#Command.java:34: end of method: void com.dmdirc.commandparser.commands.Command.com.dmdirc.commandparser.commands.Command()
    
    /** The format name used for command output. */
    protected static final String FORMAT_OUTPUT = "commandOutput";
    
    /** The format name used for command errors. */
    protected static final String FORMAT_ERROR = "commandError";
    
    /**
     * Sends a line, if appropriate, to the specified target.
     * @param target The command window to send the line to
     * @param isSilent Whether this command is being silenced or not
     * @param type The type of message to send
     * @param args The arguments of the message
     */
    protected final void sendLine(final InputWindow target,
            final boolean isSilent, final String type, final Object ... args) {
        if (!isSilent && target != null) {
    //#Command.java:51: method: void com.dmdirc.commandparser.commands.Command.sendLine(InputWindow, bool, String, Object[])
    //#input(void sendLine(InputWindow, bool, String, Object[])): args
    //#input(void sendLine(InputWindow, bool, String, Object[])): isSilent
    //#input(void sendLine(InputWindow, bool, String, Object[])): target
    //#input(void sendLine(InputWindow, bool, String, Object[])): type
    //#test_vector(void sendLine(InputWindow, bool, String, Object[])): isSilent: {1}, {0}
    //#test_vector(void sendLine(InputWindow, bool, String, Object[])): target: Addr_Set{null}, Inverse{null}
            target.addLine(type, args);
    //#Command.java:52: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.ui.interfaces.InputWindow:addLine(String, Object[])
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.commandparser.commands.Command
    //#    method: void sendLine(InputWindow, bool, String, Object[])
    //#    unanalyzed callee: void com.dmdirc.ui.interfaces.InputWindow:addLine(String, Object[])
        }
    }
    //#Command.java:54: end of method: void com.dmdirc.commandparser.commands.Command.sendLine(InputWindow, bool, String, Object[])
    
    /**
     * Sends a usage line, if appropriate, to the specified target.
     * 
     * @param target The command window to send the line to
     * @param isSilent Whether this command is being silenced or not
     * @param name The name of the command that's raising the error
     * @param args The arguments that the command accepts or expects
     */
    protected final void showUsage(final InputWindow target,
            final boolean isSilent, final String name, final String args) {
        sendLine(target, isSilent, "commandUsage", CommandManager.getCommandChar(),
    //#Command.java:66: method: void com.dmdirc.commandparser.commands.Command.showUsage(InputWindow, bool, String, String)
    //#input(void showUsage(InputWindow, bool, String, String)): args
    //#input(void showUsage(InputWindow, bool, String, String)): com/dmdirc/commandparser/CommandManager.commandChar
    //#input(void showUsage(InputWindow, bool, String, String)): isSilent
    //#input(void showUsage(InputWindow, bool, String, String)): name
    //#input(void showUsage(InputWindow, bool, String, String)): target
    //#input(void showUsage(InputWindow, bool, String, String)): this
    //#pre[2] (void showUsage(InputWindow, bool, String, String)): init'ed(com/dmdirc/commandparser/CommandManager.commandChar)
    //#unanalyzed(void showUsage(InputWindow, bool, String, String)): Effects-of-calling:com.dmdirc.ui.interfaces.InputWindow:addLine
                name, args);
    }    
    //#Command.java:68: end of method: void com.dmdirc.commandparser.commands.Command.showUsage(InputWindow, bool, String, String)
    
    /**
     * Formats the specified data into a table suitable for output in the
     * textpane. It is expected that each String[] in data has the same number
     * of elements as the headers array.
     * 
     * @param headers The headers of the table.
     * @param data The contents of the table.
     * @return A string containing an ASCII table
     */
    protected static String doTable(final String[] headers, final String[][] data) {
        final StringBuilder res = new StringBuilder();
    //#Command.java:80: method: String com.dmdirc.commandparser.commands.Command.doTable(String[], String[][])
    //#input(String doTable(String[], String[][])): data
    //#input(String doTable(String[], String[][])): data.length
    //#input(String doTable(String[], String[][])): data[0..4_294_967_295]
    //#input(String doTable(String[], String[][])): data[0..4_294_967_295].length
    //#input(String doTable(String[], String[][])): data[0..4_294_967_295][0..4_294_967_295]
    //#input(String doTable(String[], String[][])): data[0..4_294_967_295][0..4_294_967_295]._tainted
    //#input(String doTable(String[], String[][])): headers
    //#input(String doTable(String[], String[][])): headers.length
    //#input(String doTable(String[], String[][])): headers[0..4_294_967_295]
    //#input(String doTable(String[], String[][])): headers[0..4_294_967_295]._tainted
    //#output(String doTable(String[], String[][])): java.lang.StringBuilder:toString(...)._tainted
    //#output(String doTable(String[], String[][])): return_value
    //#new obj(String doTable(String[], String[][])): java.lang.StringBuilder:toString(...)
    //#pre[1] (String doTable(String[], String[][])): data != null
    //#pre[2] (String doTable(String[], String[][])): data.length <= 4_294_967_295
    //#pre[8] (String doTable(String[], String[][])): headers != null
    //#pre[3] (String doTable(String[], String[][])): (soft) data[0..4_294_967_295] != null
    //#pre[4] (String doTable(String[], String[][])): (soft) data[0..4_294_967_295].length in {1..4_294_967_295}
    //#pre[5] (String doTable(String[], String[][])): (soft) data[0..4_294_967_295].length - headers.length in {0..4_294_967_294}
    //#pre[6] (String doTable(String[], String[][])): (soft) data[0..4_294_967_295][0..4_294_967_295] != null
    //#pre[9] (String doTable(String[], String[][])): (soft) headers.length in {1..4_294_967_295}
    //#pre[10] (String doTable(String[], String[][])): (soft) headers[0..4_294_967_295] != null
    //#presumption(String doTable(String[], String[][])): java.lang.String:length(...)@87 <= 4_294_967_292
    //#presumption(String doTable(String[], String[][])): java.lang.String:length(...)@90 <= 4_294_967_292
    //#post(String doTable(String[], String[][])): init'ed(java.lang.StringBuilder:toString(...)._tainted)
    //#post(String doTable(String[], String[][])): return_value == &java.lang.StringBuilder:toString(...)
    //#unanalyzed(String doTable(String[], String[][])): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(String doTable(String[], String[][])): Effects-of-calling:java.lang.String:length
        res.append(Styliser.CODE_FIXED);
        res.append(Styliser.CODE_BOLD);
        
        int[] maxsizes = new int[headers.length];
        
        for (int i = 0; i < headers.length; i++) {
            maxsizes[i] = headers[i].length() + 3;
            
            for (int j = 0; j < data.length; j++) {
                maxsizes[i] = Math.max(maxsizes[i], data[j][i].length() + 3);
    //#Command.java:90: ?array index out of bounds
    //#    i < data[j].length
    //#    severity: MEDIUM
    //#    class: com.dmdirc.commandparser.commands.Command
    //#    method: String doTable(String[], String[][])
    //#    basic block: bb_5
    //#    assertion: i < data[j].length
    //#    VN: data[j].length - i
    //#    Expected: {1..+Inf}
    //#    Bad: {-4_294_967_293..0}
    //#    Attribs:  Int  Bad overlaps +/-1000  Bad < Exp
            }
            
            doPadding(res, headers[i], maxsizes[i]);
        }
                
        for (String[] source : data) {
            res.append('\n');
            res.append(Styliser.CODE_FIXED);
            
            for (int i = 0; i < source.length; i++) {
                doPadding(res, source[i], maxsizes[i]);
    //#Command.java:101: ?array index out of bounds
    //#    i < maxsizes.length
    //#    severity: MEDIUM
    //#    class: com.dmdirc.commandparser.commands.Command
    //#    method: String doTable(String[], String[][])
    //#    basic block: bb_11
    //#    assertion: i < maxsizes.length
    //#    VN: -(i - headers.length)
    //#    Expected: {1..+Inf}
    //#    Bad: {0}
    //#    Attribs:  Int  Bad singleton  Bad overlaps +/-1000  Bad < Exp
    //#Command.java:101: ?use of default init
    //#    init'ed(maxsizes[i])
    //#    severity: LOW
    //#    class: com.dmdirc.commandparser.commands.Command
    //#    method: String doTable(String[], String[][])
    //#    basic block: bb_11
    //#    assertion: init'ed(maxsizes[i])
    //#    VN: maxsizes[i]
    //#    Expected: {-Inf..+Inf}
    //#    Bad: {Invalid}
    //#    Attribs:  Int  Bad only invalid
            }
        }
        
        return res.toString();
    //#Command.java:105: end of method: String com.dmdirc.commandparser.commands.Command.doTable(String[], String[][])
    }
    
    /**
     * Adds the specified data to the stringbuilder, padding with spaces to
     * the specified size.
     * 
     * @param builder The stringbuilder to append data to
     * @param data The data to be added
     * @param size The minimum size that should be used
     */
    private static void doPadding(final StringBuilder builder, final String data,
            final int size) {
        builder.append(data);
    //#Command.java:118: method: void com.dmdirc.commandparser.commands.Command.doPadding(StringBuilder, String, int)
    //#input(void doPadding(StringBuilder, String, int)): builder
    //#input(void doPadding(StringBuilder, String, int)): builder._tainted
    //#input(void doPadding(StringBuilder, String, int)): data
    //#input(void doPadding(StringBuilder, String, int)): data._tainted
    //#input(void doPadding(StringBuilder, String, int)): size
    //#output(void doPadding(StringBuilder, String, int)): builder._tainted
    //#pre[1] (void doPadding(StringBuilder, String, int)): builder != null
    //#pre[2] (void doPadding(StringBuilder, String, int)): data != null
    //#post(void doPadding(StringBuilder, String, int)): builder._tainted == old builder._tainted | data._tainted
    //#post(void doPadding(StringBuilder, String, int)): init'ed(builder._tainted)
        
        for (int i = 0; i < size - data.length(); i++) {
            builder.append(' ');
        }
    }
    //#Command.java:123: end of method: void com.dmdirc.commandparser.commands.Command.doPadding(StringBuilder, String, int)

}
    //#output(com.dmdirc.commandparser.commands.Command__static_init): __Descendant_Table[com/dmdirc/commandparser/commands/Command]
    //#output(com.dmdirc.commandparser.commands.Command__static_init): __Dispatch_Table.sendLine(Lcom/dmdirc/ui/interfaces/InputWindow;ZLjava/lang/String;[Ljava/lang/Object;)V
    //#output(com.dmdirc.commandparser.commands.Command__static_init): __Dispatch_Table.showUsage(Lcom/dmdirc/ui/interfaces/InputWindow;ZLjava/lang/String;Ljava/lang/String;)V
    //#post(com.dmdirc.commandparser.commands.Command__static_init): __Descendant_Table[com/dmdirc/commandparser/commands/Command] == &__Dispatch_Table
    //#post(com.dmdirc.commandparser.commands.Command__static_init): __Dispatch_Table.sendLine(Lcom/dmdirc/ui/interfaces/InputWindow;ZLjava/lang/String;[Ljava/lang/Object;)V == &sendLine
    //#post(com.dmdirc.commandparser.commands.Command__static_init): __Dispatch_Table.showUsage(Lcom/dmdirc/ui/interfaces/InputWindow;ZLjava/lang/String;Ljava/lang/String;)V == &showUsage
    //#Command.java:: end of method: com.dmdirc.commandparser.commands.Command.com.dmdirc.commandparser.commands.Command__static_init
    //#Command.java:: end of class: com.dmdirc.commandparser.commands.Command
