IRCDocumentSearcher.java

IRCDocumentSearcher.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

Kind	Annotation Text
pre	document != null
pre	document.lines != null
presumption	java.util.List:size(...)@78 in {-2³¹+1.. 2³²-1}
post	init'ed(new LinePosition(getEndPosition#1).endPos)
post	init'ed(this.caseSensitive)
post	init'ed(this.phrase)
post	new LinePosition(getEndPosition#1) num objects == 1
post	new LinePosition(getEndPosition#1).endLine <= 2³²-2
post	new LinePosition(getEndPosition#1).startLine == new LinePosition(getEndPosition#1).endLine
post	new LinePosition(getEndPosition#1).startPos == new LinePosition(getEndPosition#1).endPos
post	this.caseSensitive == caseSensitive
post	this.document != null
post	this.document == document
post	this.phrase == phrase
post	this.position == &new LinePosition(getEndPositi on#1)
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:size

Kind	Annotation Text

Kind	Annotation Text
pre	this.document != null
pre	this.document.lines != null
presumption	getLine(...).lineParts != null
presumption	getLine(...).lineParts.length <= 2³²-1
presumption	getLine(...).lineParts[...] != null
presumption	java.util.List:get(...)@89 != null
presumption	java.util.List:size(...)@78 >= -2³¹+1
presumption	java.util.List:size(...)@78 in {-2³¹+1.. 2³²-1}
post	init'ed(return_value.endPos)
post	new LinePosition(getEndPosition#1) num objects == 1
post	return_value == &new LinePosition(getEndPositio n#1)
post	return_value.endLine <= 2³²-2
post	return_value.startLine == return_value.endLine
post	return_value.startPos == return_value.endPos
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:size
test_vector	java.util.List:size(...)@78: {-2³¹+1..0}, {1..2³²-1}

Kind	Annotation Text
pre	(soft) init'ed(this.position.startLine)
pre	(soft) init'ed(this.position.startPos)
pre	init'ed(this.position)
pre	this.document != null
pre	this.document.lines != null
presumption	getEndPosition(...)@133 init'ed
presumption	getLine(...).lineParts.length <= 2³²-1
presumption	java.util.Iterator:next(...)@145 != null
presumption	java.util.List:get(...)@89 != null
presumption	line - java.util.List:size(...)@78 in {-2³¹-1..2³²-2, 6_442_450_943}
post	init'ed(new LinePosition(getEndPosition#1).endPos)
post	init'ed(new LinePosition(getEndPosition#1). startPos)
post	init'ed(return_value)
post	new LinePosition(getEndPosition#1) num objects <= 1
post	new LinePosition(getEndPosition#1).endLine <= 2³²-2
post	new LinePosition(getEndPosition#1).startLine <= 2³²-2
post	this.position != null
post	this.position == One-of{old this.position, &new LinePosition(getEndPosition#1)}
unanalyzed	call on com.dmdirc.ui.messages.Styliser:stipControl Codes
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.regex.Matcher:end
unanalyzed	call on java.util.regex.Matcher:find
unanalyzed	call on java.util.regex.Matcher:start
unanalyzed	call on java.util.regex.Pattern:compile
unanalyzed	call on java.util.regex.Pattern:matcher
test_vector	java.util.Iterator:hasNext(...)@145: {0}, {1}
test_vector	this.position: Inverse{null}, Addr_Set{null}

Kind	Annotation Text
presumption	java.util.regex.Pattern:compile(...)@171 != null
presumption	java.util.regex.Pattern:matcher(...)@171 != null
post	new ArrayList(searchLine#1) num objects == 1
post	return_value == &new ArrayList(searchLine#1)
test_vector	java.util.regex.Matcher:find(...)@174: {0}, {1}

Kind	Annotation Text
pre	(soft) init'ed(this.position.endLine)
pre	(soft) init'ed(this.position.endPos)
pre	init'ed(this.position)
pre	this.document != null
pre	this.document.lines != null
presumption	getEndPosition(...)@96 init'ed
presumption	getLine(...).lineParts.length <= 2³²-1
presumption	java.util.List:get(...)@109 != null
presumption	java.util.List:get(...)@89 != null
presumption	java.util.List:size(...)@108 >= -2³¹+1
presumption	java.util.List:size(...)@78 + line in {-2³¹+1..8_589_934_590}
post	init'ed(new LinePosition(getEndPosition#1).endPos)
post	init'ed(new LinePosition(getEndPosition#1). startPos)
post	init'ed(return_value)
post	new LinePosition(getEndPosition#1) num objects <= 1
post	new LinePosition(getEndPosition#1).endLine <= 2³²-2
post	new LinePosition(getEndPosition#1).startLine <= 2³²-2
post	this.position != null
post	this.position == One-of{old this.position, &new LinePosition(getEndPosition#1)}
unanalyzed	call on com.dmdirc.ui.messages.Styliser:stipControl Codes
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.regex.Matcher:end
unanalyzed	call on java.util.regex.Matcher:find
unanalyzed	call on java.util.regex.Matcher:start
unanalyzed	call on java.util.regex.Pattern:compile
unanalyzed	call on java.util.regex.Pattern:matcher
test_vector	this.position: Inverse{null}, Addr_Set{null}

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