Messages

Last Msg First Msg

method

com.dmdirc.addons.ui_swing.textpane. IRCDocumentSearcher__static_init

method	void com.dmdirc.addons.ui_swing.textpane. IRCDocumentSearcher(String, IRCDocument, bool)
pre	document != null
pre	document.lines != null
presumption	java.util.List:size(...)@78 in {-2³¹+1.. 2³²-1}
post	this.caseSensitive == caseSensitive
post	init'ed(this.caseSensitive)
post	this.document == document
post	this.document != null
post	this.phrase == phrase
post	init'ed(this.phrase)
post	this.position == &new LinePosition(getEndPositi on#1)
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	init'ed(new LinePosition(getEndPosition#1).endPos)
post	new LinePosition(getEndPosition#1).startPos == new LinePosition(getEndPosition#1).endPos
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.lang.String:length

method	LinePosition getEndPosition()
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	return_value == &new LinePosition(getEndPositio n#1)
post	new LinePosition(getEndPosition#1) num objects == 1
post	return_value.endLine <= 2³²-2
post	return_value.startLine == return_value.endLine
post	init'ed(return_value.endPos)
post	return_value.startPos == return_value.endPos
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.lang.String:length
test_vector	java.util.List:size(...)@78: {-2³¹+1..0}, {1..2³²-1}

method	void setPosition(LinePosition)
post	this.position == position
post	init'ed(this.position)

method	LinePosition searchUp()
pre	init'ed(this.position)
pre	this.document != null
pre	this.document.lines != null
pre	(soft) init'ed(this.position.endLine)
pre	(soft) init'ed(this.position.endPos)
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(return_value)
post	this.position == One-of{old this.position, &new LinePosition(getEndPosition#1)}
post	this.position != null
post	new LinePosition(getEndPosition#1) num objects <= 1
post	new LinePosition(getEndPosition#1).endLine <= 2³²-2
post	init'ed(new LinePosition(getEndPosition#1).endPos)
post	new LinePosition(getEndPosition#1).startLine <= 2³²-2
post	init'ed(new LinePosition(getEndPosition#1). startPos)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.regex.Pattern:compile
unanalyzed	call on java.util.regex.Pattern:matcher
unanalyzed	call on java.util.regex.Matcher:find
unanalyzed	call on java.util.regex.Matcher:start
unanalyzed	call on java.util.regex.Matcher:end
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on com.dmdirc.ui.messages.Styliser:stipControl Codes
unanalyzed	call on java.lang.String:length
test_vector	this.position: Inverse{null}, Addr_Set{null}

Prev Msg Next Msg

precondition failure

click for all messages in this file High Prob.

com/dmdirc/addons/ui_swing/textpane/Line.getText: this.lineParts != null

Prev Msg Next Msg

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

Prev Msg Next Msg

precondition failure

click for all messages in this file High Prob.

com/dmdirc/addons/ui_swing/textpane/Line.getText: this.lineParts != null

Prev Msg Next Msg

Prev Msg Next Msg

overflow

click for all messages in this file Low Prob.

check that line in {-2³¹-1..2³²-2}

Prev Msg Next Msg

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