| method | void org.apache.roller.weblogger.ui.rendering. pagers.UsersPager(URLStrategy, String, String, int, int, int) |
| pre | (soft) length <= 232-2 |
| pre | (soft) log != null |
| post | this.length == length |
| post | (soft) this.length <= 232-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 | init'ed(this.sinceDays) |
| post | this.url == baseUrl |
| post | init'ed(this.url) |
| post | this.urlStrategy == strat |
| post | init'ed(this.urlStrategy) |
| post | this.users == &new ArrayList(getItems#1) |
| post | new ArrayList(getItems#1) num objects == 1 |
| post | (soft) length*this.page in -231.. 232-1 |
| unanalyzed | call on getPage |
| unanalyzed | call on java.util.ArrayList |
| 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:getUsers |
| unanalyzed | call on java.lang.String:charAt |
| unanalyzed | call on org.apache.roller.weblogger.business. UserManager:getUsersByLetter |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on org.apache.roller.weblogger.pojos.wrapper. UserWrapper:wrap |
| 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.UsersPager(URLStrategy, String, String, String, int, int, int) |
| pre | (soft) length <= 232-2 |
| pre | (soft) log != null |
| post | this.length == length |
| post | (soft) this.length <= 232-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 | init'ed(this.sinceDays) |
| post | this.url == baseUrl |
| post | init'ed(this.url) |
| post | this.urlStrategy == strat |
| post | init'ed(this.urlStrategy) |
| post | this.users == &new ArrayList(getItems#1) |
| post | new ArrayList(getItems#1) num objects == 1 |
| post | (soft) length*this.page in -231.. 232-1 |
| unanalyzed | call on getPage |
| unanalyzed | call on java.util.ArrayList |
| 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:getUsers |
| unanalyzed | call on java.lang.String:charAt |
| unanalyzed | call on org.apache.roller.weblogger.business. UserManager:getUsersByLetter |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on org.apache.roller.weblogger.pojos.wrapper. UserWrapper:wrap |
| 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 <= 232-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 >= -231+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: {-231+1..0}, {1..232-1} |
| method | List getItems() |
| pre | init'ed(this.users) |
| pre | (soft) log != null |
| pre | (soft) this.length <= 232-2 |
| pre | (soft) this.length*this.page in -231.. 232-1 |
| pre | (soft) init'ed(this.letter) |
| pre | (soft) init'ed(this.page) |
| presumption | init'ed(java.lang.Boolean.TRUE) |
| presumption | org.apache.roller.weblogger.business. UserManager:getUsers(...)@141 != null |
| presumption | org.apache.roller.weblogger.business. UserManager:getUsersByLetter(...)@143 != null |
| presumption | org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@138 != null |
| presumption | org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@137 != null |
| post | return_value == One-of{old this.users, &new ArrayList(getItems#1)} |
| post | return_value != null |
| post | this.users == return_value |
| post | possibly_updated(this.more) |
| post | new ArrayList(getItems#1) num objects <= 1 |
| test_vector | this.users: Inverse{null}, Addr_Set{null} |
| test_vector | this.letter: Inverse{null}, Addr_Set{null} |