ActionModel.java

ActionModel.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

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

Kind	Annotation Text
post	init'ed(this.group)
post	init'ed(this.name)
post	new ArrayList(ActionModel#1) num objects == 1
post	this.conditions == &new ArrayList(ActionModel#1 )
post	this.group == group
post	this.name == name

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

Kind	Annotation Text
pre	(soft) init'ed(response[...])
pre	(soft) init'ed(triggers[...])
pre	response != null
pre	triggers != null
post	init'ed(this.conditionTree)
post	init'ed(this.conditions)
post	init'ed(this.group)
post	init'ed(this.name)
post	init'ed(this.newFormat)
post	init'ed(this.response.length)
post	init'ed(this.triggers.length)
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.conditionTree == conditionTree
post	this.conditions == conditions
post	this.group == group
post	this.modified == 1
post	this.name == name
post	this.newFormat == newFormat
post	this.response == &new String[](ActionModel#3)
post	this.response.length == response.length
post	this.response[...] == One-of{response[...], undefined}
post	this.triggers == &new ActionType[](ActionModel# 2)
post	this.triggers.length == triggers.length
post	this.triggers[...] == One-of{triggers[...], undefined}

com.dmdirc.actions.ActionModel__static_init

Kind	Annotation Text

ConditionTree getConditionTree()

Kind	Annotation Text
pre	init'ed(this.conditionTree)
post	init'ed(return_value)
post	return_value == this.conditionTree

List getConditions()

Kind	Annotation Text
pre	init'ed(this.conditions)
post	init'ed(return_value)
post	return_value == this.conditions

String getGroup()

Kind	Annotation Text
pre	init'ed(this.group)
post	init'ed(return_value)
post	return_value == this.group

String getName()

Kind	Annotation Text
pre	init'ed(this.name)
post	init'ed(return_value)
post	return_value == this.name

String getNewFormat()

Kind	Annotation Text
pre	init'ed(this.newFormat)
post	init'ed(return_value)
post	return_value == this.newFormat

ConditionTree getRealConditionTree()

Kind	Annotation Text
pre	(soft) this.conditions != null
pre	init'ed(this.conditionTree)
post	init'ed(new ConditionTree(readTerm#1) num objects)
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	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.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

String[] getResponse()

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

ActionType[] getTriggers()

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

bool isModified()

Kind	Annotation Text
pre	init'ed(this.modified)
post	init'ed(return_value)
post	return_value == this.modified

void resetModified()

Kind	Annotation Text
post	this.modified == 0

void setConditionTree(ConditionTree)

Kind	Annotation Text
post	init'ed(this.conditionTree)
post	this.conditionTree == conditionTree
post	this.modified == 1

void setConditions(List)

Kind	Annotation Text
post	init'ed(this.conditions)
post	this.conditions == conditions
post	this.modified == 1

void setGroup(String)

Kind	Annotation Text
post	init'ed(this.group)
post	this.group == newGroup
post	this.modified == 1

void setName(String)

Kind	Annotation Text
post	init'ed(this.name)
post	this.modified == 1
post	this.name == newName

void setNewFormat(String)

Kind	Annotation Text
post	init'ed(this.newFormat)
post	this.modified == 1
post	this.newFormat == newFormat

void setResponse(String[])

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

void setTriggers(ActionType[])

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

bool test(ActionSubstitutor, Object[])

Kind	Annotation Text
pre	(soft) arguments != null
pre	(soft) arguments[1].length in {1..2³²-1}
pre	(soft) arguments[2].length in {1..2³²-1}
pre	(soft) init'ed(arguments[0])
pre	(soft) init'ed(arguments[1])
pre	(soft) init'ed(arguments[2])
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
pre	init'ed(this.conditionTree)
pre	this.conditions != null
presumption	condition.arg@166 < arguments.length
presumption	condition.arg@166 >= -1
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 - java.util.List:size(...)@163 in {-2³²+1.. -1}
presumption	getRealConditionTree(...).argument@170 in {0..2³²-2}
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 [Ljava.lang.String;:instanceof
unanalyzed	call on appliesTo
unanalyzed	call on com.dmdirc.ServerState:equals
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on com.dmdirc.config.ConfigManager:getOptions
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on doComponentSubstitutions
unanalyzed	call on doServerSubstitutions
unanalyzed	call on evaluate
unanalyzed	call on get
unanalyzed	call on getArgTypes
unanalyzed	call on getCompatibleComponents
unanalyzed	call on getServer
unanalyzed	call on getState
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.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: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.List:add
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
test_vector	java.util.Iterator:hasNext(...)@166: {0}, {1}

String toString()

Kind	Annotation Text
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	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
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	return_value == &java.lang.StringBuilder:toStri ng(...)

void trigger(StringBuffer, Object[])

Kind	Annotation Text
pre	(soft) arguments != null
pre	(soft) arguments[1].length in {1..2³²-1}
pre	(soft) arguments[2].length in {1..2³²-1}
pre	(soft) com/dmdirc/Main.controller != null
pre	(soft) init'ed(arguments[0])
pre	(soft) init'ed(arguments[1])
pre	(soft) init'ed(arguments[2])
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) init'ed(com/dmdirc/ServerManager.me)
pre	(soft) init'ed(this.newFormat)
pre	(soft) init'ed(this.response[...])
pre	(soft) this.response != null
pre	(soft) this.response.length <= 2³²-1
pre	(soft) this.triggers[0].type != null
pre	init'ed(this.conditionTree)
pre	this.conditions != null
pre	this.triggers != null
pre	this.triggers.length >= 1
pre	this.triggers[0] != 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	init'ed(new ServerManager(getServerManager#1). servers)
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
unanalyzed	call on [Ljava.lang.String;:instanceof
unanalyzed	call on appliesTo
unanalyzed	call on com.dmdirc.ServerState:equals
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on com.dmdirc.config.ConfigManager:getOptions
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.logger.Logger:assertTrue
unanalyzed	call on doComponentSubstitutions
unanalyzed	call on doServerSubstitutions
unanalyzed	call on evaluate
unanalyzed	call on get
unanalyzed	call on getArgTypes
unanalyzed	call on getCompatibleComponents
unanalyzed	call on getServer
unanalyzed	call on getState
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.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: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.List:add
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
test_vector	arguments.length: {0}, {1..+Inf}
test_vector	format: Addr_Set{null}, Inverse{null}
test_vector	java.util.List:size(...)@140: {-2³¹..0}, {1..2³²-1}
test_vector	this.newFormat: Addr_Set{null}, Inverse{null}