method

com.dmdirc.parser.irc.ParserError__static_init

method	void com.dmdirc.parser.irc.ParserError(int, String, String)
post	this.errorData == data
post	init'ed(this.errorData)
post	this.errorLevel == level
post	init'ed(this.errorLevel)
post	this.lastLine == line
post	init'ed(this.lastLine)

method	bool isFatal()
pre	init'ed(this.errorLevel)
post	init'ed(return_value)

method	bool isError()
pre	init'ed(this.errorLevel)
post	init'ed(return_value)

method	bool isWarning()
pre	init'ed(this.errorLevel)
post	init'ed(return_value)

method	bool isUserError()
pre	init'ed(this.errorLevel)
post	init'ed(return_value)

method	bool isException()
pre	init'ed(this.errorLevel)
post	init'ed(return_value)

method	bool hasLastLine()
pre	init'ed(this.lastLine)
post	init'ed(return_value)

method	void setException(Exception)
pre	(soft) this.errorLevel <= 4_294_967_279
post	this.errorLevel == One-of{old this.errorLevel, old this.errorLevel + 16}
post	init'ed(this.errorLevel)
post	this.exceptionInfo == newException
post	init'ed(this.exceptionInfo)
test_vector	this.errorLevel &amp; 16: {16}, {0..15}

method	Exception getException()
pre	init'ed(this.exceptionInfo)
post	return_value == this.exceptionInfo
post	init'ed(return_value)

method	int getLevel()
pre	init'ed(this.errorLevel)
post	return_value == this.errorLevel
post	init'ed(return_value)

method	String getData()
pre	init'ed(this.errorData)
post	return_value == this.errorData
post	init'ed(return_value)

method	void appendData(String)
pre	init'ed(this.errorData)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	this.errorData == &java.lang.StringBuilder:toSt ring(...)

method	String getLastLine()
pre	init'ed(this.lastLine)
post	return_value == this.lastLine
post	init'ed(return_value)