method

com.dmdirc.addons.ui_swing.textpane.LineInfo__ static_init

method	void com.dmdirc.addons.ui_swing.textpane. LineInfo(int, int)
post	this.index == -1
post	this.line == line
post	init'ed(this.line)
post	this.part == part
post	init'ed(this.part)

method	void com.dmdirc.addons.ui_swing.textpane. LineInfo(int, int, int)
post	this.index == index
post	init'ed(this.index)
post	this.line == line
post	init'ed(this.line)
post	this.part == part
post	init'ed(this.part)

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

method	int getPart()
pre	init'ed(this.part)
post	return_value == this.part
post	init'ed(return_value)

method	int getIndex()
pre	init'ed(this.index)
post	return_value == this.index
post	init'ed(return_value)

method	void setIndex(int)
post	this.index == index
post	init'ed(this.index)

method	void setLine(int)
post	this.line == line
post	init'ed(this.line)

method	void setPart(int)
post	this.part == part
post	init'ed(this.part)

method	String toString()
pre	init'ed(this.index)
pre	init'ed(this.line)
pre	init'ed(this.part)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuilder:toStri ng(...)