| method | void org.apache.roller.weblogger.ui.rendering. pagers.WeblogEntriesListPager(URLStrategy, String, Weblog, User, String, List, String, int, int, int) |
| pre | (soft) length <= 232-2 |
| pre | (soft) log != null |
| pre | (soft) sinceDays <= 231 |
| post | this.entries == &new ArrayList(getItems#1) |
| post | init'ed(this.lastUpdated) |
| post | this.length == length |
| post | (soft) this.length <= 232-2 |
| post | this.locale == locale |
| post | init'ed(this.locale) |
| post | init'ed(this.more) |
| post | this.page == One-of{0, pageNum} |
| post | this.page >= 0 |
| post | this.queryCat == queryCat |
| post | init'ed(this.queryCat) |
| post | this.queryTags == queryTags |
| post | init'ed(this.queryTags) |
| post | this.queryUser == queryUser |
| post | init'ed(this.queryUser) |
| post | this.queryWeblog == queryWeblog |
| post | init'ed(this.queryWeblog) |
| post | this.sinceDays == sinceDays |
| post | (soft) this.sinceDays <= 231 |
| post | this.url == baseUrl |
| post | init'ed(this.url) |
| post | this.urlStrategy == strat |
| post | init'ed(this.urlStrategy) |
| post | new ArrayList(getItems#1) num objects == 1 |
| post | (soft) length*this.page in -231.. 232-1 |
| unanalyzed | call on java.util.List:size |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on java.util.Date |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on java.util.Calendar:getInstance |
| 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:getWeblogManager |
| unanalyzed | call on org.apache.roller.weblogger.business. Weblogger:getUserManager |
| unanalyzed | call on org.apache.roller.weblogger.business. WeblogManager:getWeblogEntries |
| 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 | List getItems() |
| pre | init'ed(this.entries) |
| 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.locale) |
| pre | (soft) init'ed(this.page) |
| pre | (soft) init'ed(this.queryCat) |
| pre | (soft) init'ed(this.queryTags) |
| pre | (soft) init'ed(this.queryUser) |
| pre | (soft) init'ed(this.queryWeblog) |
| pre | (soft) this.sinceDays <= 231 |
| presumption | java.util.Calendar:getInstance(...)@104 != null |
| presumption | org.apache.roller.weblogger.business. WeblogManager:getWeblogEntries(...)@114 != null |
| presumption | org.apache.roller.weblogger.business. Weblogger:getWeblogManager(...)@112 != null |
| presumption | org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@111 != null |
| post | return_value == One-of{old this.entries, &new ArrayList(getItems#1)} |
| post | return_value != null |
| post | this.entries == return_value |
| post | possibly_updated(this.more) |
| post | new ArrayList(getItems#1) num objects <= 1 |
| test_vector | this.entries: Inverse{null}, Addr_Set{null} |
| test_vector | this.sinceDays: {-231..0}, {1..231} |
| test_vector | java.util.Iterator:hasNext(...)@131: {0}, {1} |
| method | Date getLastUpdated() |
| pre | init'ed(this.lastUpdated) |
| pre | (soft) log != null |
| pre | (soft) init'ed(this.entries) |
| pre | (soft) this.length <= 232-2 |
| pre | (soft) this.length*this.page in -231.. 232-1 |
| pre | (soft) init'ed(this.locale) |
| pre | (soft) init'ed(this.page) |
| pre | (soft) init'ed(this.queryCat) |
| pre | (soft) init'ed(this.queryTags) |
| pre | (soft) init'ed(this.queryUser) |
| pre | (soft) init'ed(this.queryWeblog) |
| pre | (soft) this.sinceDays <= 231 |
| presumption | e.pojo@161 != null |
| presumption | java.util.Iterator:next(...)@161 != null |
| presumption | java.util.List:get(...).pojo@160 != null |
| presumption | java.util.List:get(...)@160 != null |
| presumption | org.apache.roller.weblogger.pojos.WeblogEntry:getUp dateTime(...)@164 != null |
| post | return_value == One-of{old this.lastUpdated, &new Date(getLastUpdated#1), &new Date(getLastUpdated#2)} |
| post | return_value != null |
| post | this.lastUpdated == return_value |
| post | this.entries == One-of{old this.entries, &new ArrayList(getItems#1)} |
| post | (soft) init'ed(this.entries) |
| post | possibly_updated(this.more) |
| post | new ArrayList(getItems#1) num objects <= 1 |
| post | new Date(getLastUpdated#1) num objects <= 1 |
| post | new Date(getLastUpdated#2) num objects <= 1 |
| unanalyzed | call on java.util.List:size |
| unanalyzed | call on org.apache.roller.weblogger.pojos. WeblogEntry:getUpdateTime |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on org.apache.roller.weblogger.pojos. WeblogEntry:getPubTime |
| unanalyzed | call on java.util.Date |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on java.util.Calendar:getInstance |
| 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:getWeblogManager |
| unanalyzed | call on org.apache.roller.weblogger.business. Weblogger:getUserManager |
| unanalyzed | call on org.apache.roller.weblogger.business. WeblogManager:getWeblogEntries |
| 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 |
| test_vector | this.lastUpdated: Inverse{null}, Addr_Set{null} |
| test_vector | java.sql.Timestamp:after(...)@162: {0}, {1} |
| test_vector | java.util.Iterator:hasNext(...)@161: {0}, {1} |
| test_vector | java.util.List:size(...)@159: {-231..0}, {1..232-1} |