Messages

Last Msg First Msg

method

org.apache.roller.weblogger.util.LinkbackExtractor $LinkbackCallback__static_init

method

org.apache.roller.weblogger.util.LinkbackExtractor $1__static_init

method	bool access$100(LinkbackExtractor)
pre	x0 != null
pre	init'ed(x0.mFound)
post	return_value == x0.mFound
post	init'ed(return_value)

method	int access$202(LinkbackExtractor, int)
pre	x0 != null
post	return_value == x1
post	init'ed(return_value)
post	x0.mStart == return_value

method	int access$300(LinkbackExtractor)
pre	x0 != null
pre	init'ed(x0.mEnd)
post	return_value == x0.mEnd
post	init'ed(return_value)

method	int access$302(LinkbackExtractor, int)
pre	x0 != null
post	return_value == x1
post	init'ed(return_value)
post	x0.mEnd == return_value

method	String access$400(LinkbackExtractor)
pre	x0 != null
pre	init'ed(x0.mRequestURL)
post	return_value == x0.mRequestURL
post	init'ed(return_value)

method	String access$500(LinkbackExtractor)
pre	x0 != null
pre	init'ed(x0.mRequestURLWWW)
post	return_value == x0.mRequestURLWWW
post	init'ed(return_value)

method	bool access$102(LinkbackExtractor, bool)
pre	x0 != null
post	return_value == x1
post	init'ed(return_value)
post	x0.mFound == return_value

method	String access$602(LinkbackExtractor, String)
pre	x0 != null
post	return_value == x1
post	init'ed(return_value)
post	x0.mRssLink == return_value

method	Log access$700()
pre	init'ed(mLogger)
post	return_value == mLogger
post	init'ed(return_value)

method	String access$600(LinkbackExtractor)
pre	x0 != null
pre	init'ed(x0.mRssLink)
post	return_value == x0.mRssLink
post	init'ed(return_value)

method	String access$800(LinkbackExtractor)
pre	x0 != null
pre	init'ed(x0.mRefererURL)
post	return_value == x0.mRefererURL
post	init'ed(return_value)

method	String access$900(LinkbackExtractor)
pre	x0 != null
pre	init'ed(x0.mTitle)
post	return_value == x0.mTitle
post	init'ed(return_value)

method	String access$984(LinkbackExtractor, Object)
pre	init'ed(x0.mTitle)
pre	x0 != null
post	java.lang.StringBuilder:toString(...)._tainted == x0.mTitle._tainted \| x1._tainted
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &java.lang.StringBuilder:toStri ng(...)
post	x0.mTitle == &java.lang.StringBuilder:toString( ...)

method	org.apache.roller.weblogger.util.LinkbackExtractor __static_init
presumption	org.apache.commons.logging.LogFactory:getFactory(.. .)@53 != null
post	init'ed(mLogger)

info method not available -- call on LogFactory org.apache.commons.logging. LogFactory:getFactory()

info method not available -- call on Log org.apache.commons.logging. LogFactory:getInstance(Class)

method	void org.apache.roller.weblogger.util. LinkbackExtractor(String, String)
pre	(soft) mLogger != null
pre	(soft) requestURL != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	init'ed(java.lang.String:toString(...)._tainted)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	this.mEnd == 0
post	this.mStart == 0
post	init'ed(this.mExcerpt)
post	init'ed(this.mFound)
post	this.mMaxExcerpt == 500
post	init'ed(this.mPermalink)
post	this.mRefererURL == One-of{refererURL, undefined}
post	this.mRequestURL == One-of{&java.lang. StringBuilder:toString(...), requestURL, null}
post	init'ed(this.mRequestURL)
post	this.mRequestURLWWW == One-of{requestURL, &java.lang.StringBuilder:toString(...), null}
post	init'ed(this.mRequestURLWWW)
post	this.mRssLink == null
post	init'ed(this.mTitle)
unanalyzed	call on com.sun.syndication.io.SyndFeedInput
unanalyzed	call on java.net.URL
unanalyzed	call on java.net.URL:openStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on com.sun.syndication.io.SyndFeedInput:build
unanalyzed	call on com.sun.syndication.feed.synd. SyndFeed:getEntries
unanalyzed	call on java.util.List:iterator
unanalyzed	call on com.sun.syndication.feed.synd. SyndFeed:getTitle
unanalyzed	call on org.apache.commons.logging.Log:isDebugEnabl ed
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on com.sun.syndication.feed.synd. SyndEntry:getDescription
unanalyzed	call on com.sun.syndication.feed.synd. SyndContent:getValue
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on com.sun.syndication.feed.synd. SyndEntry:getLink
unanalyzed	call on java.lang.String:toString
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:length
unanalyzed	call on com.sun.syndication.feed.synd. SyndEntry:getTitle
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on javax.swing.text.html.HTMLEditorKit
unanalyzed	call on javax.swing.text.html.HTMLEditorKit:getPars er
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on java.io.BufferedReader:readLine
unanalyzed	call on java.io.BufferedReader:close
unanalyzed	call on java.io.StringReader
unanalyzed	call on javax.swing.text.html.HTMLEditorKit$ParserC allback
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on javax.swing.text.html.HTMLEditorKit$Parser: parse
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
test_vector	this.mRssLink: Addr_Set{null}, Inverse{null}

