method

com.dmdirc.addons.ui_swing.textpane.LinePosition__ static_init

method	void com.dmdirc.addons.ui_swing.textpane. LinePosition(int, int, int, int)
post	this.endLine == endLine
post	init'ed(this.endLine)
post	this.endPos == endPos
post	init'ed(this.endPos)
post	this.startLine == startLine
post	init'ed(this.startLine)
post	this.startPos == startPos
post	init'ed(this.startPos)

method	void com.dmdirc.addons.ui_swing.textpane. LinePosition(LinePosition)
pre	position != null
pre	init'ed(position.endLine)
pre	init'ed(position.endPos)
pre	init'ed(position.startLine)
pre	init'ed(position.startPos)
post	this.endLine == position.endLine
post	init'ed(this.endLine)
post	this.endPos == position.endPos
post	init'ed(this.endPos)
post	this.startLine == position.startLine
post	init'ed(this.startLine)
post	this.startPos == position.startPos
post	init'ed(this.startPos)

method	int getEndLine()
pre	init'ed(this.endLine)
post	return_value == this.endLine
post	init'ed(return_value)

method	int getEndPos()
pre	init'ed(this.endPos)
post	return_value == this.endPos
post	init'ed(return_value)

method	int getStartLine()
pre	init'ed(this.startLine)
post	return_value == this.startLine
post	init'ed(return_value)

method	int getStartPos()
pre	init'ed(this.startPos)
post	return_value == this.startPos
post	init'ed(return_value)

method	void setEndLine(int)
post	this.endLine == endLine
post	init'ed(this.endLine)

method	void setEndPos(int)
post	this.endPos == endPos
post	init'ed(this.endPos)

method	void setStartLine(int)
post	this.startLine == startLine
post	init'ed(this.startLine)

method	void setStartPos(int)
post	this.startPos == startPos
post	init'ed(this.startPos)

method	String toString()
pre	init'ed(this.endLine)
pre	init'ed(this.endPos)
pre	init'ed(this.startLine)
pre	init'ed(this.startPos)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuilder:toStri ng(...)