//# 4 errors, 187 messages
//#
/*
    //#Formatter.java:1:1: class: com.dmdirc.ui.messages.Formatter
 * 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.ui.messages;

import com.dmdirc.Precondition;
import com.dmdirc.config.ConfigManager;

import java.util.HashMap;
import java.util.IllegalFormatConversionException;
import java.util.Map;
import java.util.MissingFormatArgumentException;
import java.util.UnknownFormatConversionException;

/**
 * The Formatter provides a standard way to format messages for display.
 */
public final class Formatter {
    //#Formatter.java:37: method: com.dmdirc.ui.messages.Formatter.com.dmdirc.ui.messages.Formatter__static_init
    //#output(com.dmdirc.ui.messages.Formatter__static_init): $assertionsDisabled
    //#output(com.dmdirc.ui.messages.Formatter__static_init): __Descendant_Table[com/dmdirc/ui/messages/Formatter]
    //#output(com.dmdirc.ui.messages.Formatter__static_init): new HashMap(Formatter__static_init#1) num objects
    //#output(com.dmdirc.ui.messages.Formatter__static_init): typeCache
    //#new obj(com.dmdirc.ui.messages.Formatter__static_init): new HashMap(Formatter__static_init#1)
    //#post(com.dmdirc.ui.messages.Formatter__static_init): $assertionsDisabled == 0
    //#post(com.dmdirc.ui.messages.Formatter__static_init): __Descendant_Table[com/dmdirc/ui/messages/Formatter] == &__Dispatch_Table
    //#post(com.dmdirc.ui.messages.Formatter__static_init): typeCache == &new HashMap(Formatter__static_init#1)
    //#post(com.dmdirc.ui.messages.Formatter__static_init): new HashMap(Formatter__static_init#1) num objects == 1
       
    /**
     * A cache of types needed by the various formatters.
     */
    private static final Map<String, Character[]> typeCache
    //#Formatter.java:42: end of method: com.dmdirc.ui.messages.Formatter.com.dmdirc.ui.messages.Formatter__static_init
            = new HashMap<String, Character[]>();
   
    /**
     * Creates a new instance of Formatter.
     */
    private Formatter() {
    //#Formatter.java:48: method: void com.dmdirc.ui.messages.Formatter.com.dmdirc.ui.messages.Formatter()
        // Shouldn't be used
    }
    //#Formatter.java:50: end of method: void com.dmdirc.ui.messages.Formatter.com.dmdirc.ui.messages.Formatter()
    