info method not available -- call on bool org.apache.commons.logging. Log:isDebugEnabled()

info method not available -- call on void org.apache.commons.logging. Log:debug(Object, Throwable)

method	void extractByParsingHtml(String, String)
pre	this.mTitle != null
pre	requestURL != null
pre	init'ed(this.mStart)
pre	(soft) init'ed(this.mEnd)
pre	(soft) init'ed(this.mMaxExcerpt)
presumption	javax.swing.text.html.HTMLEditorKit:getParser(... )@118 != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	possibly_updated(this.mExcerpt)
post	this.mRefererURL == refererURL
post	init'ed(this.mRefererURL)
post	this.mRequestURL == One-of{&java.lang. StringBuilder:toString(...), requestURL}
post	this.mRequestURL != null
post	this.mRequestURLWWW == One-of{requestURL, &java.lang.StringBuilder:toString(...)}
post	this.mRequestURLWWW != null
post	this.mTitle == One-of{old this.mTitle, &java.lang.String:substring(...)}
post	this.mTitle != null
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim
unanalyzed	call on javax.swing.text.html.HTMLEditorKit
unanalyzed	call on javax.swing.text.html.HTMLEditorKit:getPars er
unanalyzed	call on javax.swing.text.html.HTMLEditorKit$ParserC allback
unanalyzed	call on java.util.Arrays:asList
test_vector	this.mEnd: {0}, {-2³¹+1..-1, 1..2³²-1}
test_vector	this.mEnd - this.mStart: {-6_442_450_943..0}, {1..6_442_450_943}
test_vector	this.mStart: {0}, {-2³¹..-1, 1..2³²-2}
test_vector	java.io.BufferedReader:readLine(...)@129: Inverse{null}, Addr_Set{null}
test_vector	java.lang.String:length(...)@155: {0,1}, {2..2³²-1}
test_vector	java.lang.String:startsWith(...)@103: {0}, {1}
test_vector	java.lang.String:startsWith(...)@155: {0}, {1}

method

void org.apache.roller.weblogger.util. LinkbackExtractor$1(LinkbackExtractor)

method	HTMLEditorKit$Parser getParser()
post	init'ed(return_value)

method	void extractByParsingRss(String, String)
pre	mLogger != null
pre	(soft) init'ed(this.mFound)
pre	(soft) init'ed(this.mMaxExcerpt)
presumption	com.sun.syndication.feed.synd.SyndContent:getValue( ...)@182 != null
presumption	com.sun.syndication.feed.synd.SyndEntry:getDescript ion(...)@182 != null
presumption	com.sun.syndication.feed.synd.SyndEntry:getDescript ion(...)@194 != null
presumption	com.sun.syndication.feed.synd.SyndEntry:getLink(... )@185 != null
presumption	com.sun.syndication.feed.synd.SyndFeed:getEntries(. ..)@168 != null
presumption	com.sun.syndication.io.SyndFeedInput:build(... )@166 != null
presumption	java.util.Iterator:next(...)@181 != null
post	init'ed(java.lang.String:toString(...)._tainted)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	possibly_updated(this.mExcerpt)
post	(soft) init'ed(this.mFound)
post	this.mPermalink == One-of{old this.mPermalink, &java.lang.String:toString(...)}
post	possibly_updated(this.mTitle)
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim
test_vector	com.sun.syndication.feed.synd.SyndFeed:getTitle(... )@169: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:indexOf(...)@182: {-1}, {-2³¹..-2, 0..2³²-1}
test_vector	java.lang.String:length(...)@186: {0}, {1..2³²-1}
test_vector	java.util.Iterator:hasNext(...)@178: {0}, {1}
test_vector	org.apache.commons.logging.Log:isDebugEnabled(... )@173: {0}, {1}
test_vector	org.apache.commons.logging.Log:isDebugEnabled(... )@204: {0}, {1}

