//# 6 errors, 326 messages
//#
/*
    //#AliasWrapper.java:1:1: class: com.dmdirc.actions.wrappers.AliasWrapper
    //#AliasWrapper.java:1:1: method: com.dmdirc.actions.wrappers.AliasWrapper.com.dmdirc.actions.wrappers.AliasWrapper__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.actions.wrappers;

import com.dmdirc.GlobalWindow;
import com.dmdirc.Server;
import com.dmdirc.ServerManager;
import com.dmdirc.actions.Action;
import com.dmdirc.actions.ActionCondition;
import com.dmdirc.actions.ActionGroup;
import com.dmdirc.actions.CoreActionType;
import com.dmdirc.commandparser.CommandManager;
import com.dmdirc.logger.ErrorLevel;
import com.dmdirc.logger.Logger;
import com.dmdirc.ui.input.TabCompletionType;

import java.util.ArrayList;
import java.util.List;

/**
 * Encapsulates alias actions.
 *
 * @author chris
 */
public final class AliasWrapper extends ActionGroup {
    
    /** Singleton instance of the alias wrapper. */
    private static AliasWrapper me;
    
    /** A list of registered alias names. */
    private final List<String> aliases = new ArrayList<String>();
    
    /**
     * Creates a new instance of AliasWrapper.
     */
    private AliasWrapper() {
        super("aliases");
    //#AliasWrapper.java:57: method: void com.dmdirc.actions.wrappers.AliasWrapper.com.dmdirc.actions.wrappers.AliasWrapper()
    //#input(void com.dmdirc.actions.wrappers.AliasWrapper()): this
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): new ArrayList(ActionGroup#1) num objects
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): new ArrayList(AliasWrapper#1) num objects
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): new HashMap(ActionGroup#2) num objects
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): this.actions
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): this.aliases
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): this.author
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): this.component
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): this.description
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): this.name
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): this.settings
    //#output(void com.dmdirc.actions.wrappers.AliasWrapper()): this.version
    //#new obj(void com.dmdirc.actions.wrappers.AliasWrapper()): new ArrayList(ActionGroup#1)
    //#new obj(void com.dmdirc.actions.wrappers.AliasWrapper()): new ArrayList(AliasWrapper#1)
    //#new obj(void com.dmdirc.actions.wrappers.AliasWrapper()): new HashMap(ActionGroup#2)
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): this.actions == &new ArrayList(ActionGroup#1)
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): this.aliases == &new ArrayList(AliasWrapper#1)
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): this.author == null
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): this.description == null
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): this.component == -1
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): this.version == -1
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): this.name == &"aliases"
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): this.settings == &new HashMap(ActionGroup#2)
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): new ArrayList(ActionGroup#1) num objects == 1
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): new ArrayList(AliasWrapper#1) num objects == 1
    //#post(void com.dmdirc.actions.wrappers.AliasWrapper()): new HashMap(ActionGroup#2) num objects == 1
    //#unanalyzed(void com.dmdirc.actions.wrappers.AliasWrapper()): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(void com.dmdirc.actions.wrappers.AliasWrapper()): Effects-of-calling:java.util.HashMap
    }
    //#AliasWrapper.java:58: end of method: void com.dmdirc.actions.wrappers.AliasWrapper.com.dmdirc.actions.wrappers.AliasWrapper()
    
    /**
     * Retrieves a singleton instance of this alias wrapper.
     *
     * @return A singleton instance of AliasWrapper
     */
    public static synchronized AliasWrapper getAliasWrapper() {
        if (me == null) {
    //#AliasWrapper.java:66: method: AliasWrapper com.dmdirc.actions.wrappers.AliasWrapper.getAliasWrapper()
    //#input(AliasWrapper getAliasWrapper()): __Class_Obj.__Lock
    //#input(AliasWrapper getAliasWrapper()): me
    //#output(AliasWrapper getAliasWrapper()): me
    //#output(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1) num objects
    //#output(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).__Tag
    //#output(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).actions
    //#output(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).aliases
    //#output(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).author
    //#output(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).component
    //#output(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).description
    //#output(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).name
    //#output(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).settings
    //#output(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).version
    //#output(AliasWrapper getAliasWrapper()): new ArrayList(ActionGroup#1) num objects
    //#output(AliasWrapper getAliasWrapper()): new ArrayList(AliasWrapper#1) num objects
    //#output(AliasWrapper getAliasWrapper()): new HashMap(ActionGroup#2) num objects
    //#output(AliasWrapper getAliasWrapper()): return_value
    //#new obj(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1)
    //#new obj(AliasWrapper getAliasWrapper()): new ArrayList(ActionGroup#1)
    //#new obj(AliasWrapper getAliasWrapper()): new ArrayList(AliasWrapper#1)
    //#new obj(AliasWrapper getAliasWrapper()): new HashMap(ActionGroup#2)
    //#pre[1] (AliasWrapper getAliasWrapper()): init'ed(me)
    //#post(AliasWrapper getAliasWrapper()): me == One-of{old me, &new AliasWrapper(getAliasWrapper#1)}
    //#post(AliasWrapper getAliasWrapper()): me != null
    //#post(AliasWrapper getAliasWrapper()): return_value == me
    //#post(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1) num objects <= 1
    //#post(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).__Tag == com/dmdirc/actions/wrappers/AliasWrapper
    //#post(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).actions == &new ArrayList(ActionGroup#1)
    //#post(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).aliases == &new ArrayList(AliasWrapper#1)
    //#post(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).author == null
    //#post(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).component == -1
    //#post(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).description == null
    //#post(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).name == &"aliases"
    //#post(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).settings == &new HashMap(ActionGroup#2)
    //#post(AliasWrapper getAliasWrapper()): new AliasWrapper(getAliasWrapper#1).version == -1
    //#post(AliasWrapper getAliasWrapper()): new ArrayList(ActionGroup#1) num objects <= 1
    //#post(AliasWrapper getAliasWrapper()): new ArrayList(AliasWrapper#1) num objects <= 1
    //#post(AliasWrapper getAliasWrapper()): new HashMap(ActionGroup#2) num objects <= 1
    //#unanalyzed(AliasWrapper getAliasWrapper()): Effects-of-calling:com.dmdirc.actions.ActionGroup
    //#unanalyzed(AliasWrapper getAliasWrapper()): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(AliasWrapper getAliasWrapper()): Effects-of-calling:java.util.HashMap
    //#test_vector(AliasWrapper getAliasWrapper()): me: Inverse{null}, Addr_Set{null}
            me = new AliasWrapper();
        }
        
        return me;
    //#AliasWrapper.java:70: end of method: AliasWrapper com.dmdirc.actions.wrappers.AliasWrapper.getAliasWrapper()
    }
    
    /**
     * Retrieves a list of alias names registered with this wrapper.
     * 
     * @return A list of alias names
     */
    public List<String> getAliases() {
        return new ArrayList<String>(aliases);
    //#AliasWrapper.java:79: method: List com.dmdirc.actions.wrappers.AliasWrapper.getAliases()
    //#input(List getAliases()): this
    //#input(List getAliases()): this.aliases
    //#output(List getAliases()): new ArrayList(getAliases#1) num objects
    //#output(List getAliases()): return_value
    //#new obj(List getAliases()): new ArrayList(getAliases#1)
    //#post(List getAliases()): return_value == &new ArrayList(getAliases#1)
    //#post(List getAliases()): new ArrayList(getAliases#1) num objects == 1
    //#AliasWrapper.java:79: end of method: List com.dmdirc.actions.wrappers.AliasWrapper.getAliases()
    }
    
    /** {@inheritDoc} */
    @Override
    public void add(final Action action) {
        if (action.getTriggers()[0].equals(CoreActionType.UNKNOWN_COMMAND)) {
    //#AliasWrapper.java:85: method: void com.dmdirc.actions.wrappers.AliasWrapper.add(Action)
    //#AliasWrapper.java:85: ?use of default init
    //#    init'ed(getTriggers(...).length)
    //#    severity: LOW
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void add(Action)
    //#    basic block: Entry_BB_1
    //#    assertion: init'ed(getTriggers(...).length)
    //#    VN: getTriggers(...).length
    //#    Expected: {-Inf..+Inf}
    //#    Bad: {Invalid}
    //#    Attribs:  Int  Bad only invalid
    //#AliasWrapper.java:85: ?use of default init
    //#    init'ed(getTriggers(...)[0])
    //#    severity: SUPPRESSED
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void add(Action)
    //#    basic block: Entry_BB_1
    //#    assertion: init'ed(getTriggers(...)[0])
    //#    VN: getTriggers(...)[0]
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    //#AliasWrapper.java:85: ?null dereference
    //#    getTriggers(...)[0] != null
    //#    severity: MEDIUM
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void add(Action)
    //#    basic block: Entry_BB_1
    //#    assertion: getTriggers(...)[0] != null
    //#    VN: getTriggers(...)[0]
    //#    Expected: Inverse{null} or Invalid
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#input(void add(Action)): "Invalid alias action (no name): "._tainted
    //#input(void add(Action)): "Invalid alias action (wrong trigger): "._tainted
    //#input(void add(Action)): action
    //#input(void add(Action)): action.__Tag
    //#input(void add(Action)): action.conditions
    //#input(void add(Action)): action.name
    //#input(void add(Action)): action.name._tainted
    //#input(void add(Action)): action.triggers
    //#input(void add(Action)): action.triggers.length
    //#input(void add(Action)): action.triggers[0]
    //#input(void add(Action)): action.triggers[1..+Inf]
    //#input(void add(Action)): com.dmdirc.logger.ErrorLevel.MEDIUM
    //#input(void add(Action)): com.dmdirc.ui.input.TabCompletionType.COMMAND
    //#input(void add(Action)): com/dmdirc/GlobalWindow.__Descendant_Table[com/dmdirc/GlobalWindow]
    //#input(void add(Action)): com/dmdirc/GlobalWindow.__Descendant_Table[others]
    //#input(void add(Action)): com/dmdirc/GlobalWindow.__Dispatch_Table.getTabCompleter()Lcom/dmdirc/ui/input/TabCompleter;
    //#input(void add(Action)): com/dmdirc/GlobalWindow.globalWindow
    //#input(void add(Action)): com/dmdirc/GlobalWindow.globalWindow.__Tag
    //#input(void add(Action)): com/dmdirc/GlobalWindow.globalWindow.tabCompleter
    //#input(void add(Action)): com/dmdirc/Server.__Descendant_Table[com/dmdirc/Server]
    //#input(void add(Action)): com/dmdirc/Server.__Descendant_Table[others]
    //#input(void add(Action)): com/dmdirc/Server.__Dispatch_Table.getTabCompleter()Lcom/dmdirc/ui/input/TabCompleter;
    //#input(void add(Action)): com/dmdirc/ServerManager.__Class_Obj.__Lock
    //#input(void add(Action)): com/dmdirc/ServerManager.me
    //#input(void add(Action)): com/dmdirc/ServerManager.me.servers
    //#input(void add(Action)): com/dmdirc/actions/Action.__Descendant_Table[com/dmdirc/actions/Action]
    //#input(void add(Action)): com/dmdirc/actions/Action.__Descendant_Table[others]
    //#input(void add(Action)): com/dmdirc/actions/Action.__Dispatch_Table.getConditions()Ljava/util/List;
    //#input(void add(Action)): com/dmdirc/actions/Action.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void add(Action)): com/dmdirc/actions/Action.__Dispatch_Table.getTriggers()[Lcom/dmdirc/actions/interfaces/ActionType;
    //#input(void add(Action)): com/dmdirc/actions/ActionCondition.__Descendant_Table[com/dmdirc/actions/ActionCondition]
    //#input(void add(Action)): com/dmdirc/actions/ActionCondition.__Descendant_Table[others]
    //#input(void add(Action)): com/dmdirc/actions/ActionCondition.__Dispatch_Table.getArg()I
    //#input(void add(Action)): com/dmdirc/actions/ActionCondition.__Dispatch_Table.getTarget()Ljava/lang/String;
    //#input(void add(Action)): com/dmdirc/actions/CoreActionType.UNKNOWN_COMMAND
    //#input(void add(Action)): this
    //#input(void add(Action)): this.actions
    //#input(void add(Action)): this.aliases
    //#output(void add(Action)): com/dmdirc/ServerManager.me
    //#output(void add(Action)): new ArrayList(ServerManager#1) num objects
    //#output(void add(Action)): new ServerManager(getServerManager#1) num objects
    //#output(void add(Action)): new ServerManager(getServerManager#1).__Tag
    //#output(void add(Action)): new ServerManager(getServerManager#1).servers
    //#new obj(void add(Action)): new ArrayList(ServerManager#1)
    //#new obj(void add(Action)): new ServerManager(getServerManager#1)
    //#pre[1] (void add(Action)): action != null
    //#pre[2] (void add(Action)): action.__Tag == com/dmdirc/actions/Action
    //#pre[6] (void add(Action)): action.triggers != null
    //#pre[7] (void add(Action)): action.triggers.length >= 1
    //#pre[3] (void add(Action)): (soft) action.conditions != null
    //#pre[4] (void add(Action)): (soft) init'ed(action.name)
    //#pre[8] (void add(Action)): (soft) action.triggers[0] != null
    //#pre[9] (void add(Action)): (soft) action.triggers[1..+Inf] != null
    //#pre[10] (void add(Action)): (soft) init'ed(com/dmdirc/GlobalWindow.globalWindow)
    //#pre[11] (void add(Action)): (soft) com/dmdirc/GlobalWindow.globalWindow.__Tag == com/dmdirc/GlobalWindow
    //#pre[12] (void add(Action)): (soft) com/dmdirc/GlobalWindow.globalWindow.tabCompleter != null
    //#pre[13] (void add(Action)): (soft) init'ed(com/dmdirc/ServerManager.me)
    //#pre[15] (void add(Action)): (soft) this.actions != null
    //#pre[16] (void add(Action)): (soft) this.aliases != null
    //#presumption(void add(Action)): init'ed(com.dmdirc.logger.ErrorLevel.MEDIUM)
    //#presumption(void add(Action)): init'ed(com.dmdirc.ui.input.TabCompletionType.COMMAND)
    //#presumption(void add(Action)): java.util.Iterator:next(...).__Tag@98 == com/dmdirc/Server
    //#presumption(void add(Action)): java.util.Iterator:next(...)@98 != null
    //#presumption(void add(Action)): server.tabCompleter@98 != null
    //#post(void add(Action)): com/dmdirc/ServerManager.me == One-of{old com/dmdirc/ServerManager.me, &new ServerManager(getServerManager#1)}
    //#post(void add(Action)): init'ed(com/dmdirc/ServerManager.me)
    //#post(void add(Action)): new ArrayList(ServerManager#1) num objects <= 1
    //#post(void add(Action)): new ServerManager(getServerManager#1) num objects <= 1
    //#post(void add(Action)): init'ed(new ServerManager(getServerManager#1).__Tag)
    //#post(void add(Action)): init'ed(new ServerManager(getServerManager#1).servers)
    //#unanalyzed(void add(Action)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(void add(Action)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void add(Action)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void add(Action)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void add(Action)): Effects-of-calling:getConditions
    //#unanalyzed(void add(Action)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void add(Action)): Effects-of-calling:com.dmdirc.commandparser.CommandManager:getCommandChar
    //#unanalyzed(void add(Action)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void add(Action)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void add(Action)): Effects-of-calling:java.util.List:add
    //#test_vector(void add(Action)): com/dmdirc/GlobalWindow.globalWindow: Addr_Set{null}, Inverse{null}
    //#test_vector(void add(Action)): java.lang.Object:equals(...)@85: {0}, {1}
            
            final String commandName = getCommandName(action);

            if (commandName != null) {
                super.add(action);
                aliases.add(commandName);

                if (GlobalWindow.getGlobalWindow() != null) {
                    GlobalWindow.getGlobalWindow().getTabCompleter()
    //#AliasWrapper.java:94: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.ui.input.TabCompleter:addEntry(TabCompletionType, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void add(Action)
    //#    unanalyzed callee: void com.dmdirc.ui.input.TabCompleter:addEntry(TabCompletionType, String)
                            .addEntry(TabCompletionType.COMMAND, commandName);
                }

                for (Server server : ServerManager.getServerManager().getServers()) {
                    server.getTabCompleter().addEntry(TabCompletionType.COMMAND, commandName);
    //#AliasWrapper.java:99: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.ui.input.TabCompleter:addEntry(TabCompletionType, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void add(Action)
    //#    unanalyzed callee: void com.dmdirc.ui.input.TabCompleter:addEntry(TabCompletionType, String)
                }
            } else {
                Logger.userError(ErrorLevel.MEDIUM, "Invalid alias action (no name): "
    //#AliasWrapper.java:102: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.logger.Logger:userError(ErrorLevel, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void add(Action)
    //#    unanalyzed callee: void com.dmdirc.logger.Logger:userError(ErrorLevel, String)
                        + action.getName());
            }
        } else {
            Logger.userError(ErrorLevel.MEDIUM, "Invalid alias action (wrong trigger): "
    //#AliasWrapper.java:106: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.logger.Logger:userError(ErrorLevel, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void add(Action)
    //#    unanalyzed callee: void com.dmdirc.logger.Logger:userError(ErrorLevel, String)
                    + action.getName());
        }
    }
    //#AliasWrapper.java:109: end of method: void com.dmdirc.actions.wrappers.AliasWrapper.add(Action)
    
    /** {@inheritDoc} */
    @Override
    public void remove(final Action action) {
        if (action.getTriggers()[0].equals(CoreActionType.UNKNOWN_COMMAND)) {
    //#AliasWrapper.java:114: method: void com.dmdirc.actions.wrappers.AliasWrapper.remove(Action)
    //#AliasWrapper.java:114: ?use of default init
    //#    init'ed(getTriggers(...).length)
    //#    severity: LOW
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void remove(Action)
    //#    basic block: Entry_BB_1
    //#    assertion: init'ed(getTriggers(...).length)
    //#    VN: getTriggers(...).length
    //#    Expected: {-Inf..+Inf}
    //#    Bad: {Invalid}
    //#    Attribs:  Int  Bad only invalid
    //#AliasWrapper.java:114: ?use of default init
    //#    init'ed(getTriggers(...)[0])
    //#    severity: SUPPRESSED
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void remove(Action)
    //#    basic block: Entry_BB_1
    //#    assertion: init'ed(getTriggers(...)[0])
    //#    VN: getTriggers(...)[0]
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    //#AliasWrapper.java:114: ?null dereference
    //#    getTriggers(...)[0] != null
    //#    severity: MEDIUM
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void remove(Action)
    //#    basic block: Entry_BB_1
    //#    assertion: getTriggers(...)[0] != null
    //#    VN: getTriggers(...)[0]
    //#    Expected: Inverse{null} or Invalid
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#input(void remove(Action)): action
    //#input(void remove(Action)): action.__Tag
    //#input(void remove(Action)): action.conditions
    //#input(void remove(Action)): action.triggers
    //#input(void remove(Action)): action.triggers.length
    //#input(void remove(Action)): action.triggers[0]
    //#input(void remove(Action)): action.triggers[1..+Inf]
    //#input(void remove(Action)): com.dmdirc.ui.input.TabCompletionType.COMMAND
    //#input(void remove(Action)): com/dmdirc/Server.__Descendant_Table[com/dmdirc/Server]
    //#input(void remove(Action)): com/dmdirc/Server.__Descendant_Table[others]
    //#input(void remove(Action)): com/dmdirc/Server.__Dispatch_Table.getTabCompleter()Lcom/dmdirc/ui/input/TabCompleter;
    //#input(void remove(Action)): com/dmdirc/ServerManager.__Class_Obj.__Lock
    //#input(void remove(Action)): com/dmdirc/ServerManager.me
    //#input(void remove(Action)): com/dmdirc/ServerManager.me.servers
    //#input(void remove(Action)): com/dmdirc/actions/Action.__Descendant_Table[com/dmdirc/actions/Action]
    //#input(void remove(Action)): com/dmdirc/actions/Action.__Descendant_Table[others]
    //#input(void remove(Action)): com/dmdirc/actions/Action.__Dispatch_Table.getConditions()Ljava/util/List;
    //#input(void remove(Action)): com/dmdirc/actions/Action.__Dispatch_Table.getTriggers()[Lcom/dmdirc/actions/interfaces/ActionType;
    //#input(void remove(Action)): com/dmdirc/actions/ActionCondition.__Descendant_Table[com/dmdirc/actions/ActionCondition]
    //#input(void remove(Action)): com/dmdirc/actions/ActionCondition.__Descendant_Table[others]
    //#input(void remove(Action)): com/dmdirc/actions/ActionCondition.__Dispatch_Table.getArg()I
    //#input(void remove(Action)): com/dmdirc/actions/ActionCondition.__Dispatch_Table.getTarget()Ljava/lang/String;
    //#input(void remove(Action)): com/dmdirc/actions/CoreActionType.UNKNOWN_COMMAND
    //#input(void remove(Action)): this
    //#input(void remove(Action)): this.actions
    //#input(void remove(Action)): this.aliases
    //#output(void remove(Action)): com/dmdirc/ServerManager.me
    //#output(void remove(Action)): new ArrayList(ServerManager#1) num objects
    //#output(void remove(Action)): new ServerManager(getServerManager#1) num objects
    //#output(void remove(Action)): new ServerManager(getServerManager#1).__Tag
    //#output(void remove(Action)): new ServerManager(getServerManager#1).servers
    //#new obj(void remove(Action)): new ArrayList(ServerManager#1)
    //#new obj(void remove(Action)): new ServerManager(getServerManager#1)
    //#pre[1] (void remove(Action)): action != null
    //#pre[2] (void remove(Action)): action.__Tag == com/dmdirc/actions/Action
    //#pre[4] (void remove(Action)): action.triggers != null
    //#pre[5] (void remove(Action)): action.triggers.length >= 1
    //#pre[3] (void remove(Action)): (soft) action.conditions != null
    //#pre[6] (void remove(Action)): (soft) action.triggers[0] != null
    //#pre[7] (void remove(Action)): (soft) action.triggers[1..+Inf] != null
    //#pre[8] (void remove(Action)): (soft) init'ed(com/dmdirc/ServerManager.me)
    //#pre[10] (void remove(Action)): (soft) this.actions != null
    //#pre[11] (void remove(Action)): (soft) this.aliases != null
    //#presumption(void remove(Action)): init'ed(com.dmdirc.ui.input.TabCompletionType.COMMAND)
    //#presumption(void remove(Action)): java.util.Iterator:next(...).__Tag@121 == com/dmdirc/Server
    //#presumption(void remove(Action)): java.util.Iterator:next(...)@121 != null
    //#presumption(void remove(Action)): server.tabCompleter@121 != null
    //#post(void remove(Action)): com/dmdirc/ServerManager.me == One-of{old com/dmdirc/ServerManager.me, &new ServerManager(getServerManager#1)}
    //#post(void remove(Action)): init'ed(com/dmdirc/ServerManager.me)
    //#post(void remove(Action)): new ArrayList(ServerManager#1) num objects <= 1
    //#post(void remove(Action)): new ServerManager(getServerManager#1) num objects <= 1
    //#post(void remove(Action)): init'ed(new ServerManager(getServerManager#1).__Tag)
    //#post(void remove(Action)): init'ed(new ServerManager(getServerManager#1).servers)
    //#unanalyzed(void remove(Action)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(void remove(Action)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void remove(Action)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void remove(Action)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void remove(Action)): Effects-of-calling:getConditions
    //#unanalyzed(void remove(Action)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void remove(Action)): Effects-of-calling:com.dmdirc.commandparser.CommandManager:getCommandChar
    //#unanalyzed(void remove(Action)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void remove(Action)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void remove(Action)): Effects-of-calling:java.util.List:remove
    //#test_vector(void remove(Action)): java.lang.Object:equals(...)@114: {0}, {1}
    //#test_vector(void remove(Action)): java.util.Iterator:hasNext(...)@121: {0}, {1}
            super.remove(action);
            
            final String commandName = getCommandName(action);
            
            aliases.remove(commandName);
            
            for (Server server : ServerManager.getServerManager().getServers()) {
                server.getTabCompleter().removeEntry(TabCompletionType.COMMAND, commandName);
    //#AliasWrapper.java:122: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.ui.input.TabCompleter:removeEntry(TabCompletionType, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: void remove(Action)
    //#    unanalyzed callee: void com.dmdirc.ui.input.TabCompleter:removeEntry(TabCompletionType, String)
            }
        }
    }
    //#AliasWrapper.java:125: end of method: void com.dmdirc.actions.wrappers.AliasWrapper.remove(Action)
    
    /**
     * Retrieves the command name of the specified alias action.
     *
     * @param action The action whose name is to be determined
     * @return The command name for the specified alias, or null if it has
     *         no appropriate conditions.
     */
    public static String getCommandName(final Action action) {
        for (ActionCondition condition : action.getConditions()) {
    //#AliasWrapper.java:135: method: String com.dmdirc.actions.wrappers.AliasWrapper.getCommandName(Action)
    //#input(String getCommandName(Action)): action
    //#input(String getCommandName(Action)): action.__Tag
    //#input(String getCommandName(Action)): action.conditions
    //#input(String getCommandName(Action)): com/dmdirc/actions/Action.__Descendant_Table[com/dmdirc/actions/Action]
    //#input(String getCommandName(Action)): com/dmdirc/actions/Action.__Descendant_Table[others]
    //#input(String getCommandName(Action)): com/dmdirc/actions/Action.__Dispatch_Table.getConditions()Ljava/util/List;
    //#input(String getCommandName(Action)): com/dmdirc/actions/ActionCondition.__Descendant_Table[com/dmdirc/actions/ActionCondition]
    //#input(String getCommandName(Action)): com/dmdirc/actions/ActionCondition.__Descendant_Table[others]
    //#input(String getCommandName(Action)): com/dmdirc/actions/ActionCondition.__Dispatch_Table.getArg()I
    //#input(String getCommandName(Action)): com/dmdirc/actions/ActionCondition.__Dispatch_Table.getTarget()Ljava/lang/String;
    //#output(String getCommandName(Action)): java.lang.StringBuilder:toString(...)._tainted
    //#output(String getCommandName(Action)): return_value
    //#new obj(String getCommandName(Action)): java.lang.StringBuilder:toString(...)
    //#pre[1] (String getCommandName(Action)): action != null
    //#pre[2] (String getCommandName(Action)): action.__Tag == com/dmdirc/actions/Action
    //#pre[3] (String getCommandName(Action)): action.conditions != null
    //#presumption(String getCommandName(Action)): java.util.Iterator:next(...).__Tag@135 == com/dmdirc/actions/ActionCondition
    //#presumption(String getCommandName(Action)): java.util.Iterator:next(...)@135 != null
    //#post(String getCommandName(Action)): java.lang.StringBuilder:toString(...)._tainted == 0
    //#post(String getCommandName(Action)): return_value in Addr_Set{null,&java.lang.StringBuilder:toString(...)}
    //#test_vector(String getCommandName(Action)): condition.arg@135: {-2_147_483_648..0, 2..4_294_967_295}, {1}
    //#test_vector(String getCommandName(Action)): java.util.Iterator:hasNext(...)@135: {0}, {1}
            if (condition.getArg() == 1) {
                return CommandManager.getCommandChar() + condition.getTarget();
    //#AliasWrapper.java:137: Warning: method not available - call not analyzed
    //#    call on char com.dmdirc.commandparser.CommandManager:getCommandChar()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.actions.wrappers.AliasWrapper
    //#    method: String getCommandName(Action)
    //#    unanalyzed callee: char com.dmdirc.commandparser.CommandManager:getCommandChar()
            }
        }
        
        // How can we have an alias without a command name?
        return null;
    //#AliasWrapper.java:142: end of method: String com.dmdirc.actions.wrappers.AliasWrapper.getCommandName(Action)
    }

    /** {@inheritDoc} */
    @Override
    public boolean isDelible() {
        return false;
    //#AliasWrapper.java:148: method: bool com.dmdirc.actions.wrappers.AliasWrapper.isDelible()
    //#output(bool isDelible()): return_value
    //#post(bool isDelible()): return_value == 0
    //#AliasWrapper.java:148: end of method: bool com.dmdirc.actions.wrappers.AliasWrapper.isDelible()
    }

    /** {@inheritDoc} */
    @Override
    public String getDescription() {
        return "Aliases allow you to create new commands that invoke one or "
    //#AliasWrapper.java:154: method: String com.dmdirc.actions.wrappers.AliasWrapper.getDescription()
    //#output(String getDescription()): return_value
    //#post(String getDescription()): return_value == &"Aliases allow you to create new commands that invoke one or more other ... anage aliases using the "Alias Manager", located in the Settings menu."
    //#AliasWrapper.java:154: end of method: String com.dmdirc.actions.wrappers.AliasWrapper.getDescription()
                + "more other commands. You can manage aliases using the \""
                + "Alias Manager\", located in the Settings menu.";
    }
    
}
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Descendant_Table[com/dmdirc/actions/wrappers/AliasWrapper]
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.add(Lcom/dmdirc/actions/Action;)V
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.clear()V
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.contains(Lcom/dmdirc/actions/Action;)Z
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.get(I)Lcom/dmdirc/actions/Action;
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getActions()Ljava/util/List;
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getAliases()Ljava/util/List;
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getAuthor()Ljava/lang/String;
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getComponent()I
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getDescription()Ljava/lang/String;
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getName()Ljava/lang/String;
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getSettings()Ljava/util/Map;
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getVersion()I
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.isDelible()Z
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.iterator()Ljava/util/Iterator;
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.remove(Lcom/dmdirc/actions/Action;)V
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.setAuthor(Ljava/lang/String;)V
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.setComponent(I)V
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.setDescription(Ljava/lang/String;)V
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.setVersion(I)V
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.size()I
    //#output(com.dmdirc.actions.wrappers.AliasWrapper__static_init): com/dmdirc/actions/ActionGroup.__Descendant_Table[com/dmdirc/actions/wrappers/AliasWrapper]
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Descendant_Table[com/dmdirc/actions/wrappers/AliasWrapper] == &__Dispatch_Table
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): com/dmdirc/actions/ActionGroup.__Descendant_Table[com/dmdirc/actions/wrappers/AliasWrapper] == &__Dispatch_Table
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.add(Lcom/dmdirc/actions/Action;)V == &add
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.clear()V == &com/dmdirc/actions/ActionGroup.clear
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.contains(Lcom/dmdirc/actions/Action;)Z == &com/dmdirc/actions/ActionGroup.contains
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.get(I)Lcom/dmdirc/actions/Action; == &com/dmdirc/actions/ActionGroup.get
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getActions()Ljava/util/List; == &com/dmdirc/actions/ActionGroup.getActions
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getAliases()Ljava/util/List; == &getAliases
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getAuthor()Ljava/lang/String; == &com/dmdirc/actions/ActionGroup.getAuthor
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getComponent()I == &com/dmdirc/actions/ActionGroup.getComponent
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getDescription()Ljava/lang/String; == &getDescription
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getName()Ljava/lang/String; == &com/dmdirc/actions/ActionGroup.getName
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getSettings()Ljava/util/Map; == &com/dmdirc/actions/ActionGroup.getSettings
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.getVersion()I == &com/dmdirc/actions/ActionGroup.getVersion
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.isDelible()Z == &isDelible
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.iterator()Ljava/util/Iterator; == &com/dmdirc/actions/ActionGroup.iterator
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.remove(Lcom/dmdirc/actions/Action;)V == &remove
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.setAuthor(Ljava/lang/String;)V == &com/dmdirc/actions/ActionGroup.setAuthor
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.setComponent(I)V == &com/dmdirc/actions/ActionGroup.setComponent
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.setDescription(Ljava/lang/String;)V == &com/dmdirc/actions/ActionGroup.setDescription
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.setVersion(I)V == &com/dmdirc/actions/ActionGroup.setVersion
    //#post(com.dmdirc.actions.wrappers.AliasWrapper__static_init): __Dispatch_Table.size()I == &com/dmdirc/actions/ActionGroup.size
    //#AliasWrapper.java:: end of method: com.dmdirc.actions.wrappers.AliasWrapper.com.dmdirc.actions.wrappers.AliasWrapper__static_init
    //#AliasWrapper.java:: end of class: com.dmdirc.actions.wrappers.AliasWrapper