    /**
     * Inserts the supplied arguments into a format string for the specified
     * message type.
     * 
     * @param messageType The message type that the arguments should be formatted as
     * @param config The config manager to use to format the message
     * @param arguments The arguments to this message type
     * @return A formatted string
     */
    @Precondition("The specified message type is not null")
    public static String formatMessage(final ConfigManager config, final String messageType,
            final Object... arguments) {
        assert(messageType != null);
    //#Formatter.java:64: method: String com.dmdirc.ui.messages.Formatter.formatMessage(ConfigManager, String, Object[])
    //#input(String formatMessage(ConfigManager, String, Object[])): ""._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "$"._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "%"._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): ", "._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "; Error: Illegal format conversion: "._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "; Error: Missing format argument: "._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "; Error: Unknown format conversion: "._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "<Invalid format string for message type "._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "<No format string for message type "._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): ">"._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "day"._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "hour"._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "minute"._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): "second"._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): arguments
    //#input(String formatMessage(ConfigManager, String, Object[])): arguments.length
    //#input(String formatMessage(ConfigManager, String, Object[])): arguments[0..4_294_967_295]
    //#input(String formatMessage(ConfigManager, String, Object[])): arguments[0..4_294_967_295]._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): config
    //#input(String formatMessage(ConfigManager, String, Object[])): messageType
    //#input(String formatMessage(ConfigManager, String, Object[])): messageType._tainted
    //#input(String formatMessage(ConfigManager, String, Object[])): typeCache
    //#output(String formatMessage(ConfigManager, String, Object[])): java.lang.StringBuilder:toString(...)._tainted
    //#output(String formatMessage(ConfigManager, String, Object[])): return_value
    //#new obj(String formatMessage(ConfigManager, String, Object[])): java.lang.StringBuilder:toString(...)
    //#pre[5] (String formatMessage(ConfigManager, String, Object[])): config != null
    //#pre[6] (String formatMessage(ConfigManager, String, Object[])): messageType != null
    //#pre[1] (String formatMessage(ConfigManager, String, Object[])): (soft) arguments != null
    //#pre[2] (String formatMessage(ConfigManager, String, Object[])): (soft) arguments.length <= 4_294_967_295
    //#pre[3] (String formatMessage(ConfigManager, String, Object[])): (soft) arguments[0..4_294_967_295] != null
    //#presumption(String formatMessage(ConfigManager, String, Object[])): com.dmdirc.config.ConfigManager:getOption(...)@66 != null
    //#post(String formatMessage(ConfigManager, String, Object[])): init'ed(java.lang.StringBuilder:toString(...)._tainted)
    //#post(String formatMessage(ConfigManager, String, Object[])): init'ed(return_value)
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.String:charAt
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.Character:valueOf
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.util.Map:put
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.StringBuilder:length
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.util.Map:containsKey
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.util.Map:get
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.Character:charValue
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.String:valueOf
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.Integer:valueOf
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.Float:valueOf
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.String:instanceof
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.Long:valueOf
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.Long:longValue
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.Object:toString
    //#unanalyzed(String formatMessage(ConfigManager, String, Object[])): Effects-of-calling:java.lang.Integer:intValue
    //#test_vector(String formatMessage(ConfigManager, String, Object[])): com.dmdirc.config.ConfigManager:hasOptionString(...)@66: {1}, {0}
                
        final String res = config.hasOptionString("formatter", messageType) ?
    //#Formatter.java:66: Warning: method not available - call not analyzed
    //#    call on bool com.dmdirc.config.ConfigManager:hasOptionString(String, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.messages.Formatter
    //#    method: String formatMessage(ConfigManager, String, Object[])
    //#    unanalyzed callee: bool com.dmdirc.config.ConfigManager:hasOptionString(String, String)
    //#Formatter.java:66: Warning: method not available - call not analyzed
    //#    call on String com.dmdirc.config.ConfigManager:getOption(String, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.messages.Formatter
    //#    method: String formatMessage(ConfigManager, String, Object[])
    //#    unanalyzed callee: String com.dmdirc.config.ConfigManager:getOption(String, String)
            config.getOption("formatter", messageType).replace("%-1$", "%"
            + arguments.length + "$"): null;
        
        if (res == null) {
            return "<No format string for message type " + messageType + ">";
        } else {
            try {
                final Object[] newArgs = castArguments(res, arguments);
                return String.format(res.replaceAll("(%[0-9]+\\$)u", "$1s"), newArgs);
            } catch (IllegalFormatConversionException ex) {
                return "<Invalid format string for message type " + messageType
                        + "; Error: Illegal format conversion: " + ex.getMessage() + ">";
            } catch (UnknownFormatConversionException ex) {
                return "<Invalid format string for message type " + messageType
                        + "; Error: Unknown format conversion: " + ex.getMessage() + ">";
            } catch (MissingFormatArgumentException ex) {
                return "<Invalid format string for message type " + messageType
    //#Formatter.java:83: end of method: String com.dmdirc.ui.messages.Formatter.formatMessage(ConfigManager, String, Object[])
                        + "; Error: Missing format argument: " + ex.getMessage() + ">";
            }
        }
    }
    
