| method | GrantedAuthority[] getGrantedAuthorities(LdapUserD etails) |
| pre | init'ed(this.defaultRole) |
| pre | userDetails != null |
| presumption | init'ed(java.lang.Boolean.TRUE) |
| presumption | java.util.Iterator:next(...)@70 != null |
| presumption | java.util.Set:size(...)@65 in 1..232-2 |
| presumption | org.apache.roller.weblogger.business. UserManager:getUserByUserName(...)@56 != null |
| presumption | org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@55 != null |
| presumption | org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@54 != null |
| presumption | org.apache.roller.weblogger.pojos.User:getRoles(... )@65 != null |
| presumption | org.apache.roller.weblogger.pojos.User:getRoles(... )@69 != null |
| post | return_value == &new GrantedAuthorityImpl[](get GrantedAuthorities#4) |
| post | init'ed(new GrantedAuthorityImpl(getGrantedAuthorit ies#5) num objects) |
| post | new GrantedAuthorityImpl[](getGrantedAuthorities#4) num objects == 1 |
| post | (soft) new GrantedAuthorityImpl[](getGrantedAuthori ties#4).length in 1..232-1 |
| post | new GrantedAuthorityImpl[](getGrantedAuthorities#4) [...] != null |
| test_vector | this.defaultRole: Addr_Set{null}, Inverse{null} |
| test_vector | java.util.Iterator:hasNext(...)@69: {0}, {1} |