info method not available -- call on void com.sun.syndication.io. SyndFeedInput()

info method not available -- call on SyndFeed com.sun.syndication.io. SyndFeedInput:build(Reader)

info method not available -- call on List com.sun.syndication.feed.synd. SyndFeed:getEntries()

info method not available -- call on String com.sun.syndication.feed.synd. SyndFeed:getTitle()

info method not available -- call on bool org.apache.commons.logging. Log:isDebugEnabled()

info method not available -- call on void org.apache.commons.logging. Log:debug(Object)

Prev Msg Next Msg

+

click for all messages in this file low

overflow check might fail: requires count in -2³¹-1..2³²-2

Prev Msg Next Msg

info method not available -- call on SyndContent com.sun.syndication.feed. synd.SyndEntry:getDescription()

info method not available -- call on String com.sun.syndication.feed.synd. SyndContent:getValue()

info method not available -- call on String com.sun.syndication.feed.synd. SyndEntry:getLink()

info method not available -- call on String com.sun.syndication.feed.synd. SyndEntry:getTitle()

info method not available -- call on bool org.apache.commons.logging. Log:isDebugEnabled()

info method not available -- call on void org.apache.commons.logging. Log:debug(Object)

method	String getExcerpt()
pre	init'ed(this.mExcerpt)
post	return_value == this.mExcerpt
post	init'ed(return_value)

method	String getTitle()
pre	init'ed(this.mTitle)
post	return_value == this.mTitle
post	init'ed(return_value)

method	String getPermalink()
pre	init'ed(this.mPermalink)
post	return_value == this.mPermalink
post	init'ed(return_value)

method	void setPermalink(String)
post	this.mPermalink == permalink
post	init'ed(this.mPermalink)

method	void org.apache.roller.weblogger.util. LinkbackExtractor$LinkbackCallback(LinkbackExtracto r)
presumption	init'ed(javax.swing.text.html.HTML$Tag.BLOCKQUOTE)
presumption	init'ed(javax.swing.text.html.HTML$Tag.BR)
presumption	init'ed(javax.swing.text.html.HTML$Tag.DIV)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H1)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H2)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H3)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H4)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H5)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H6)
presumption	init'ed(javax.swing.text.html.HTML$Tag.HR)
presumption	init'ed(javax.swing.text.html.HTML$Tag.LI)
presumption	init'ed(javax.swing.text.html.HTML$Tag.P)
presumption	init'ed(javax.swing.text.html.HTML$Tag.PRE)
presumption	init'ed(javax.swing.text.html.HTML$Tag.SPAN)
presumption	init'ed(javax.swing.text.html.HTML$Tag.TD)
post	this.mCurrentTag == null
post	this.mDivTags == &new HTML$Tag[](LinkbackExtrac tor$LinkbackCallback#1)
post	init'ed(this.mList)
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 ) num objects == 1
post	this.mDivTags.length == 15
post	this.mDivTags[0] == javax.swing.text.html.HTML$Tag. TD
post	(soft) init'ed(this.mDivTags[0])
post	this.mDivTags[10] == javax.swing.text.html. HTML$Tag.H2
post	(soft) init'ed(this.mDivTags[10])
post	this.mDivTags[11] == javax.swing.text.html. HTML$Tag.H3
post	(soft) init'ed(this.mDivTags[11])
post	this.mDivTags[12] == javax.swing.text.html. HTML$Tag.H4
post	(soft) init'ed(this.mDivTags[12])
post	this.mDivTags[13] == javax.swing.text.html. HTML$Tag.H5
post	(soft) init'ed(this.mDivTags[13])
post	this.mDivTags[14] == javax.swing.text.html. HTML$Tag.H6
post	(soft) init'ed(this.mDivTags[14])
post	this.mDivTags[1] == javax.swing.text.html.HTML$Tag. DIV
post	(soft) init'ed(this.mDivTags[1])
post	this.mDivTags[2] == javax.swing.text.html.HTML$Tag. SPAN
post	(soft) init'ed(this.mDivTags[2])
post	this.mDivTags[3] == javax.swing.text.html.HTML$Tag. BLOCKQUOTE
post	(soft) init'ed(this.mDivTags[3])
post	this.mDivTags[4] == javax.swing.text.html.HTML$Tag. P
post	(soft) init'ed(this.mDivTags[4])
post	this.mDivTags[5] == javax.swing.text.html.HTML$Tag. LI
post	(soft) init'ed(this.mDivTags[5])
post	this.mDivTags[6] == javax.swing.text.html.HTML$Tag. BR
post	(soft) init'ed(this.mDivTags[6])
post	this.mDivTags[7] == javax.swing.text.html.HTML$Tag. HR
post	(soft) init'ed(this.mDivTags[7])
post	this.mDivTags[8] == javax.swing.text.html.HTML$Tag. PRE
post	(soft) init'ed(this.mDivTags[8])
post	this.mDivTags[9] == javax.swing.text.html.HTML$Tag. H1
post	(soft) init'ed(this.mDivTags[9])

