Messages

Last Msg First Msg

method

com.dmdirc.actions.ActionModel__static_init

method	void com.dmdirc.actions.ActionModel(String, String)
post	this.conditions == &new ArrayList(ActionModel#1 )
post	this.group == group
post	init'ed(this.group)
post	this.name == name
post	init'ed(this.name)
post	new ArrayList(ActionModel#1) num objects == 1

method	void com.dmdirc.actions.ActionModel(String, String, ActionType[], String[], List, ConditionTree, String)
pre	response != null
pre	triggers != null
pre	(soft) init'ed(response[...])
pre	(soft) init'ed(triggers[...])
post	this.conditionTree == conditionTree
post	init'ed(this.conditionTree)
post	this.conditions == conditions
post	init'ed(this.conditions)
post	this.group == group
post	init'ed(this.group)
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	this.triggers.length == triggers.length
post	init'ed(this.triggers.length)
post	this.triggers[...] == One-of{triggers[...], undefined}
post	this.response.length == response.length
post	init'ed(this.response.length)
post	this.response[...] == One-of{response[...], undefined}

method	void trigger(StringBuffer, Object[])
pre	init'ed(this.conditionTree)
pre	this.conditions != null
pre	this.triggers != null
pre	this.triggers.length >= 1
pre	this.triggers[0] != null
pre	(soft) arguments != null
pre	(soft) init'ed(arguments[0])
pre	(soft) init'ed(arguments[1])
pre	(soft) arguments[1].length in {1..2³²-1}
pre	(soft) init'ed(arguments[2])
pre	(soft) arguments[2].length in {1..2³²-1}
pre	(soft) init'ed(arguments[...])
pre	(soft) init'ed(com.dmdirc.actions.ConditionTree$1__ static_init.new int[](ConditionTree$1__static_init# 1)[...])
pre	(soft) com/dmdirc/Main.controller != null
pre	(soft) init'ed(com/dmdirc/ServerManager.me)
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[0].type != null
presumption	com.dmdirc.commandparser.parsers.GlobalCommandParse r:getGlobalCommandParser(...)@140 != null
presumption	com.dmdirc.ui.interfaces.InputWindow:getCommandPars er(...)@142 != null
presumption	getServerManager(...).servers != null
presumption	java.util.List:get(...)@136 != null
post	init'ed(com/dmdirc/ServerManager.me)
post	init'ed(format._tainted)
post	new ArrayList(ServerManager#1) num objects <= 1
post	new ArrayList(ServerManager#1) num objects == 0
post	new ServerManager(getServerManager#1) num objects <= 1
post	new ServerManager(getServerManager#1) num objects == 0
post	init'ed(new ServerManager(getServerManager#1). servers)
unanalyzed	call on java.util.List:size
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: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 getType
unanalyzed	call on getArgTypes
unanalyzed	call on test
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on evaluate
unanalyzed	call on java.util.ArrayList
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on java.util.List:add
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on appliesTo
test_vector	arguments.length: {0}, {1..+Inf}
test_vector	format: Addr_Set{null}, Inverse{null}
test_vector	this.newFormat: Addr_Set{null}, Inverse{null}
test_vector	java.util.List:size(...)@140: {-2³¹..0}, {1..2³²-1}

method not available - call not analyzed Info call on Window com.dmdirc.ui.interfaces. UIController:getActiveWindow()

call too complex - analysis skipped Info call on InputWindow getFrame()

method not available - call not analyzed Info call on GlobalCommandParser com.dmdirc. commandparser.parsers.GlobalCommandParser:getGlobal CommandParser()

method not available - call not analyzed Info call on CommandParser com.dmdirc.ui.interfaces. InputWindow:getCommandParser()

Prev Msg Next Msg

unused assignment in callee

click for all messages in this file Low Prob.

Unused assignment to (java.lang.StringBuilder:toStr ing(...)._tainted) in doSubstitution

method not available - call not analyzed Info call on void com.dmdirc.commandparser.parsers. CommandParser:parseCommand(InputWindow, String)

Prev Msg Next Msg

method	bool test(ActionSubstitutor, Object[])
pre	init'ed(this.conditionTree)
pre	this.conditions != null
pre	(soft) arguments != null
pre	(soft) init'ed(arguments[0])
pre	(soft) init'ed(arguments[1])
pre	(soft) arguments[1].length in {1..2³²-1}
pre	(soft) init'ed(arguments[2])
pre	(soft) arguments[2].length in {1..2³²-1}
pre	(soft) init'ed(arguments[...])
pre	(soft) init'ed(com.dmdirc.actions.ConditionTree$1__ static_init.new int[](ConditionTree$1__static_init# 1)[...])
pre	(soft) sub != null
pre	(soft) sub.type != null
pre	(soft) sub.type.type != null
presumption	condition.arg@166 >= -1
presumption	condition.arg@166 < arguments.length
presumption	condition.comparison@166 != null
presumption	condition.component@166 != null
presumption	getRealConditionTree(...)...argument@170 >= 0
presumption	getRealConditionTree(...)...leftArg@170 != null
presumption	getRealConditionTree(...)...op@170 != null
presumption	getRealConditionTree(...)...rightArg@170 != null
presumption	getRealConditionTree(...).argument@170 in {0..2³²-2}
presumption	getRealConditionTree(...).argument@170 - java.util.List:size(...)@163 in {-2³²+1.. -1}
presumption	getRealConditionTree(...).leftArg@170 != null
presumption	getRealConditionTree(...).op@170 != null
presumption	getRealConditionTree(...).rightArg@170 != null
presumption	java.util.Iterator:next(...)@166 != null
presumption	java.util.List:size(...)@163 >= 1
post	init'ed(return_value)
unanalyzed	call on java.util.List:size
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.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.util.List:iterator
unanalyzed	call on java.lang.Object:toString
unanalyzed	call on get
unanalyzed	call on getType
unanalyzed	call on getArgTypes
unanalyzed	call on test
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on evaluate
unanalyzed	call on java.util.ArrayList
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on java.util.List:add
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on appliesTo
test_vector	java.util.Iterator:hasNext(...)@166: {0}, {1}

Prev Msg Next Msg

array index out of bounds

click for all messages in this file Medium Prob.

check that i < results.length

overflow

Low Prob.

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

Prev Msg Next Msg

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that getRealConditionTree(...) != null

Prev Msg Next Msg

method	List getConditions()
pre	init'ed(this.conditions)
post	return_value == this.conditions
post	init'ed(return_value)

method	void setConditions(List)
post	this.conditions == conditions
post	init'ed(this.conditions)
post	this.modified == 1

method	ActionType[] getTriggers()
pre	init'ed(this.triggers)
pre	(soft) init'ed(this.triggers[...])
post	return_value == One-of{this.triggers, &new ActionType[](getTriggers#1)}
post	return_value in Addr_Set{null,&new ActionType[](getTriggers#1)}
post	new ActionType[](getTriggers#1) num objects <= 1
post	new ActionType[](getTriggers#1).length == this.triggers.length
post	init'ed(new ActionType[](getTriggers#1).length)
post	new ActionType[](getTriggers#1)[...] == One-of{this.triggers[...], undefined}

method	void setTriggers(ActionType[])
pre	triggers != null
pre	(soft) init'ed(triggers[...])
post	this.modified == 1
post	new ActionType[](setTriggers#1) num objects == 1
post	this.triggers == &new ActionType[](setTriggers# 1)
post	this.triggers.length == triggers.length
post	init'ed(this.triggers.length)
post	possibly_updated(this.triggers[...])

method	String getNewFormat()
pre	init'ed(this.newFormat)
post	return_value == this.newFormat
post	init'ed(return_value)

method	void setNewFormat(String)
post	this.modified == 1
post	this.newFormat == newFormat
post	init'ed(this.newFormat)

method	String[] getResponse()
pre	init'ed(this.response)
pre	(soft) init'ed(this.response[...])
post	return_value == One-of{this.response, &new String[](getResponse#1)}
post	return_value in Addr_Set{null,&new String[](getResponse#1)}
post	new String[](getResponse#1) num objects <= 1
post	new String[](getResponse#1).length == this.response.length
post	init'ed(new String[](getResponse#1).length)
post	new String[](getResponse#1)[...] == One-of{this.response[...], undefined}

method	void setResponse(String[])
pre	response != null
pre	(soft) init'ed(response[...])
post	this.modified == 1
post	new String[](setResponse#1) num objects == 1
post	this.response == &new String[](setResponse#1)
post	this.response.length == response.length
post	init'ed(this.response.length)
post	possibly_updated(this.response[...])

method	String getGroup()
pre	init'ed(this.group)
post	return_value == this.group
post	init'ed(return_value)

method	void setGroup(String)
post	this.group == newGroup
post	init'ed(this.group)
post	this.modified == 1

method	String getName()
pre	init'ed(this.name)
post	return_value == this.name
post	init'ed(return_value)

method	void setName(String)
post	this.modified == 1
post	this.name == newName
post	init'ed(this.name)

method	ConditionTree getConditionTree()
pre	init'ed(this.conditionTree)
post	return_value == this.conditionTree
post	init'ed(return_value)

method	ConditionTree getRealConditionTree()
pre	init'ed(this.conditionTree)
pre	(soft) this.conditions != null
post	init'ed(return_value)
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

method	void setConditionTree(ConditionTree)
post	this.conditionTree == conditionTree
post	init'ed(this.conditionTree)
post	this.modified == 1

method	bool isModified()
pre	init'ed(this.modified)
post	return_value == this.modified
post	init'ed(return_value)

method	void resetModified()
post	this.modified == 0

method	String toString()
pre	init'ed(this.conditions)
pre	init'ed(this.group)
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.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(...)