Messages

Last Msg First Msg

method	com.dmdirc.actions.Action__static_init
post	DOMAIN_CONDITIONTREE != null
post	DOMAIN_FORMAT != null
post	DOMAIN_METADATA != null
post	DOMAIN_RESPONSE != null
post	DOMAIN_TRIGGERS != null

method	void com.dmdirc.actions.Action(String, String)
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 == One-of{old com/dmdirc/Main.configdir, &java.lang. StringBuilder:toString(...)}
post	com/dmdirc/Main.configdir != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	this.conditions == &new ArrayList(ActionModel#1 )
post	init'ed(this.config)
post	this.group == group
post	init'ed(this.group)
post	this.location == &java.lang.StringBuilder:toStr ing(...)
post	this.name == name
post	init'ed(this.name)
post	new ArrayList(ActionModel#1) num objects == 1
post	new ConfigFile(Action#2) num objects <= 1
unanalyzed	call on getConfigDir
unanalyzed	call on java.lang.System:getProperty
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.System:getenv

method not available - call not analyzed Info call on void com.dmdirc.util.ConfigFile(String)

method not available - call not analyzed Info call on void com.dmdirc.util.ConfigFile:read()

call too complex - analysis skipped Info call on void loadActionFromConfig()

method not available - call not analyzed Info call on String com.dmdirc.util.InvalidConfigFileExc eption:getMessage()

method not available - call not analyzed Info call on void com.dmdirc.logger.Logger:userError(Err orLevel, String)

method not available - call not analyzed Info call on void com.dmdirc.logger.Logger:userError(Err orLevel, String)

method	void com.dmdirc.actions.Action(String, String, ActionType[], String[], List, String)
pre	conditions != null
pre	(soft) init'ed(com/dmdirc/ServerManager.me)
post	com/dmdirc/ServerManager.me == old com/dmdirc/Serve rManager.me
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	new ConditionTree(readTerm#1)._tainted == 0
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	new ActionType[](ActionModel#2) num objects == undefined
post	new ActionType[](ActionModel#2) num objects == 0, if init'ed
post	new ActionType[](ActionModel#2).length == new ActionType[](ActionModel#2) num objects
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 ServerManager(getServerManager#1) num objects == new ActionType[](ActionModel#2) num objects
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 ActionType[](ActionModel#2)[...] == undefined
post	new ActionType[](ActionModel#2)[...] == null
post	new ServerManager(getServerManager#1).servers == new ActionType[](ActionModel#2)[...]
post	new String[](ActionModel#3)[...] == new ActionType[](ActionModel#2)[...]
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	init'ed(new ConditionTree(readTerm#1) num objects)
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
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on readTerm
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on parseStack
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:size
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.Character:valueOf

call too complex - analysis skipped Info call on void com.dmdirc.actions.Action(String, String, ActionType[], String[], List, ConditionTree, String)

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

call too complex - analysis skipped Info call on void save()

method	void loadActionFromConfig()
pre	this.config != null
pre	(soft) init'ed(com/dmdirc/ServerManager.me)
pre	(soft) init'ed(this.triggers[0])
pre	(soft) init'ed(this.triggers[...])
pre	(soft) this.conditions != null
pre	(soft) init'ed(this.group)
pre	(soft) init'ed(this.name)
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	possibly_updated(this.conditionTree)
post	possibly_updated(this.newFormat)
post	this.response == One-of{old this.response, &new String[](loadActionFromConfig#1)}
post	init'ed(this.response[...])
post	this.triggers == One-of{&new ActionType[](loadT riggers#1), old this.triggers}
post	init'ed(this.triggers[0])
post	init'ed(this.triggers[...])
post	new ActionType[](loadTriggers#1) num objects <= 1
post	init'ed(new ActionType[](loadTriggers#1).length)
post	init'ed(new ActionType[](loadTriggers#1)[0])
post	possibly_updated(new ActionType[](loadTriggers#1)[...])
post	new ArrayList(ServerManager#1) num objects <= 1
post	new ConditionTree(parseStack#3) num objects <= 1
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	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	new ServerManager(getServerManager#1) num objects <= 1
post	init'ed(new ServerManager(getServerManager#1). servers)
post	new String[](loadActionFromConfig#1) num objects <= 1
post	init'ed(new String[](loadActionFromConfig#1). length)
post	init'ed(new String[](loadActionFromConfig#1)[...])
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on com.dmdirc.util.ConfigFile:isKeyDomain
unanalyzed	call on com.dmdirc.util.ConfigFile:getKeyDomain
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on getType
unanalyzed	call on getArity
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on com.dmdirc.config.IdentityManager:getAddonI dentity
unanalyzed	call on com.dmdirc.config.Identity:setOption
unanalyzed	call on com.dmdirc.config.prefs.PreferencesType:val ueOf
unanalyzed	call on com.dmdirc.config.prefs.PreferencesSetting
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Enum:name
unanalyzed	call on getActionComponent
unanalyzed	call on getArgTypes
unanalyzed	call on appliesTo
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.Class:getName
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on java.lang.IllegalArgumentException:getMessa ge
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on readTerm
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on parseStack
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:size
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on getMaximumArgument
unanalyzed	call on java.lang.Math:max
unanalyzed	call on com.dmdirc.util.MapList:add
unanalyzed	call on getTriggers
unanalyzed	call on getTabCompleter
unanalyzed	call on getConditions
unanalyzed	call on com.dmdirc.commandparser.CommandManager:get CommandChar
unanalyzed	call on getGroup
unanalyzed	call on add
unanalyzed	call on getName
unanalyzed	call on getGlobalWindow
unanalyzed	call on com.dmdirc.ui.input.TabCompleter:addEntry
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}

method not available - call not analyzed Info call on bool com.dmdirc.util.ConfigFile:isFlatDomai n(String)

method not available - call not analyzed Info call on List com.dmdirc.util.ConfigFile:getFlatDoma in(String)

method not available - call not analyzed Info call on bool com.dmdirc.util.ConfigFile:isFlatDomai n(String)

method not available - call not analyzed Info call on List com.dmdirc.util.ConfigFile:getFlatDoma in(String)

Prev Msg Next Msg

array index out of bounds

click for all messages in this file Medium Prob.

check that i < this.response.length

overflow

Low Prob.

check that i in {-2³¹-1..2³²-2}

Prev Msg Next Msg

method not available - call not analyzed Info call on bool com.dmdirc.util.ConfigFile:isFlatDomai n(String)

method not available - call not analyzed Info call on List com.dmdirc.util.ConfigFile:getFlatDoma in(String)

Prev Msg Next Msg

overflow

click for all messages in this file Low Prob.

check that cond in {-2³¹-1..2³²-2}

method not available - call not analyzed Info call on bool com.dmdirc.util.ConfigFile:isKeyDomain (String)

Prev Msg Next Msg

method not available - call not analyzed Info call on Map com.dmdirc.util.ConfigFile:getKeyDomain (String)

method not available - call not analyzed Info call on bool com.dmdirc.util.ConfigFile:isFlatDomai n(String)

method not available - call not analyzed Info call on List com.dmdirc.util.ConfigFile:getFlatDoma in(String)

method not available - call not analyzed Info call on List com.dmdirc.util.ConfigFile:getFlatDoma in(String)

method	void checkMetaData()
pre	this.config != null
pre	(soft) init'ed(this.group)
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 java.util.Map:put
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Map:get
unanalyzed	call on com.dmdirc.config.IdentityManager:getAddonI dentity
unanalyzed	call on com.dmdirc.config.Identity:setOption
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}

method not available - call not analyzed Info call on bool com.dmdirc.util.ConfigFile:isKeyDomain (String)

method not available - call not analyzed Info call on Map com.dmdirc.util.ConfigFile:getKeyDomain (String)

Prev Msg Next Msg

overflow

click for all messages in this file Low Prob.

check that i in {-2³¹-1..2³²-2}

method not available - call not analyzed Info call on bool com.dmdirc.util.ConfigFile:isKeyDomain (String)

Prev Msg Next Msg

method not available - call not analyzed Info call on Map com.dmdirc.util.ConfigFile:getKeyDomain (String)

method not available - call not analyzed Info call on PreferencesType com.dmdirc.config.prefs. PreferencesType:valueOf(String)

method not available - call not analyzed Info call on void com.dmdirc.config.prefs. PreferencesSetting(PreferencesType, String, String, String, String)

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

method	void save()
pre	init'ed(this.modified)
pre	(soft) init'ed(com.dmdirc.actions.ConditionTree$1__ static_init.new int[](ConditionTree$1__static_init# 1)[...])
pre	(soft) com.dmdirc.actions.CoreActionType__static_ init.new CoreActionType(CoreActionType__static_init #72).type != null
pre	(soft) init'ed(com/dmdirc/actions/ActionManager. killSwitch)
pre	(soft) init'ed(com/dmdirc/ServerManager.me)
pre	(soft) init'ed(this.conditionTree)
pre	(soft) init'ed(this.conditionTree.argument)
pre	(soft) init'ed(this.conditionTree.leftArg)
pre	(soft) this.conditionTree.op != null
pre	(soft) init'ed(this.conditionTree.rightArg)
pre	(soft) this.conditions != null
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) this.response != null
pre	(soft) this.response.length <= 2³²-1
pre	(soft) init'ed(this.response[...])
pre	(soft) this.triggers != null
pre	(soft) this.triggers.length <= 2³²-1
pre	(soft) init'ed(this.triggers[...])
presumption	init'ed(com.dmdirc.logger.ErrorLevel.HIGH)
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
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	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 com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on getType
unanalyzed	call on com.dmdirc.util.MapList:containsKey
unanalyzed	call on com.dmdirc.util.MapList:get
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on trigger
unanalyzed	call on getArity
unanalyzed	call on com.dmdirc.interfaces.ActionListener:proces sEvent
unanalyzed	call on triggerActions
unanalyzed	call on getArgTypes
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on readTerm
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on parseStack
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:size
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:iterator
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.config.ConfigManager:getOptions
unanalyzed	call on java.util.Map:entrySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.util.Map$Entry:getKey
unanalyzed	call on java.util.Map$Entry:getValue
unanalyzed	call on [Ljava.lang.String;:instanceof
unanalyzed	call on java.lang.String:instanceof
unanalyzed	call on java.lang.String:split
unanalyzed	call on doServerSubstitutions
unanalyzed	call on doComponentSubstitutions
unanalyzed	call on getServer
unanalyzed	call on getState
unanalyzed	call on com.dmdirc.ServerState:equals
unanalyzed	call on getCompatibleComponents
unanalyzed	call on java.lang.Object:toString
unanalyzed	call on get
unanalyzed	call on test
unanalyzed	call on evaluate
unanalyzed	call on getUI
unanalyzed	call on com.dmdirc.ui.interfaces.UIController:getAc tiveWindow
unanalyzed	call on getFrame
unanalyzed	call on com.dmdirc.ui.interfaces.InputWindow:instan ceof
unanalyzed	call on java.util.List:get
unanalyzed	call on com.dmdirc.commandparser.parsers. GlobalCommandParser:getGlobalCommandParser
unanalyzed	call on com.dmdirc.ui.interfaces.InputWindow:getCom mandParser
unanalyzed	call on com.dmdirc.commandparser.parsers. CommandParser:parseCommand
test_vector	this.modified: {1}, {0}
test_vector	this.conditionTree: Addr_Set{null}, Inverse{null}
test_vector	this.config: Addr_Set{null}, Inverse{null}
test_vector	this.newFormat: Addr_Set{null}, Inverse{null}
test_vector	this.triggers[...]: Inverse{null}, Addr_Set{null}
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}

method not available - call not analyzed Info call on void com.dmdirc.util.ConfigFile(String)

method not available - call not analyzed Info call on void com.dmdirc.logger.Logger:appError(Erro rLevel, String, Throwable)

method not available - call not analyzed Info call on void com.dmdirc.util.ConfigFile:addDomain(S tring, List)

Prev Msg Next Msg

unused assignment in callee

click for all messages in this file Low Prob.

Unused assignment to (java.lang.String:valueOf(... )._tainted, java.lang.StringBuilder:toString(...)._ tainted, java.lang.StringBuilder:toString(...). _tainted, java.lang.StringBuilder:toString(...). _tainted) in toString

method not available - call not analyzed Info call on List com.dmdirc.util.ConfigFile:getFlatDoma in(String)

Prev Msg Next Msg

method not available - call not analyzed Info call on void com.dmdirc.util.ConfigFile:addDomain(S tring, List)

method not available - call not analyzed Info call on List com.dmdirc.util.ConfigFile:getFlatDoma in(String)

method not available - call not analyzed Info call on void com.dmdirc.util.ConfigFile:addDomain(S tring, Map)

Prev Msg Next Msg

overflow

click for all messages in this file Low Prob.

check that i in {-2³¹-1..2³²-2}

Prev Msg Next Msg

method not available - call not analyzed Info call on bool com.dmdirc.util.ConfigFile:isKeyDomain (String)

method not available - call not analyzed Info call on Map com.dmdirc.util.ConfigFile:getKeyDomain (String)

method not available - call not analyzed Info call on void com.dmdirc.util.ConfigFile:addDomain(S tring, Map)

method not available - call not analyzed Info call on void com.dmdirc.util.ConfigFile:write()

method not available - call not analyzed Info call on void com.dmdirc.logger.Logger:userError(Err orLevel, String)

method	bool readCondition(Map)
pre	data != null
pre	(soft) this.conditions != null
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
presumption	appliesTo(...)@414 != null
presumption	getType(...)@385 != getType(...)
presumption	java.util.Map:get(...)@408 != null
post	init'ed(return_value)
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on getType
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Enum:name
unanalyzed	call on getActionComponent
unanalyzed	call on getArgTypes
unanalyzed	call on appliesTo
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.List:add
unanalyzed	call on java.lang.Class:getName
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on java.lang.IllegalArgumentException:getMessa ge
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}

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into target

Prev Msg Next Msg

call too complex - analysis skipped Info call on int getArity()

call too complex - analysis skipped Info call on Class appliesTo()

call too complex - analysis skipped Info call on Class getType()

method	ActionComponent readComponent(Map, int)
pre	data != null
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
presumption	appliesTo(...)@467 != null
presumption	getArgTypes(...).length@454 >= 1
presumption	arg < getArgTypes(...).length@454
presumption	getArgTypes(...).length@467 >= 1
presumption	arg < getArgTypes(...).length@467
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	possibly_updated(new ActionComponentChain(readCompo nent#1).components)
post	new ArrayList(ActionComponentChain#1) num objects <= 1
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Enum:name
unanalyzed	call on getActionComponent
unanalyzed	call on appliesTo
unanalyzed	call on getType
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.List:add
unanalyzed	call on java.lang.Class:getName
unanalyzed	call on java.lang.IllegalArgumentException
test_vector	java.lang.Object:equals(...)@467: {1}, {0}
test_vector	java.lang.String:indexOf(...)@450: {-2³¹. .-2, 0..2³²-1}, {-1}

call too complex - analysis skipped Info call on Class[] getArgTypes()

call too complex - analysis skipped Info call on Class appliesTo()

call too complex - analysis skipped Info call on Class[] getArgTypes()

method	void error(String)
pre	init'ed(this.group)
pre	init'ed(this.name)
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)

method not available - call not analyzed Info call on void com.dmdirc.logger.Logger:userError(Err orLevel, String)

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

call too complex - analysis skipped Info call on void save()

method	void setGroup(String)
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 == One-of{old com/dmdirc/Main.configdir, &java.lang. StringBuilder:toString(...)}
post	com/dmdirc/Main.configdir != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	this.group == newGroup
post	init'ed(this.group)
post	this.location == &java.lang.StringBuilder:toStr ing(...)
post	this.modified == 1
unanalyzed	call on getConfigDir
unanalyzed	call on java.lang.System:getProperty
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.System:getenv

call too complex - analysis skipped Info call on void save()

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

method	String toString()
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	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	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &java.lang.StringBuilder:toStri ng(...)
unanalyzed	call on java.util.Arrays:toString

	method not available - call not analyzed	Info	call on String com.dmdirc.util.InvalidConfigFileExc eption:getMessage()
	method not available - call not analyzed	Info	call on void com.dmdirc.logger.Logger:userError(Err orLevel, String)

	method not available - call not analyzed	Info	call on bool com.dmdirc.util.ConfigFile:isFlatDomai n(String)
	method not available - call not analyzed	Info	call on List com.dmdirc.util.ConfigFile:getFlatDoma in(String)

	method not available - call not analyzed	Info	call on PreferencesType com.dmdirc.config.prefs. PreferencesType:valueOf(String)
	method not available - call not analyzed	Info	call on void com.dmdirc.config.prefs. PreferencesSetting(PreferencesType, String, String, String, String)

	method not available - call not analyzed	Info	call on Map com.dmdirc.util.ConfigFile:getKeyDomain (String)
	method not available - call not analyzed	Info	call on void com.dmdirc.util.ConfigFile:addDomain(S tring, Map)

	call too complex - analysis skipped	Info	call on Class appliesTo()
	call too complex - analysis skipped	Info	call on Class getType()