    /**
     * Casts the specified arguments to the relevant classes, based on the
     * format type cache.
     *
     * @param format The format to be used
     * @param args The arguments to be casted
     * @return A new set of arguments of appropriate types
     */
    @Precondition("The specified format is not null")
    private static Object[] castArguments(final String format, final Object[] args) {
        assert(format != null);
    //#Formatter.java:99: method: Object[] com.dmdirc.ui.messages.Formatter.castArguments(String, Object[])
    //#input(Object[] castArguments(String, Object[])): ""._tainted
    //#input(Object[] castArguments(String, Object[])): "$"._tainted
    //#input(Object[] castArguments(String, Object[])): "%"._tainted
    //#input(Object[] castArguments(String, Object[])): ", "._tainted
    //#input(Object[] castArguments(String, Object[])): "day"._tainted
    //#input(Object[] castArguments(String, Object[])): "hour"._tainted
    //#input(Object[] castArguments(String, Object[])): "minute"._tainted
    //#input(Object[] castArguments(String, Object[])): "second"._tainted
    //#input(Object[] castArguments(String, Object[])): args
    //#input(Object[] castArguments(String, Object[])): args.length
    //#input(Object[] castArguments(String, Object[])): args[0..4_294_967_295]
    //#input(Object[] castArguments(String, Object[])): args[0..4_294_967_295]._tainted
    //#input(Object[] castArguments(String, Object[])): format
    //#input(Object[] castArguments(String, Object[])): typeCache
    //#output(Object[] castArguments(String, Object[])): java.lang.String:valueOf(...)._tainted
    //#output(Object[] castArguments(String, Object[])): java.lang.StringBuilder:toString(...)._tainted
    //#output(Object[] castArguments(String, Object[])): new Object[](castArguments#1) num objects
    //#output(Object[] castArguments(String, Object[])): return_value.length
    //#output(Object[] castArguments(String, Object[])): return_value[0..4_294_967_295]
    //#output(Object[] castArguments(String, Object[])): return_value
    //#new obj(Object[] castArguments(String, Object[])): java.lang.String:valueOf(...)
    //#new obj(Object[] castArguments(String, Object[])): java.lang.StringBuilder:toString(...)
    //#new obj(Object[] castArguments(String, Object[])): new Object[](castArguments#1)
    //#pre[1] (Object[] castArguments(String, Object[])): args != null
    //#pre[5] (Object[] castArguments(String, Object[])): format != null
    //#pre[2] (Object[] castArguments(String, Object[])): (soft) args.length <= 4_294_967_295
    //#pre[3] (Object[] castArguments(String, Object[])): (soft) args[0..4_294_967_295] != null
    //#presumption(Object[] castArguments(String, Object[])): arr$.length@108 <= 4_294_967_295
    //#presumption(Object[] castArguments(String, Object[])): arr$.length@108 - args.length in {-4_294_967_295..0}
    //#presumption(Object[] castArguments(String, Object[])): arr$[i$]@108 != null
    //#presumption(Object[] castArguments(String, Object[])): java.lang.Integer:valueOf(...)@141 != null
    //#presumption(Object[] castArguments(String, Object[])): java.lang.Long:longValue(...)@134 in {-9_223_372_036_854_775..18_446_744_073_709_551}
    //#presumption(Object[] castArguments(String, Object[])): java.lang.Long:valueOf(...)@134 != null
    //#presumption(Object[] castArguments(String, Object[])): java.util.Map:get(...)@108 != null
    //#post(Object[] castArguments(String, Object[])): init'ed(java.lang.String:valueOf(...)._tainted)
    //#post(Object[] castArguments(String, Object[])): init'ed(java.lang.StringBuilder:toString(...)._tainted)
    //#post(Object[] castArguments(String, Object[])): return_value == &new Object[](castArguments#1)
    //#post(Object[] castArguments(String, Object[])): new Object[](castArguments#1) num objects == 1
    //#post(Object[] castArguments(String, Object[])): return_value.length == args.length
    //#post(Object[] castArguments(String, Object[])): return_value.length <= 4_294_967_295
    //#post(Object[] castArguments(String, Object[])): possibly_updated(return_value[0..4_294_967_295])
    //#unanalyzed(Object[] castArguments(String, Object[])): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(Object[] castArguments(String, Object[])): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(Object[] castArguments(String, Object[])): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(Object[] castArguments(String, Object[])): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(Object[] castArguments(String, Object[])): Effects-of-calling:java.lang.String:charAt
    //#unanalyzed(Object[] castArguments(String, Object[])): Effects-of-calling:java.lang.Character:valueOf
    //#unanalyzed(Object[] castArguments(String, Object[])): Effects-of-calling:java.util.Map:put
    //#unanalyzed(Object[] castArguments(String, Object[])): Effects-of-calling:java.lang.StringBuilder:length
    //#test_vector(Object[] castArguments(String, Object[])): java.lang.Character:charValue(...)@113: {65, 69, 71, 97, 101..103}, {66, 72, 83, 98, 104, 115}, {67, 99}, {84, 116}, {88, 100, 111, 120}, {117}, {0..64, 68, 70, 73..82, 85..87, 89..96, 105..110, 112..114, 118,119, 121..65_535}
    //#test_vector(Object[] castArguments(String, Object[])): java.lang.String:instanceof(...)@132: {0}, {1}
    //#test_vector(Object[] castArguments(String, Object[])): java.util.Map:containsKey(...)@101: {1}, {0}
        
        if (!typeCache.containsKey(format)) {
            analyseFormat(format, args);
        }
        
        final Object[] res = new Object[args.length];
        
        int i = 0;
        for (Character chr : typeCache.get(format)) {
            if (i >= args.length) {
                break;
            }
            
            switch (chr) {
            case 'b': case 'B': case 'h': case 'H': case 's': case 'S':
                // General (strings)
                res[i] = String.valueOf(args[i]);
                break;
            case 'c': case 'C':
                // Character
                res[i] = String.valueOf(args[i]).charAt(0);
                break;
            case 'd': case 'o': case 'x': case 'X':
                // Integers
                res[i] = Integer.valueOf((String) args[i]);
                break;
            case 'e': case 'E': case 'f': case 'g': case 'G': case 'a': case 'A':
                // Floating point
                res[i] = Float.valueOf((String) args[i]);
                break;
            case 't': case 'T':
                // Date
                if (args[i] instanceof String) {
                    // Assume it's a timestamp(?)
                    res[i] = Long.valueOf(1000 * Long.valueOf((String) args[i]));
                } else {
                    res[i] = args[i];
                }
                break;
            case 'u':
                // Duration hacks
                res[i] = formatDuration(Integer.valueOf(String.valueOf(args[i].toString())));
                break;
            default:
                res[i] = args[i];
            }
            
            i++;
        }
        
        return res;
    //#Formatter.java:150: end of method: Object[] com.dmdirc.ui.messages.Formatter.castArguments(String, Object[])
    }
    
