LinePosition.java

LinePosition.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void com.dmdirc.addons.ui_swing.textpane.LinePosition(int, int, int, int)

Kind	Annotation Text
post	init'ed(this.endLine)
post	init'ed(this.endPos)
post	init'ed(this.startLine)
post	init'ed(this.startPos)
post	this.endLine == endLine
post	this.endPos == endPos
post	this.startLine == startLine
post	this.startPos == startPos

void com.dmdirc.addons.ui_swing.textpane.LinePosition(LinePosition)

Kind	Annotation Text
pre	init'ed(position.endLine)
pre	init'ed(position.endPos)
pre	init'ed(position.startLine)
pre	init'ed(position.startPos)
pre	position != null
post	init'ed(this.endLine)
post	init'ed(this.endPos)
post	init'ed(this.startLine)
post	init'ed(this.startPos)
post	this.endLine == position.endLine
post	this.endPos == position.endPos
post	this.startLine == position.startLine
post	this.startPos == position.startPos

com.dmdirc.addons.ui_swing.textpane.LinePosition__static_init

Kind	Annotation Text

int getEndLine()

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

int getEndPos()

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

int getStartLine()

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

int getStartPos()

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

void setEndLine(int)

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

void setEndPos(int)

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

void setStartLine(int)

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

void setStartPos(int)

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

String toString()

Kind	Annotation Text
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(...)