method

com.dmdirc.commandparser.CommandArguments__static_ init

method	void com.dmdirc.commandparser.CommandArguments(Str ing)
post	this.line == line
post	init'ed(this.line)

method	String getLine()
post	return_value == this.line
post	init'ed(return_value)

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

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

method	String[] getArguments()
pre	init'ed(this.words)
pre	(soft) this.line != null
presumption	this.words.length@97 <= 232-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 == One-of{old this.words, &amp;java.lang.String:split(...)}
post	this.words != null
unanalyzed	call on java.lang.String:split

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

method	String getArgumentsAsString(int)
pre	init'ed(this.words)
pre	start <= 232-2
pre	(soft) this.line != null
presumption	this.words.length@123 <= 232-1
presumption	this.words.length@123 - start in {-231+1.. 232}
post	init'ed(java.lang.String:split(...)._tainted)
post	init'ed(java.lang.String:split(...).length)
post	init'ed(return_value)
post	this.words == One-of{old this.words, &amp;java.lang.String:split(...)}
post	this.words != null
unanalyzed	call on java.util.regex.Pattern:compile
unanalyzed	call on java.util.regex.Pattern:matcher
unanalyzed	call on java.util.regex.Matcher:matches
unanalyzed	call on java.util.regex.Matcher:group
unanalyzed	call on java.lang.String:split

method	String getWordsAsString(int)
pre	this.words != null
pre	this.words.length <= 232-1
pre	this.words.length - start in {-231.. 232-1}
post	init'ed(return_value)
unanalyzed	call on java.util.regex.Pattern:compile
unanalyzed	call on java.util.regex.Pattern:matcher
unanalyzed	call on java.util.regex.Matcher:matches
unanalyzed	call on java.util.regex.Matcher:group

method	String getWordsAsString(int, int)
pre	end - start in {-231..232-1}
presumption	java.util.regex.Pattern:compile(...)@148 != null
presumption	java.util.regex.Pattern:matcher(...)@150 != null
post	init'ed(return_value)

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

method	bool isCommand()
pre	this.line != null
pre	(soft) init'ed(com/dmdirc/commandparser/CommandMana ger.commandChar)
post	init'ed(return_value)

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

method	String getCommandName()
pre	init'ed(this.words)
pre	this.line != null
pre	(soft) init'ed(com/dmdirc/commandparser/CommandMana ger.commandChar)
pre	(soft) init'ed(com/dmdirc/commandparser/CommandMana ger.silenceChar)
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 == One-of{old this.words, &java.lang.String:split(...)}
post	this.words != null
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:length