    /**
     * Tests for and adds one component of the duration format.
     * 
     * @param builder The string builder to append text to
     * @param current The number of seconds in the duration
     * @param duration The number of seconds in this component
     * @param name The name of this component
     * @return The number of seconds used by this component
     */
    private static int doDuration(final StringBuilder builder, final int current,
            final int duration, final String name) {
        int res = 0;
    //#Formatter.java:164: method: int com.dmdirc.ui.messages.Formatter.doDuration(StringBuilder, int, int, String)
    //#input(int doDuration(StringBuilder, int, int, String)): ""._tainted
    //#input(int doDuration(StringBuilder, int, int, String)): ", "._tainted
    //#input(int doDuration(StringBuilder, int, int, String)): builder
    //#input(int doDuration(StringBuilder, int, int, String)): builder._tainted
    //#input(int doDuration(StringBuilder, int, int, String)): current
    //#input(int doDuration(StringBuilder, int, int, String)): duration
    //#input(int doDuration(StringBuilder, int, int, String)): name
    //#input(int doDuration(StringBuilder, int, int, String)): name._tainted
    //#output(int doDuration(StringBuilder, int, int, String)): builder._tainted
    //#output(int doDuration(StringBuilder, int, int, String)): return_value
    //#pre[1] (int doDuration(StringBuilder, int, int, String)): (soft) builder != null
    //#pre[4] (int doDuration(StringBuilder, int, int, String)): (soft) current/duration in {-2_147_483_648..4_294_967_295}
    //#pre[5] (int doDuration(StringBuilder, int, int, String)): (soft) duration != 0
    //#pre[9] (int doDuration(StringBuilder, int, int, String)): (soft) duration*(current/duration) in {-2_147_483_648..4_294_967_295}
    //#post(int doDuration(StringBuilder, int, int, String)): init'ed(builder._tainted)
    //#post(int doDuration(StringBuilder, int, int, String)): return_value == One-of{0, duration*(current/duration)}
    //#post(int doDuration(StringBuilder, int, int, String)): init'ed(return_value)
    //#test_vector(int doDuration(StringBuilder, int, int, String)): duration - current: {1..6_442_450_943}, {-6_442_450_943..0}
    //#test_vector(int doDuration(StringBuilder, int, int, String)): java.lang.StringBuilder:length(...)@170: {-2_147_483_648..0}, {1..4_294_967_295}
        
        if (current >= duration) {
            final int units = current / duration;
            res = units * duration;
            
            if (builder.length() > 0) {
                builder.append(", ");
            }
            
            builder.append(units);
            builder.append(' ');
            builder.append(name + (units != 1 ? 's' : ""));
        }
        
        return res;
    //#Formatter.java:179: end of method: int com.dmdirc.ui.messages.Formatter.doDuration(StringBuilder, int, int, String)
    }
    
