LineInfo.java

LineInfo.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.LineInfo(int, int)

Kind	Annotation Text
post	init'ed(this.line)
post	init'ed(this.part)
post	this.index == -1
post	this.line == line
post	this.part == part

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

Kind	Annotation Text
post	init'ed(this.index)
post	init'ed(this.line)
post	init'ed(this.part)
post	this.index == index
post	this.line == line
post	this.part == part

com.dmdirc.addons.ui_swing.textpane.LineInfo__static_init

Kind	Annotation Text

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

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

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

void setIndex(int)

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

void setLine(int)

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

void setPart(int)

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

String toString()

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