Alias.java

Alias.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.wrappers.Alias(String)

Kind	Annotation Text
post	init'ed(this.command)
post	new ArrayList(Alias#1) num objects == 1
post	new String[](Alias#3) num objects == 1
post	this.arguments == &new ArrayList(Alias#1)
post	this.command == command
post	this.response == &new String[](Alias#3)
post	this.response.length == 1
post	this.response[0] == &""

void com.dmdirc.actions.wrappers.Alias(String, List, String[])

Kind	Annotation Text
pre	(soft) init'ed(response[...])
pre	response != null
post	init'ed(this.command)
post	init'ed(this.response.length)
post	new ArrayList(Alias#1) num objects == 1
post	new String[](Alias#2) num objects == 1
post	this.arguments == &new ArrayList(Alias#1)
post	this.command == command
post	this.response == &new String[](Alias#2)
post	this.response.length == response.length
post	this.response[...] == One-of{response[...], undefined}

com.dmdirc.actions.wrappers.Alias__static_init

Kind	Annotation Text

Action createAction()

Kind	Annotation Text
pre	(soft) init'ed(this.response[...])
pre	init'ed(com/dmdirc/actions/wrappers/AliasWrapper. me)
pre	init'ed(this.command)
pre	this.arguments != null
pre	this.response != null
post	com/dmdirc/actions/wrappers/AliasWrapper.me != null
post	com/dmdirc/actions/wrappers/AliasWrapper.me == One-of{old com/dmdirc/actions/wrappers/AliasWrappe r.me, &new AliasWrapper(getAliasWrapper#1)}
post	new Action(createAction#1) num objects == 1
post	new AliasWrapper(getAliasWrapper#1) num objects <= 1
post	new AliasWrapper(getAliasWrapper#1).actions == &new ArrayList(ActionGroup#1)
post	new AliasWrapper(getAliasWrapper#1).aliases == &new ArrayList(AliasWrapper#1)
post	new AliasWrapper(getAliasWrapper#1).author == null
post	new AliasWrapper(getAliasWrapper#1).component == -1
post	new AliasWrapper(getAliasWrapper#1).description == null
post	new AliasWrapper(getAliasWrapper#1).name == &"aliases"
post	new AliasWrapper(getAliasWrapper#1).settings == &new HashMap(ActionGroup#2)
post	new AliasWrapper(getAliasWrapper#1).version == -1
post	new ArrayList(ActionGroup#1) num objects == new AliasWrapper(getAliasWrapper#1) num objects
post	new ArrayList(AliasWrapper#1) num objects == new AliasWrapper(getAliasWrapper#1) num objects
post	new HashMap(ActionGroup#2) num objects == new AliasWrapper(getAliasWrapper#1) num objects
post	return_value == &new Action(createAction#1)
unanalyzed	call on com.dmdirc.actions.ActionGroup
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on java.lang.Object:toString
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:size

ActionCondition getArgsArgument()

Kind	Annotation Text
pre	this.arguments != null
presumption	java.util.List:get(...)@156 != null
post	init'ed(return_value)
test_vector	argument.comparison@156: Inverse{&com.dmdirc. actions.CoreActionComparison__static_init.new CoreActionComparison$2(CoreActionComparison__ static_init#2)}, Addr_Set{&com.dmdirc.actions. CoreActionComparison__static_init.new CoreActionCompariso...
test_vector	java.util.List:size(...)@159: {-2³¹..1}, {2..2³²-1}

List getArguments()

Kind	Annotation Text
pre	init'ed(this.arguments)
post	new ArrayList(getArguments#1) num objects == 1
post	return_value == &new ArrayList(getArguments#1)

String getCommand()

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

String getName()

Kind	Annotation Text
pre	init'ed(this.command)
pre	this.arguments != null
presumption	condition.comparison != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value in Addr_Set{&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...)}
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:size
test_vector	java.lang.Object:equals(...)@126: {0}, {1}
test_vector	java.lang.Object:equals(...)@128: {0}, {1}
test_vector	java.lang.Object:equals(...)@130: {0}, {1}

String[] getResponse()

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

bool matches(Alias)

Kind	Annotation Text
pre	(soft) init'ed(alias.arguments)
pre	(soft) init'ed(this.arguments)
pre	alias != null
pre	alias.command != null
pre	init'ed(this.command)
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList

void setArguments(List)

Kind	Annotation Text
pre	this.arguments != null
post	new ArrayList(setArguments#1) num objects <= 1
post	this.arguments != null
post	this.arguments == One-of{old this.arguments, &new ArrayList(setArguments#1)}
test_vector	java.lang.Object:equals(...)@175: {1}, {0}

void setCommand(String)

Kind	Annotation Text
pre	(soft) this.arguments != null
pre	this.command != null
presumption	java.util.List:get(...)@105 != null
presumption	java.util.List:get(...)@108 != null
post	init'ed(this.command)
post	this.command == One-of{old this.command, command}
test_vector	argument.comparison@105: Addr_Set{&com.dmdirc. actions.CoreActionComparison__static_init.new CoreActionComparison$2(CoreActionComparison__ static_init#2)}, Inverse{&com.dmdirc.actions. CoreActionComparison__static_init.new CoreActionCompariso...
test_vector	java.lang.String:equals(...)@100: {1}, {0}

void setResponse(String[])

Kind	Annotation Text
pre	(soft) init'ed(response[...])
pre	(soft) response != null
pre	init'ed(this.response)
post	init'ed(new String[](setResponse#1).length)
post	init'ed(this.response)
post	new String[](setResponse#1) num objects <= 1
post	new String[](setResponse#1).length == response.length
post	possibly_updated(new String[](setResponse#1)[...])
post	this.response == One-of{old this.response, &new String[](setResponse#1)}
test_vector	java.util.Arrays:equals(...)@195: {1}, {0}

String toString()

Kind	Annotation Text
pre	init'ed(this.command)
pre	init'ed(this.response)
pre	this.arguments != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &java.lang.StringBuilder:toStri ng(...)
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on java.lang.Object:toString
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:size

void update(Alias)

Kind	Annotation Text
pre	(soft) init'ed(alias.response[...])
pre	alias != null
pre	alias.response != null
pre	init'ed(alias.arguments)
pre	init'ed(alias.command)
pre	init'ed(this.response)
pre	this.arguments != null
pre	this.command != null
post	init'ed(new String[](setResponse#1).length)
post	init'ed(this.command)
post	init'ed(this.response)
post	new ArrayList(setArguments#1) num objects <= 1
post	new String[](setResponse#1) num objects <= 1
post	new String[](setResponse#1).length == alias.response.length
post	possibly_updated(new String[](setResponse#1)[...])
post	this.arguments != null
post	this.arguments == One-of{old this.arguments, &new ArrayList(setArguments#1)}
post	this.command == One-of{old this.command, alias.command}
post	this.response == One-of{old this.response, &new String[](setResponse#1)}
unanalyzed	call on java.lang.Object:equals
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Arrays:equals
unanalyzed	call on java.util.List:get