    /**
     * Formats the specified number of seconds as a string containing the
     * number of days, hours, minutes and seconds.
     * 
     * @param duration The duration in seconds to be formatted
     * @return A textual version of the duration
     */
    public static String formatDuration(final int duration) {
        final StringBuilder buff = new StringBuilder();
    //#Formatter.java:190: method: String com.dmdirc.ui.messages.Formatter.formatDuration(int)
    //#input(String formatDuration(int)): ""._tainted
    //#input(String formatDuration(int)): ", "._tainted
    //#input(String formatDuration(int)): "day"._tainted
    //#input(String formatDuration(int)): "hour"._tainted
    //#input(String formatDuration(int)): "minute"._tainted
    //#input(String formatDuration(int)): "second"._tainted
    //#input(String formatDuration(int)): duration
    //#output(String formatDuration(int)): java.lang.StringBuilder:toString(...)._tainted
    //#output(String formatDuration(int)): return_value
    //#new obj(String formatDuration(int)): java.lang.StringBuilder:toString(...)
    //#post(String formatDuration(int)): init'ed(java.lang.StringBuilder:toString(...)._tainted)
    //#post(String formatDuration(int)): return_value == &java.lang.StringBuilder:toString(...)
    //#unanalyzed(String formatDuration(int)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(String formatDuration(int)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(String formatDuration(int)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(String formatDuration(int)): Effects-of-calling:java.lang.Character:valueOf
    //#unanalyzed(String formatDuration(int)): Effects-of-calling:java.lang.StringBuilder:length
        
        int seconds = duration;
        
        seconds -= doDuration(buff, seconds, 60*60*24, "day");
    //#Formatter.java:194: Warning: unused assignment in callee
    //#    Unused assignment to (java.lang.StringBuilder:append.return_value@176._tainted) in doDuration
    //#    severity: LOW
    //#    class: com.dmdirc.ui.messages.Formatter
    //#    method: String formatDuration(int)
    //#Formatter.java:194: ?overflow
    //#    seconds - doDuration(...) in {-2_147_483_648..4_294_967_295}
    //#    severity: SUPPRESSED
    //#    class: com.dmdirc.ui.messages.Formatter
    //#    method: String formatDuration(int)
    //#    basic block: Entry_BB_1
    //#    assertion: seconds - doDuration(...) in {-2_147_483_648..4_294_967_295}
    //#    VN: -(res - duration)
    //#    Expected: {-2_147_483_648..4_294_967_295, Invalid}
    //#    Bad: {-6_442_427_648..-2_147_483_649}
    //#    Attribs:  Int  Bad < Exp
        seconds -= doDuration(buff, seconds, 60*60, "hour");
    //#Formatter.java:195: Warning: unused assignment in callee
    //#    Unused assignment to (java.lang.StringBuilder:append.return_value@176._tainted) in doDuration
    //#    severity: LOW
    //#    class: com.dmdirc.ui.messages.Formatter
    //#    method: String formatDuration(int)
    //#Formatter.java:195: ?overflow
    //#    seconds - doDuration(...) in {-2_147_483_648..4_294_967_295}
    //#    severity: SUPPRESSED
    //#    class: com.dmdirc.ui.messages.Formatter
    //#    method: String formatDuration(int)
    //#    basic block: Entry_BB_1
    //#    assertion: seconds - doDuration(...) in {-2_147_483_648..4_294_967_295}
    //#    VN: -((res - duration) + res)
    //#    Expected: {-2_147_483_648..4_294_967_295, Invalid}
    //#    Bad: {-6_442_449_248..-2_147_483_649}
    //#    Attribs:  Int  Bad < Exp
        seconds -= doDuration(buff, seconds, 60, "minute");
    //#Formatter.java:196: Warning: unused assignment in callee
    //#    Unused assignment to (java.lang.StringBuilder:append.return_value@176._tainted) in doDuration
    //#    severity: LOW
    //#    class: com.dmdirc.ui.messages.Formatter
    //#    method: String formatDuration(int)
    //#Formatter.java:196: ?overflow
    //#    seconds - doDuration(...) in {-2_147_483_648..4_294_967_295}
    //#    severity: SUPPRESSED
    //#    class: com.dmdirc.ui.messages.Formatter
    //#    method: String formatDuration(int)
    //#    basic block: Entry_BB_1
    //#    assertion: seconds - doDuration(...) in {-2_147_483_648..4_294_967_295}
    //#    VN: -((res - duration) + res + res)
    //#    Expected: {-2_147_483_648..4_294_967_295, Invalid}
    //#    Bad: {-6_442_450_928..-2_147_483_649}
    //#    Attribs:  Int  Bad < Exp
        seconds -= doDuration(buff, seconds, 1, "second");
    //#Formatter.java:197: Warning: unused assignment
    //#    Unused assignment into seconds
    //#    severity: LOW
    //#    class: com.dmdirc.ui.messages.Formatter
    //#    method: String formatDuration(int)
    //#Formatter.java:197: ?overflow
    //#    seconds - doDuration(...) in {-2_147_483_648..4_294_967_295}
    //#    severity: SUPPRESSED
    //#    class: com.dmdirc.ui.messages.Formatter
    //#    method: String formatDuration(int)
    //#    basic block: Entry_BB_1
    //#    assertion: seconds - doDuration(...) in {-2_147_483_648..4_294_967_295}
    //#    VN: -((res - duration) + res + res + res)
    //#    Expected: {-2_147_483_648..4_294_967_295, Invalid}
    //#    Bad: {-6_442_450_943..-2_147_483_649}
    //#    Attribs:  Int  Bad < Exp
        
        return buff.toString();
    //#Formatter.java:199: end of method: String com.dmdirc.ui.messages.Formatter.formatDuration(int)
    }
    
