CommandArguments.java

CommandArguments.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void com.dmdirc.commandparser.CommandArguments(String)

Kind	Annotation Text
post	init'ed(this.line)
post	this.line == line

com.dmdirc.commandparser.CommandArguments__static_init

Kind	Annotation Text

String[] getArguments()

Kind	Annotation Text
pre	(soft) this.line != null
pre	init'ed(this.words)
presumption	this.words.length@97 <= 2³²-1
post	init'ed(java.lang.String:split(...)._tainted)
post	init'ed(java.lang.String:split(...).length)
post	init'ed(return_value)
post	this.words != null
post	this.words == One-of{old this.words, &java.lang.String:split(...)}
unanalyzed	call on java.lang.String:split

String getArgumentsAsString()

Kind	Annotation Text
pre	(soft) this.line != null
pre	init'ed(this.words)
post	init'ed(java.lang.String:split(...)._tainted)
post	init'ed(java.lang.String:split(...).length)
post	init'ed(return_value)
post	java.lang.String:split(...)._tainted == 0
post	this.words != null
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.regex.Matcher:group
unanalyzed	call on java.util.regex.Matcher:matches
unanalyzed	call on java.util.regex.Pattern:compile
unanalyzed	call on java.util.regex.Pattern:matcher

String getArgumentsAsString(int)

Kind	Annotation Text
pre	(soft) this.line != null
pre	init'ed(this.words)
pre	start <= 2³²-2
presumption	this.words.length@123 - start in {-2³¹+1.. 2³²}
presumption	this.words.length@123 <= 2³²-1
post	init'ed(java.lang.String:split(...)._tainted)
post	init'ed(java.lang.String:split(...).length)
post	init'ed(return_value)
post	this.words != null
post	this.words == One-of{old this.words, &java.lang.String:split(...)}
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.regex.Matcher:group
unanalyzed	call on java.util.regex.Matcher:matches
unanalyzed	call on java.util.regex.Pattern:compile
unanalyzed	call on java.util.regex.Pattern:matcher

String getCommandName()

Kind	Annotation Text
pre	(soft) init'ed(com/dmdirc/commandparser/CommandMana ger.commandChar)
pre	(soft) init'ed(com/dmdirc/commandparser/CommandMana ger.silenceChar)
pre	init'ed(this.words)
pre	this.line != null
presumption	getWords(...).length@190 >= 1
presumption	getWords(...)[0]@190 != null
post	init'ed(java.lang.String:split(...)._tainted)
post	init'ed(java.lang.String:split(...).length)
post	init'ed(java.lang.String:split(...)[0])
post	init'ed(java.lang.String:substring(...)._tainted)
post	return_value == &java.lang.String:substring(... )
post	this.words != null
post	this.words == One-of{old this.words, &java.lang.String:split(...)}
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split

String getLine()

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

String getStrippedLine()

Kind	Annotation Text
pre	(soft) init'ed(com/dmdirc/commandparser/CommandMana ger.commandChar)
pre	(soft) init'ed(com/dmdirc/commandparser/CommandMana ger.silenceChar)
pre	this.line != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	java.lang.String:substring(...)._tainted == this.line._tainted
post	return_value == &java.lang.String:substring(... )
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:length

String[] getWords()

Kind	Annotation Text
pre	(soft) this.line != null
pre	init'ed(this.words)
post	init'ed(java.lang.String:split(...)._tainted)
post	return_value != null
post	return_value == One-of{old this.words, &java.lang.String:split(...)}
post	this.words == return_value
unanalyzed	call on java.lang.String:split

String getWordsAsString(int)

Kind	Annotation Text
pre	this.words != null
pre	this.words.length - start in {-2³¹.. 2³²-1}
pre	this.words.length <= 2³²-1
post	init'ed(return_value)
unanalyzed	call on java.util.regex.Matcher:group
unanalyzed	call on java.util.regex.Matcher:matches
unanalyzed	call on java.util.regex.Pattern:compile
unanalyzed	call on java.util.regex.Pattern:matcher

String getWordsAsString(int, int)

Kind	Annotation Text
pre	end - start in {-2³¹..2³²-1}
presumption	java.util.regex.Pattern:compile(...)@148 != null
presumption	java.util.regex.Pattern:matcher(...)@150 != null
post	init'ed(return_value)

bool isCommand()

Kind	Annotation Text
pre	(soft) init'ed(com/dmdirc/commandparser/CommandMana ger.commandChar)
pre	this.line != null
post	init'ed(return_value)

bool isSilent()

Kind	Annotation Text
pre	(soft) init'ed(com/dmdirc/commandparser/CommandMana ger.commandChar)
pre	(soft) init'ed(com/dmdirc/commandparser/CommandMana ger.silenceChar)
pre	this.line != null
post	init'ed(return_value)
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:isEmpty

Kind	Annotation Text
pre	(soft) this.line != null
pre	init'ed(this.words)
post	init'ed(java.lang.String:split(...)._tainted)
post	this.words != null
post	this.words == One-of{old this.words, &java.lang.String:split(...)}
test_vector	this.words: Inverse{null}, Addr_Set{null}