method	void org.apache.roller.weblogger.util. LinkbackExtractor$LinkbackCallback(LinkbackExtracto r, LinkbackExtractor$1)
presumption	init'ed(javax.swing.text.html.HTML$Tag.BLOCKQUOTE)
presumption	init'ed(javax.swing.text.html.HTML$Tag.BR)
presumption	init'ed(javax.swing.text.html.HTML$Tag.DIV)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H1)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H2)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H3)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H4)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H5)
presumption	init'ed(javax.swing.text.html.HTML$Tag.H6)
presumption	init'ed(javax.swing.text.html.HTML$Tag.HR)
presumption	init'ed(javax.swing.text.html.HTML$Tag.LI)
presumption	init'ed(javax.swing.text.html.HTML$Tag.P)
presumption	init'ed(javax.swing.text.html.HTML$Tag.PRE)
presumption	init'ed(javax.swing.text.html.HTML$Tag.SPAN)
presumption	init'ed(javax.swing.text.html.HTML$Tag.TD)
post	this.mCurrentTag == null
post	this.mDivTags == &new HTML$Tag[](LinkbackExtrac tor$LinkbackCallback#1)
post	init'ed(this.mList)
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 ) num objects == 1
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 ).length == 15
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[0] == javax.swing.text.html.HTML$Tag.TD
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[0])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[10] == javax.swing.text.html.HTML$Tag.H2
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[10])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[11] == javax.swing.text.html.HTML$Tag.H3
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[11])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[12] == javax.swing.text.html.HTML$Tag.H4
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[12])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[13] == javax.swing.text.html.HTML$Tag.H5
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[13])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[14] == javax.swing.text.html.HTML$Tag.H6
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[14])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[1] == javax.swing.text.html.HTML$Tag.DIV
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[1])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[2] == javax.swing.text.html.HTML$Tag.SPAN
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[2])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[3] == javax.swing.text.html.HTML$Tag.BLOCKQUOTE
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[3])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[4] == javax.swing.text.html.HTML$Tag.P
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[4])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[5] == javax.swing.text.html.HTML$Tag.LI
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[5])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[6] == javax.swing.text.html.HTML$Tag.BR
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[6])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[7] == javax.swing.text.html.HTML$Tag.HR
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[7])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[8] == javax.swing.text.html.HTML$Tag.PRE
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[8])
post	new HTML$Tag[](LinkbackExtractor$LinkbackCallback#1 )[9] == javax.swing.text.html.HTML$Tag.H1
post	init'ed(new HTML$Tag[](LinkbackExtractor$LinkbackCa llback#1)[9])
unanalyzed	call on javax.swing.text.html.HTMLEditorKit$ParserC allback
unanalyzed	call on java.util.Arrays:asList

method	void handleStartTag(HTML$Tag, MutableAttributeSet, int)
pre	this.mList != null
pre	(soft) atts != null
pre	(soft) init'ed(this.mEnd)
pre	(soft) init'ed(this.mFound)
pre	(soft) tag != null
pre	(soft) init'ed(this.mRequestURL)
pre	(soft) init'ed(this.mRequestURLWWW)
presumption	init'ed(javax.swing.text.html.HTML$Attribute.HREF)
presumption	init'ed(javax.swing.text.html.HTML$Tag.A)
post	this.mCurrentTag == One-of{old this.mCurrentTag, tag}
post	this.mEnd == One-of{old this.mEnd, pos}
post	(soft) init'ed(this.mEnd)
post	(soft) init'ed(this.mFound)
post	this.mStart == One-of{old this.mStart, pos}
test_vector	this.mEnd: {-2³¹..-1, 1..2³²-1}, {0}
test_vector	this.mFound: {1}, {0}
test_vector	java.lang.Object:equals(...)@298: {0}, {1}
test_vector	java.lang.String:equals(...)@308: {1}, {0}
test_vector	java.lang.String:equals(...)@308: {0}, {1}
test_vector	java.lang.String:lastIndexOf(...)@303: {-1}, {-2³¹..-2, 0..2³²-1}
test_vector	java.util.List:contains(...)@290: {0}, {1}
test_vector	java.util.List:contains(...)@294: {0}, {1}
test_vector	javax.swing.text.MutableAttributeSet:getAttribute(. ..)@300: Inverse{null}, Addr_Set{null}

Prev Msg Next Msg

+

click for all messages in this file warning

test always goes same way test predetermined because href != null

Prev Msg Next Msg

method	void handleSimpleTag(HTML$Tag, MutableAttributeSet , int)
pre	this.mList != null
pre	(soft) atts != null
pre	(soft) init'ed(this.mEnd)
pre	(soft) org/apache/roller/weblogger/util/LinkbackExt ractor.mLogger != null
pre	(soft) tag != null
pre	(soft) init'ed(this.mFound)
pre	(soft) this.mRefererURL != null
presumption	javax.swing.text.MutableAttributeSet:getAttribute(. ..)@343 != null
presumption	init'ed(javax.swing.text.html.HTML$Attribute.HREF)
presumption	init'ed(javax.swing.text.html.HTML$Attribute. TITLE)
presumption	init'ed(javax.swing.text.html.HTML$Attribute.TYPE)
presumption	init'ed(javax.swing.text.html.HTML$Tag.LINK)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	(soft) init'ed(this.mEnd)
post	possibly_updated(this.mRssLink)
test_vector	this.mEnd: {-2³¹..-1, 1..2³²-1}, {0}
test_vector	this.mFound: {0}, {1}
test_vector	java.lang.Object:equals(...)@334: {0}, {1}
test_vector	java.lang.String:equals(...)@339: {0}, {1}
test_vector	java.lang.String:lastIndexOf(...)@370: {-1}, {-2³¹..-2, 0..2³²-1}
test_vector	java.lang.String:length(...)@350: {0,1}, {2..2³²-1}
test_vector	java.lang.String:startsWith(...)@350: {0}, {1}
test_vector	java.lang.String:startsWith(...)@368: {1}, {0}
test_vector	java.util.List:contains(...)@330: {0}, {1}
test_vector	javax.swing.text.MutableAttributeSet:getAttribute(. ..)@337: Addr_Set{null}, Inverse{null}
test_vector	javax.swing.text.MutableAttributeSet:getAttribute(. ..)@338: Addr_Set{null}, Inverse{null}
test_vector	org.apache.commons.logging.Log:isDebugEnabled(... )@345: {0}, {1}
test_vector	org.apache.commons.logging.Log:isDebugEnabled(... )@377: {0}, {1}

info method not available -- call on bool org.apache.commons.logging. Log:isDebugEnabled()

info method not available -- call on void org.apache.commons.logging. Log:debug(Object)

info method not available -- call on bool org.apache.commons.logging. Log:isDebugEnabled()

info method not available -- call on void org.apache.commons.logging. Log:debug(Object, Throwable)

info method not available -- call on bool org.apache.commons.logging. Log:isDebugEnabled()

info method not available -- call on void org.apache.commons.logging. Log:debug(Object)

method	void handleEndTag(HTML$Tag, int)
pre	this.mList != null
pre	(soft) init'ed(this.mEnd)
pre	(soft) init'ed(this.mFound)
post	this.mCurrentTag == One-of{old this.mCurrentTag, null}
post	this.mEnd == One-of{pos, old this.mEnd}
post	(soft) init'ed(this.mEnd)
post	this.mStart == One-of{old this.mStart, pos}
test_vector	this.mEnd: {-2³¹..-1, 1..2³²-1}, {0}
test_vector	this.mFound: {0}, {1}
test_vector	java.util.List:contains(...)@395: {0}, {1}
test_vector	java.util.List:contains(...)@399: {0}, {1}

method	void handleText(char[], int)
pre	init'ed(this.mCurrentTag)
pre	(soft) this.mTitle != null
presumption	init'ed(javax.swing.text.html.HTML$Tag.TITLE)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	this.mTitle == One-of{old this.mTitle, &java.lang.StringBuilder:toString(...)}
post	(soft) this.mTitle != null
test_vector	this.mCurrentTag: Addr_Set{null}, Inverse{null}
test_vector	java.lang.Object:equals(...)@414: {0}, {1}
test_vector	java.lang.String:length(...)@417: {50.. 2³²-1}, {0..49}

	info	method not available	-- call on LogFactory org.apache.commons.logging. LogFactory:getFactory()
	info	method not available	-- call on Log org.apache.commons.logging. LogFactory:getInstance(Class)

	info	method not available	-- call on SyndContent com.sun.syndication.feed. synd.SyndEntry:getDescription()
	info	method not available	-- call on String com.sun.syndication.feed.synd. SyndContent:getValue()