    /**
     * Analyses the specified format string and fills in the format type cache.
     *
     * @param format The format to analyse
     * @param args The raw arguments
     */
    private static void analyseFormat(final String format, final Object[] args) {
        final Character[] types = new Character[args.length];
    //#Formatter.java:209: method: void com.dmdirc.ui.messages.Formatter.analyseFormat(String, Object[])
    //#input(void analyseFormat(String, Object[])): "$"._tainted
    //#input(void analyseFormat(String, Object[])): "%"._tainted
    //#input(void analyseFormat(String, Object[])): args
    //#input(void analyseFormat(String, Object[])): args.length
    //#input(void analyseFormat(String, Object[])): format
    //#input(void analyseFormat(String, Object[])): typeCache
    //#pre[1] (void analyseFormat(String, Object[])): args != null
    //#pre[2] (void analyseFormat(String, Object[])): args.length <= 4_294_967_295
    //#pre[3] (void analyseFormat(String, Object[])): (soft) format != null
    //#presumption(void analyseFormat(String, Object[])): java.lang.String:indexOf(...)@212 <= 4_294_967_292
    //#test_vector(void analyseFormat(String, Object[])): java.lang.String:indexOf(...)@212: {-2_147_483_648..-1}, {0..4_294_967_292}
        
        for (int i = 0; i < args.length; i++) {
            final int index = format.indexOf("%" + (i + 1) + "$");
            
            if (index > -1) {
                types[i] = format.charAt(index + 3);
            } else {
                types[i] = 's';
            }
        }
        
        typeCache.put(format, types);
    }
    //#Formatter.java:222: end of method: void com.dmdirc.ui.messages.Formatter.analyseFormat(String, Object[])

}
    //#Formatter.java:: end of class: com.dmdirc.ui.messages.Formatter
