Action.java

Action.java

current inspection = 2009-09-03 21:56:13 (id #1)

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void checkMetaData()

Kind	Annotation Text
pre	(soft) init'ed(this.group)
pre	this.config != null
presumption	com.dmdirc.util.ConfigFile:getKeyDomain(...)@215 != null
presumption	com.dmdirc.util.ConfigFile:getKeyDomain(...)@244 != null
presumption	java.util.Map:get(...)@309 != null
presumption	myGroup.settings != null
unanalyzed	call on com.dmdirc.config.Identity:setOption
unanalyzed	call on com.dmdirc.config.IdentityManager:getAddonI dentity
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
test_vector	com.dmdirc.util.ConfigFile:isKeyDomain(...)@213: {0}, {1}
test_vector	com.dmdirc.util.ConfigFile:isKeyDomain(...)@242: {0}, {1}
test_vector	java.util.Map:containsKey(...)@217: {0}, {1}
test_vector	java.util.Map:containsKey(...)@221: {0}, {1}
test_vector	java.util.Map:containsKey(...)@225: {0}, {1}
test_vector	java.util.Map:containsKey(...)@233: {0}, {1}
test_vector	java.util.Map:containsKey(...)@246: {0}, {1}

void com.dmdirc.actions.Action(String, String)

Kind	Annotation Text
pre	init'ed(com/dmdirc/Main.configdir)
presumption	init'ed(com.dmdirc.logger.ErrorLevel.HIGH)
presumption	init'ed(com.dmdirc.logger.ErrorLevel.MEDIUM)
presumption	init'ed(java.io.File.separator)
post	com/dmdirc/Main.configdir != null
post	com/dmdirc/Main.configdir == One-of{old com/dmdirc/Main.configdir, &java.lang. StringBuilder:toString(...)}
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	init'ed(this.config)
post	init'ed(this.group)
post	init'ed(this.name)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	new ArrayList(ActionModel#1) num objects == 1
post	new ConfigFile(Action#2) num objects <= 1
post	this.conditions == &new ArrayList(ActionModel#1 )
post	this.group == group
post	this.location == &java.lang.StringBuilder:toStr ing(...)
post	this.name == name
unanalyzed	call on getConfigDir
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.System:getProperty
unanalyzed	call on java.lang.System:getenv
unanalyzed	call on java.util.ArrayList

void com.dmdirc.actions.Action(String, String, ActionType[], String[], List, ConditionTree, String)

Kind	Annotation Text
pre	(soft) com.dmdirc.actions.CoreActionType__static_ init.new CoreActionType(CoreActionType__static_init #71).type != null
pre	(soft) conditions init'ed
pre	(soft) init'ed(com/dmdirc/ServerManager.me)
pre	(soft) init'ed(response[...])
pre	(soft) init'ed(triggers[...])
pre	(soft) triggers.length <= 2³²-1
pre	init'ed(com/dmdirc/Main.configdir)
pre	init'ed(com/dmdirc/actions/ActionManager. killSwitch)
pre	response != null
pre	triggers != null
presumption	init'ed(java.io.File.separator)
post	com/dmdirc/Main.configdir != null
post	com/dmdirc/Main.configdir == One-of{old com/dmdirc/Main.configdir, &java.lang. StringBuilder:toString(...)}
post	init'ed(com/dmdirc/ServerManager.me)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	init'ed(new ActionType[](ActionModel#2)[0])
post	init'ed(new ServerManager(getServerManager#1). servers)
post	init'ed(new String[](ActionModel#3).length)
post	init'ed(this.conditionTree)
post	init'ed(this.conditions)
post	init'ed(this.config)
post	init'ed(this.group)
post	init'ed(this.name)
post	init'ed(this.newFormat)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	new ActionType[](ActionModel#2) num objects == 1
post	new ActionType[](ActionModel#2).length <= 2³²-1
post	new ActionType[](ActionModel#2).length == triggers.length
post	new ActionType[](ActionModel#2)[0] == One-of{triggers[...], undefined}
post	new ActionType[](ActionModel#2)[...] == One-of{triggers[...], undefined}
post	new ArrayList(ActionModel#1) num objects == 1
post	new ArrayList(ServerManager#1) num objects <= 1
post	new ArrayList(ServerManager#1) num objects == 0, if init'ed
post	new ArrayList(ServerManager#1) num objects == undefined
post	new ServerManager(getServerManager#1) num objects <= 1
post	new ServerManager(getServerManager#1) num objects == new ArrayList(ServerManager#1) num objects
post	new ServerManager(getServerManager#1).servers == null
post	new ServerManager(getServerManager#1).servers == undefined
post	new String[](ActionModel#3) num objects == 1
post	new String[](ActionModel#3).length == response.length
post	new String[](ActionModel#3)[...] == One-of{response[...], undefined}
post	this.conditionTree == conditionTree
post	this.conditions == conditions
post	this.group == group
post	this.location == &java.lang.StringBuilder:toStr ing(...)
post	this.modified == 1
post	this.name == name
post	this.newFormat == newFormat
post	this.response == &new String[](ActionModel#3)
post	this.triggers == &new ActionType[](ActionModel# 2)
unanalyzed	call on [Ljava.lang.String;:instanceof
unanalyzed	call on add
unanalyzed	call on com.dmdirc.ServerState:equals
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on com.dmdirc.commandparser.CommandManager:get CommandChar
unanalyzed	call on com.dmdirc.commandparser.parsers. CommandParser:parseCommand
unanalyzed	call on com.dmdirc.commandparser.parsers. GlobalCommandParser:getGlobalCommandParser
unanalyzed	call on com.dmdirc.config.ConfigManager:getOptions
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.interfaces.ActionListener:proces sEvent
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.ui.input.TabCompleter:addEntry
unanalyzed	call on com.dmdirc.ui.interfaces.InputWindow:getCom mandParser
unanalyzed	call on com.dmdirc.ui.interfaces.InputWindow:instan ceof
unanalyzed	call on com.dmdirc.ui.interfaces.UIController:getAc tiveWindow
unanalyzed	call on com.dmdirc.util.MapList:add
unanalyzed	call on com.dmdirc.util.MapList:containsKey
unanalyzed	call on com.dmdirc.util.MapList:get
unanalyzed	call on doComponentSubstitutions
unanalyzed	call on doServerSubstitutions
unanalyzed	call on evaluate
unanalyzed	call on get
unanalyzed	call on getArgTypes
unanalyzed	call on getArity
unanalyzed	call on getCompatibleComponents
unanalyzed	call on getConditions
unanalyzed	call on getConfigDir
unanalyzed	call on getFrame
unanalyzed	call on getGlobalWindow
unanalyzed	call on getGroup
unanalyzed	call on getName
unanalyzed	call on getServer
unanalyzed	call on getState
unanalyzed	call on getTabCompleter
unanalyzed	call on getTriggers
unanalyzed	call on getType
unanalyzed	call on getUI
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on java.lang.Object:toString
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:instanceof
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.System:getProperty
unanalyzed	call on java.lang.System:getenv
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:size
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on parseStack
unanalyzed	call on readTerm
unanalyzed	call on test
unanalyzed	call on trigger
unanalyzed	call on triggerActions

void com.dmdirc.actions.Action(String, String, ActionType[], String[], List, String)

Kind	Annotation Text
pre	(soft) init'ed(com/dmdirc/ServerManager.me)
pre	conditions != null
post	com/dmdirc/ServerManager.me == old com/dmdirc/Serve rManager.me
post	init'ed(new ConditionTree(readTerm#1) num objects)
post	init'ed(this.conditionTree)
post	init'ed(this.conditions)
post	init'ed(this.config)
post	init'ed(this.group)
post	init'ed(this.location)
post	init'ed(this.modified)
post	init'ed(this.name)
post	init'ed(this.newFormat)
post	init'ed(this.response)
post	init'ed(this.triggers)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	new ActionType[](ActionModel#2) num objects == 0, if init'ed
post	new ActionType[](ActionModel#2) num objects == undefined
post	new ActionType[](ActionModel#2).length == new ActionType[](ActionModel#2) num objects
post	new ActionType[](ActionModel#2)[...] == null
post	new ActionType[](ActionModel#2)[...] == undefined
post	new ArrayList(ActionModel#1) num objects == new ActionType[](ActionModel#2) num objects
post	new ArrayList(ServerManager#1) num objects == new ActionType[](ActionModel#2) num objects
post	new ConditionTree(parseStack#3) num objects <= 1
post	new ConditionTree(parseStack#3).argument == -1
post	new ConditionTree(parseStack#3).leftArg == null
post	new ConditionTree(parseStack#3).op == &com.dmdirc.actions.ConditionTree$OPERATION__ static_init.new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#5)
post	new ConditionTree(parseStack#3).rightArg == null
post	new ConditionTree(readTerm#1)._tainted == 0
post	new ConditionTree(readTerm#1).argument == 0, if init'ed
post	new ConditionTree(readTerm#1).leftArg == null
post	new ConditionTree(readTerm#1).op == null
post	new ConditionTree(readTerm#1).rightArg == null
post	new ServerManager(getServerManager#1) num objects == new ActionType[](ActionModel#2) num objects
post	new ServerManager(getServerManager#1).servers == new ActionType[](ActionModel#2)[...]
post	new String[](ActionModel#3) num objects == new ActionType[](ActionModel#2) num objects
post	new String[](ActionModel#3).length == new ActionType[](ActionModel#2) num objects
post	new String[](ActionModel#3)[...] == new ActionType[](ActionModel#2)[...]
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:size
unanalyzed	call on parseStack
unanalyzed	call on readTerm

com.dmdirc.actions.Action__static_init

Kind	Annotation Text
post	DOMAIN_CONDITIONTREE != null
post	DOMAIN_FORMAT != null
post	DOMAIN_METADATA != null
post	DOMAIN_RESPONSE != null
post	DOMAIN_TRIGGERS != null

void delete()

Kind	Annotation Text
pre	(soft) com.dmdirc.actions.CoreActionType__static_ init.new CoreActionType(CoreActionType__static_init #73).type != null
pre	(soft) init'ed(com/dmdirc/ServerManager.me)
pre	init'ed(com/dmdirc/actions/ActionManager. killSwitch)
pre	init'ed(this.group)
pre	init'ed(this.location)
pre	init'ed(this.name)
post	com/dmdirc/ServerManager.me == old com/dmdirc/Serve rManager.me
post	new ArrayList(ServerManager#1) num objects == 0, if init'ed
post	new ArrayList(ServerManager#1) num objects == undefined
post	new ServerManager(getServerManager#1) num objects == new ArrayList(ServerManager#1) num objects
post	new ServerManager(getServerManager#1).servers == null
post	new ServerManager(getServerManager#1).servers == undefined
unanalyzed	call on [Ljava.lang.String;:instanceof
unanalyzed	call on com.dmdirc.ServerState:equals
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on com.dmdirc.commandparser.parsers. CommandParser:parseCommand
unanalyzed	call on com.dmdirc.commandparser.parsers. GlobalCommandParser:getGlobalCommandParser
unanalyzed	call on com.dmdirc.config.ConfigManager:getOptions
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.interfaces.ActionListener:proces sEvent
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on com.dmdirc.ui.interfaces.InputWindow:getCom mandParser
unanalyzed	call on com.dmdirc.ui.interfaces.InputWindow:instan ceof
unanalyzed	call on com.dmdirc.ui.interfaces.UIController:getAc tiveWindow
unanalyzed	call on com.dmdirc.util.MapList:containsKey
unanalyzed	call on com.dmdirc.util.MapList:get
unanalyzed	call on doComponentSubstitutions
unanalyzed	call on doServerSubstitutions
unanalyzed	call on evaluate
unanalyzed	call on get
unanalyzed	call on getArgTypes
unanalyzed	call on getArity
unanalyzed	call on getCompatibleComponents
unanalyzed	call on getFrame
unanalyzed	call on getServer
unanalyzed	call on getState
unanalyzed	call on getType
unanalyzed	call on getUI
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Object:toString
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:instanceof
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on parseStack
unanalyzed	call on readTerm
unanalyzed	call on test
unanalyzed	call on trigger
unanalyzed	call on triggerActions

void error(String)

Kind	Annotation Text
pre	init'ed(this.group)
pre	init'ed(this.name)
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)

void loadActionFromConfig()

Kind	Annotation Text
pre	(soft) init'ed(com/dmdirc/ServerManager.me)
pre	(soft) init'ed(this.group)
pre	(soft) init'ed(this.name)
pre	(soft) init'ed(this.triggers[0])
pre	(soft) init'ed(this.triggers[...])
pre	(soft) this.conditions != null
pre	this.config != null
presumption	com.dmdirc.util.ConfigFile:getFlatDomain(...)@154 != null
presumption	com.dmdirc.util.ConfigFile:getFlatDomain(...)@163 != null
presumption	com.dmdirc.util.ConfigFile:getFlatDomain(...)@166 != null
presumption	com.dmdirc.util.ConfigFile:getFlatDomain(...)@175 != null
presumption	com.dmdirc.util.ConfigFile:getFlatDomain(...)@185 != null
presumption	com.dmdirc.util.ConfigFile:getFlatDomain(...)@187 != null
presumption	com.dmdirc.util.ConfigFile:getKeyDomain(...)@180 != null
presumption	java.util.List:get(...)@187 != null
presumption	java.util.List:size(...)@163 >= 1
presumption	java.util.List:size(...)@264 != 0
presumption	this.conditionTree...leftArg != null
presumption	this.conditionTree...leftArg@195 != null
presumption	this.conditionTree...rightArg != null
presumption	this.conditionTree...rightArg@195 != null
presumption	this.conditionTree.leftArg != null
presumption	this.conditionTree.leftArg@195 != null
presumption	this.conditionTree.rightArg != null
presumption	this.conditionTree.rightArg@195 != null
presumption	this.triggers[0].type != null
post	init'ed(com/dmdirc/ServerManager.me)
post	init'ed(new ActionType[](loadTriggers#1).length)
post	init'ed(new ActionType[](loadTriggers#1)[0])
post	init'ed(new ConditionTree(parseStack#3).argument)
post	init'ed(new ConditionTree(parseStack#3).leftArg)
post	init'ed(new ConditionTree(parseStack#3).op)
post	init'ed(new ConditionTree(parseStack#3).rightArg)
post	init'ed(new ConditionTree(readTerm#1) num objects)
post	init'ed(new ServerManager(getServerManager#1). servers)
post	init'ed(new String[](loadActionFromConfig#1). length)
post	init'ed(new String[](loadActionFromConfig#1)[...])
post	init'ed(this.response[...])
post	init'ed(this.triggers[0])
post	init'ed(this.triggers[...])
post	new ActionType[](loadTriggers#1) num objects <= 1
post	new ArrayList(ServerManager#1) num objects <= 1
post	new ConditionTree(parseStack#3) num objects <= 1
post	new ServerManager(getServerManager#1) num objects <= 1
post	new String[](loadActionFromConfig#1) num objects <= 1
post	possibly_updated(new ActionType[](loadTriggers#1)[...])
post	possibly_updated(new ConditionTree(readTerm#1). argument)
post	possibly_updated(new ConditionTree(readTerm#1). leftArg)
post	possibly_updated(new ConditionTree(readTerm#1).op)
post	possibly_updated(new ConditionTree(readTerm#1). rightArg)
post	possibly_updated(this.conditionTree)
post	possibly_updated(this.newFormat)
post	this.response == One-of{old this.response, &new String[](loadActionFromConfig#1)}
post	this.triggers == One-of{&new ActionType[](loadT riggers#1), old this.triggers}
unanalyzed	call on add
unanalyzed	call on appliesTo
unanalyzed	call on com.dmdirc.commandparser.CommandManager:get CommandChar
unanalyzed	call on com.dmdirc.config.Identity:setOption
unanalyzed	call on com.dmdirc.config.IdentityManager:getAddonI dentity
unanalyzed	call on com.dmdirc.config.prefs.PreferencesSetting
unanalyzed	call on com.dmdirc.config.prefs.PreferencesType:val ueOf
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.ui.input.TabCompleter:addEntry
unanalyzed	call on com.dmdirc.util.ConfigFile:getKeyDomain
unanalyzed	call on com.dmdirc.util.ConfigFile:isKeyDomain
unanalyzed	call on com.dmdirc.util.MapList:add
unanalyzed	call on getActionComponent
unanalyzed	call on getArgTypes
unanalyzed	call on getArity
unanalyzed	call on getConditions
unanalyzed	call on getGlobalWindow
unanalyzed	call on getGroup
unanalyzed	call on getMaximumArgument
unanalyzed	call on getName
unanalyzed	call on getTabCompleter
unanalyzed	call on getTriggers
unanalyzed	call on getType
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Class:getName
unanalyzed	call on java.lang.Enum:name
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.IllegalArgumentException:getMessa ge
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Math:max
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:size
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
unanalyzed	call on parseStack
unanalyzed	call on readTerm
test_vector	com.dmdirc.util.ConfigFile:isFlatDomain(...)@153: {0}, {1}
test_vector	com.dmdirc.util.ConfigFile:isFlatDomain(...)@162: {0}, {1}
test_vector	com.dmdirc.util.ConfigFile:isFlatDomain(...)@174: {0}, {1}
test_vector	com.dmdirc.util.ConfigFile:isFlatDomain(...)@185: {0}, {1}
test_vector	com.dmdirc.util.ConfigFile:isKeyDomain(...)@179: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@166: {0}, {1}
test_vector	java.util.List:size(...)@185: {-2³¹..0}, {1..2³²-1}

bool loadTriggers(List)

Kind	Annotation Text
pre	(soft) init'ed(this.group)
pre	(soft) init'ed(this.name)
pre	newTriggers != null
presumption	java.util.List:size(...)@264 >= 0
presumption	this.triggers[i].type != null
post	init'ed(return_value)
post	init'ed(this.triggers[0])
post	new ActionType[](loadTriggers#1) num objects == 1
post	possibly_updated(this.triggers[0])
post	possibly_updated(this.triggers[...])
post	this.triggers == &new ActionType[](loadTriggers #1)
post	this.triggers.length <= 2³²-1
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on java.lang.Enum:name
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.util.List:iterator
test_vector	java.lang.Object:equals(...)@272: {1}, {0}

ActionComponent readComponent(Map, int)

Kind	Annotation Text
pre	(soft) arg >= 0
pre	(soft) init'ed(this.group)
pre	(soft) init'ed(this.name)
pre	(soft) this.triggers != null
pre	(soft) this.triggers.length >= 1
pre	(soft) this.triggers[0] != null
pre	(soft) this.triggers[0].type != null
pre	data != null
presumption	appliesTo(...)@467 != null
presumption	arg < getArgTypes(...).length@454
presumption	arg < getArgTypes(...).length@467
presumption	getArgTypes(...).length@454 >= 1
presumption	getArgTypes(...).length@467 >= 1
presumption	getArgTypes(...)@454 != null
presumption	getArgTypes(...)@467 != null
presumption	getType(...)@454 != getType(...)
presumption	getType(...)@467 != getType(...)
presumption	java.util.Map:get(...)@447 != null
post	init'ed(return_value)
post	new ActionComponentChain(readComponent#1) num objects <= 1
post	new ArrayList(ActionComponentChain#1) num objects <= 1
post	possibly_updated(new ActionComponentChain(readCompo nent#1).components)
unanalyzed	call on appliesTo
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on getActionComponent
unanalyzed	call on getType
unanalyzed	call on java.lang.Class:getName
unanalyzed	call on java.lang.Enum:name
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:iterator
test_vector	java.lang.Object:equals(...)@467: {1}, {0}
test_vector	java.lang.String:indexOf(...)@450: {-2³¹. .-2, 0..2³²-1}, {-1}

bool readCondition(Map)

Kind	Annotation Text
pre	(soft) init'ed(this.group)
pre	(soft) init'ed(this.name)
pre	(soft) this.conditions != null
pre	(soft) this.triggers != null
pre	(soft) this.triggers.length >= 1
pre	(soft) this.triggers[0] != null
pre	(soft) this.triggers[0].type != null
pre	data != null
presumption	appliesTo(...)@414 != null
presumption	getType(...)@385 != getType(...)
presumption	java.util.Map:get(...)@408 != null
post	init'ed(return_value)
unanalyzed	call on appliesTo
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on getActionComponent
unanalyzed	call on getArgTypes
unanalyzed	call on getType
unanalyzed	call on java.lang.Class:getName
unanalyzed	call on java.lang.Enum:name
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.IllegalArgumentException:getMessa ge
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.Map:get
test_vector	java.lang.Integer:parseInt(...)@379: {-2³¹..-2}, {0..2³²-2}, {-1}
test_vector	java.lang.Object:equals(...)@414: {0}, {1}
test_vector	java.lang.Object:equals(...)@414: {1}, {0}
test_vector	java.util.Map:get(...)@393: Inverse{null}, Addr_Set{null}
test_vector	java.util.Map:get(...)@422: Inverse{null}, Addr_Set{null}

void save()

Kind	Annotation Text
pre	(soft) com.dmdirc.actions.CoreActionType__static_ init.new CoreActionType(CoreActionType__static_init #72).type != null
pre	(soft) init'ed(com.dmdirc.actions.ConditionTree$1__ static_init.new int[](ConditionTree$1__static_init# 1)[...])
pre	(soft) init'ed(com/dmdirc/ServerManager.me)
pre	(soft) init'ed(com/dmdirc/actions/ActionManager. killSwitch)
pre	(soft) init'ed(this.conditionTree)
pre	(soft) init'ed(this.conditionTree.argument)
pre	(soft) init'ed(this.conditionTree.leftArg)
pre	(soft) init'ed(this.conditionTree.rightArg)
pre	(soft) init'ed(this.config)
pre	(soft) init'ed(this.group)
pre	(soft) init'ed(this.location)
pre	(soft) init'ed(this.name)
pre	(soft) init'ed(this.newFormat)
pre	(soft) init'ed(this.response[...])
pre	(soft) init'ed(this.triggers[...])
pre	(soft) this.conditionTree.op != null
pre	(soft) this.conditions != null
pre	(soft) this.response != null
pre	(soft) this.response.length <= 2³²-1
pre	(soft) this.triggers != null
pre	(soft) this.triggers.length <= 2³²-1
pre	init'ed(this.modified)
presumption	com.dmdirc.util.ConfigFile:getFlatDomain(...)@314 != null
presumption	com.dmdirc.util.ConfigFile:getFlatDomain(...)@319 != null
presumption	condition.comparison@323 != null
presumption	condition.component@323 != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.HIGH)
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	java.util.Iterator:next(...)@323 != null
post	com/dmdirc/ServerManager.me == old com/dmdirc/Serve rManager.me
post	init'ed(this.modified)
post	new ArrayList(ServerManager#1) num objects == 0, if init'ed
post	new ServerManager(getServerManager#1) num objects == 0, if init'ed
post	new ServerManager(getServerManager#1).servers == null
unanalyzed	call on [Ljava.lang.String;:instanceof
unanalyzed	call on com.dmdirc.ServerState:equals
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on com.dmdirc.commandparser.parsers. CommandParser:parseCommand
unanalyzed	call on com.dmdirc.commandparser.parsers. GlobalCommandParser:getGlobalCommandParser
unanalyzed	call on com.dmdirc.config.ConfigManager:getOptions
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.interfaces.ActionListener:proces sEvent
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on com.dmdirc.ui.interfaces.InputWindow:getCom mandParser
unanalyzed	call on com.dmdirc.ui.interfaces.InputWindow:instan ceof
unanalyzed	call on com.dmdirc.ui.interfaces.UIController:getAc tiveWindow
unanalyzed	call on com.dmdirc.util.MapList:containsKey
unanalyzed	call on com.dmdirc.util.MapList:get
unanalyzed	call on doComponentSubstitutions
unanalyzed	call on doServerSubstitutions
unanalyzed	call on evaluate
unanalyzed	call on get
unanalyzed	call on getArgTypes
unanalyzed	call on getArity
unanalyzed	call on getCompatibleComponents
unanalyzed	call on getFrame
unanalyzed	call on getServer
unanalyzed	call on getState
unanalyzed	call on getType
unanalyzed	call on getUI
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Object:toString
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:instanceof
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on parseStack
unanalyzed	call on readTerm
unanalyzed	call on test
unanalyzed	call on trigger
unanalyzed	call on triggerActions
test_vector	com.dmdirc.util.ConfigFile:isKeyDomain(...)@343: {0}, {1}
test_vector	com.dmdirc.util.ConfigFile:isKeyDomain(...)@347: {0}, {1}
test_vector	condition.arg@323: {-2³¹..-2, 0..2³²-1}, {-1}
test_vector	java.util.Iterator:hasNext(...)@323: {0}, {1}
test_vector	this.conditionTree: Addr_Set{null}, Inverse{null}
test_vector	this.config: Addr_Set{null}, Inverse{null}
test_vector	this.modified: {1}, {0}
test_vector	this.newFormat: Addr_Set{null}, Inverse{null}
test_vector	this.triggers[...]: Inverse{null}, Addr_Set{null}

void setGroup(String)

Kind	Annotation Text
pre	init'ed(com/dmdirc/Main.configdir)
pre	init'ed(this.location)
pre	init'ed(this.name)
presumption	init'ed(java.io.File.separator)
post	com/dmdirc/Main.configdir != null
post	com/dmdirc/Main.configdir == One-of{old com/dmdirc/Main.configdir, &java.lang. StringBuilder:toString(...)}
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	init'ed(this.group)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	this.group == newGroup
post	this.location == &java.lang.StringBuilder:toStr ing(...)
post	this.modified == 1
unanalyzed	call on getConfigDir
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.System:getProperty
unanalyzed	call on java.lang.System:getenv

void setName(String)

Kind	Annotation Text
pre	init'ed(com/dmdirc/Main.configdir)
pre	init'ed(this.group)
pre	init'ed(this.location)
presumption	init'ed(java.io.File.separator)
post	com/dmdirc/Main.configdir != null
post	com/dmdirc/Main.configdir == One-of{old com/dmdirc/Main.configdir, &java.lang. StringBuilder:toString(...)}
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	init'ed(this.name)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	this.location == &java.lang.StringBuilder:toStr ing(...)
post	this.modified == 1
post	this.name == newName
unanalyzed	call on getConfigDir
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.System:getProperty
unanalyzed	call on java.lang.System:getenv

String toString()

Kind	Annotation Text
pre	init'ed(this.conditions)
pre	init'ed(this.group)
pre	init'ed(this.location)
pre	init'ed(this.name)
pre	init'ed(this.newFormat)
pre	init'ed(this.response)
pre	init'ed(this.triggers)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	java.lang.StringBuilder:toString(...)._tainted == this.location._tainted \| this.conditions._tainted \| this.group._tainted \| this.name._tainted \| One-of{this.conditions._tainted \| this.group._ tainted \| this.name._tainted, this.newFormat. _tainted}
post	return_value == &java.lang.StringBuilder:toStri ng(...)
unanalyzed	call on java.util.Arrays:toString