| method | String execute() |
| pre | (soft) log != null |
| pre | (soft) init'ed(this.removeId) |
| presumption | java.util.Iterator:next(...)@94 != null |
| presumption | org.apache.roller.weblogger.business. WeblogManager:getWeblogCategories(...)@93 != null |
| presumption | org.apache.roller.weblogger.business. Weblogger:getWeblogManager(...)@92 != null |
| presumption | org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@92 != null |
| presumption | org.apache.roller.weblogger.pojos.WeblogCategory:ge tId(...)@95 != null |
| post | return_value == &"input" |
| post | this.allCategories == One-of{old this. allCategories, &new TreeSet(execute#1)} |
| post | new TreeSet(execute#1) num objects == 1 |
| test_vector | java.lang.String:equals(...)@95: {1}, {0} |
| test_vector | java.util.TreeSet:size(...)@105: {-231.. 0}, {1..232-1} |
| method | String remove() |
| pre | init'ed(this.category) |
| pre | (soft) log != null |
| pre | (soft) init'ed(this.removeId) |
| pre | (soft) init'ed(this.targetCategoryId) |
| presumption | org.apache.roller.weblogger.business. Weblogger:getWeblogManager(...)@119 != null |
| presumption | org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@119 != null |
| presumption | org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@124 != null |
| presumption | org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@132 != null |
| post | return_value in Addr_Set{&"success", &"input"} |
| post | this.allCategories == One-of{old this. allCategories, &new TreeSet(execute#1)} |
| post | init'ed(this.removeId) |
| post | new TreeSet(execute#1) num objects <= 1 |
| unanalyzed | call on org.apache.roller.weblogger.pojos. WeblogCategoryPathComparator |
| unanalyzed | call on java.util.TreeSet |
| 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.ui.struts2. editor.CategoryRemove:getActionWeblog |
| unanalyzed | call on org.apache.roller.weblogger.business. WeblogManager:getWeblogCategories |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on org.apache.roller.weblogger.pojos. WeblogCategory:getId |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on java.util.TreeSet:add |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on org.apache.commons.logging.Log:error |
| unanalyzed | call on org.apache.roller.weblogger.ui.struts2. editor.CategoryRemove:addError |
| unanalyzed | call on java.util.TreeSet:size |
| test_vector | this.category: Addr_Set{null}, Inverse{null} |
| test_vector | this.targetCategoryId: Addr_Set{null}, Inverse{null} |