Messages

Last Msg First Msg

method	org.apache.roller.weblogger.ui.rendering.pagers. WeblogsPager__static_init
post	init'ed(log)

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

method	void org.apache.roller.weblogger.ui.rendering. pagers.WeblogsPager(URLStrategy, String, String, int, int, int)
pre	(soft) length <= 2³²-2
pre	(soft) log != null
pre	(soft) sinceDays <= 2³¹
post	this.length == length
post	(soft) this.length <= 2³²-2
post	init'ed(this.letter)
post	this.locale == locale
post	init'ed(this.locale)
post	init'ed(this.more)
post	this.page == One-of{0, page}
post	this.page >= 0
post	this.sinceDays == sinceDays
post	(soft) this.sinceDays <= 2³¹
post	this.url == baseUrl
post	init'ed(this.url)
post	this.urlStrategy == strat
post	init'ed(this.urlStrategy)
post	this.weblogs == &new ArrayList(getItems#1)
post	new ArrayList(getItems#1) num objects == 1
post	(soft) length*this.page in -2³¹.. 2³²-1
unanalyzed	call on getPage
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Calendar:getInstance
unanalyzed	call on java.util.Date
unanalyzed	call on java.util.Calendar:setTime
unanalyzed	call on java.util.Calendar:add
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsites
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWeblogsByLetter
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.commons.logging.Log:error

method	void org.apache.roller.weblogger.ui.rendering. pagers.WeblogsPager(URLStrategy, String, String, String, int, int, int)
pre	(soft) length <= 2³²-2
pre	(soft) log != null
pre	(soft) sinceDays <= 2³¹
post	this.length == length
post	(soft) this.length <= 2³²-2
post	this.letter == letter
post	init'ed(this.letter)
post	this.locale == locale
post	init'ed(this.locale)
post	init'ed(this.more)
post	this.page == One-of{0, page}
post	this.page >= 0
post	this.sinceDays == sinceDays
post	(soft) this.sinceDays <= 2³¹
post	this.url == baseUrl
post	init'ed(this.url)
post	this.urlStrategy == strat
post	init'ed(this.urlStrategy)
post	this.weblogs == &new ArrayList(getItems#1)
post	new ArrayList(getItems#1) num objects == 1
post	(soft) length*this.page in -2³¹.. 2³²-1
unanalyzed	call on getPage
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Calendar:getInstance
unanalyzed	call on java.util.Date
unanalyzed	call on java.util.Calendar:setTime
unanalyzed	call on java.util.Calendar:add
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsites
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWeblogsByLetter
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.commons.logging.Log:error

method	String getNextLink()
pre	init'ed(this.letter)
pre	(soft) init'ed(this.more)
pre	(soft) this.page <= 2³²-2
pre	(soft) init'ed(this.url)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value in Addr_Set{null,&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...)}
unanalyzed	call on createURL
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Map:put
unanalyzed	call on org.apache.roller.weblogger.ui.rendering. util.WeblogFeedRequest:getWeblogCategoryName
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.net.URLEncoder:encode
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.ui.rendering. util.WeblogFeedRequest:getTerm
unanalyzed	call on org.apache.roller.weblogger.ui.rendering. util.WeblogFeedRequest:getTags
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.apache.roller.weblogger.ui.rendering. util.WeblogFeedRequest:isExcerpts
unanalyzed	call on hasMoreItems
test_vector	this.letter: Addr_Set{null}, Inverse{null}
test_vector	this.more: {0}, {1}

method	String getPrevLink()
pre	init'ed(this.letter)
pre	(soft) this.page >= -2³¹+1
pre	(soft) init'ed(this.url)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value in Addr_Set{null,&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...)}
unanalyzed	call on createURL
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Map:put
unanalyzed	call on org.apache.roller.weblogger.ui.rendering. util.WeblogFeedRequest:getWeblogCategoryName
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.net.URLEncoder:encode
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.ui.rendering. util.WeblogFeedRequest:getTerm
unanalyzed	call on org.apache.roller.weblogger.ui.rendering. util.WeblogFeedRequest:getTags
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.apache.roller.weblogger.ui.rendering. util.WeblogFeedRequest:isExcerpts
test_vector	this.letter: Addr_Set{null}, Inverse{null}
test_vector	this.page: {-2³¹+1..0}, {1..2³²-1}

method	List getItems()
pre	init'ed(this.weblogs)
pre	(soft) log != null
pre	(soft) this.length <= 2³²-2
pre	(soft) this.length*this.page in -2³¹.. 2³²-1
pre	(soft) init'ed(this.letter)
pre	(soft) init'ed(this.page)
pre	(soft) this.sinceDays <= 2³¹
presumption	init'ed(java.lang.Boolean.TRUE)
presumption	java.util.Calendar:getInstance(...)@140 != null
presumption	org.apache.roller.weblogger.business. UserManager:getWeblogsByLetter(...)@152 != null
presumption	org.apache.roller.weblogger.business. UserManager:getWebsites(...)@150 != null
presumption	org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@147 != null
presumption	org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@146 != null
post	return_value == One-of{old this.weblogs, &new ArrayList(getItems#1)}
post	return_value != null
post	this.weblogs == return_value
post	possibly_updated(this.more)
post	new ArrayList(getItems#1) num objects <= 1
test_vector	this.weblogs: Inverse{null}, Addr_Set{null}
test_vector	this.letter: Inverse{null}, Addr_Set{null}
test_vector	this.sinceDays: {-1}, {-2³¹..-2, 0..2³¹}

info method not available -- call on Weblogger org.apache.roller.weblogger. business.WebloggerFactory:getWeblogger()

info method not available -- call on UserManager org.apache.roller.weblogger. business.Weblogger:getUserManager()

info method not available -- call on List org.apache.roller.weblogger. business.UserManager:getWebsites(User, Boolean, Boolean, Date, Date, int, int)

info method not available -- call on List org.apache.roller.weblogger. business.UserManager:getWeblogsByLetter(char, int, int)

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 void org.apache.commons.logging. Log:error(Object, Throwable)

method	bool hasMoreItems()
pre	init'ed(this.more)
post	return_value == this.more
post	init'ed(return_value)