Messages

Last Msg First Msg

method | net.sourceforge.pebble.security.PebbleUserDetails_ _static_init

method | void net.sourceforge.pebble.security. PebbleUserDetails()
post | this.detailsUpdateable == 1
post | new HashMap(PebbleUserDetails#1) num objects == 1
post | this.preferences == &new HashMap(PebbleUserDeta ils#1)

method | void net.sourceforge.pebble.security. PebbleUserDetails(String, String, String, String, String, String[], Map, bool)
pre | (soft) roles.length <= 232-1
pre | (soft) roles[...] != null
post | this.detailsUpdateable == detailsUpdateable
post | init'ed(this.detailsUpdateable)
post | this.emailAddress == emailAddress
post | init'ed(this.emailAddress)
post | init'ed(this.grantedAuthories)
post | this.name == name
post | init'ed(this.name)
post | this.preferences == preferences
post | init'ed(this.preferences)
post | this.profile == profile
post | init'ed(this.profile)
post | this.username == username
post | init'ed(this.username)
post | this.website == website
post | init'ed(this.website)
post | new HashMap(PebbleUserDetails#1) num objects == 1
unanalyzed | call on java.util.HashSet
unanalyzed | call on java.lang.String:trim
unanalyzed | call on org.acegisecurity.GrantedAuthorityImpl
unanalyzed | call on java.util.Set:add
unanalyzed | call on java.util.Set:toArray

method | void net.sourceforge.pebble.security. PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)
pre | (soft) roles.length <= 232-1
pre | (soft) roles[...] != null
post | this.detailsUpdateable == detailsUpdateable
post | init'ed(this.detailsUpdateable)
post | this.emailAddress == emailAddress
post | init'ed(this.emailAddress)
post | init'ed(this.grantedAuthories)
post | this.name == name
post | init'ed(this.name)
post | this.password == password
post | init'ed(this.password)
post | this.preferences == preferences
post | init'ed(this.preferences)
post | this.profile == profile
post | init'ed(this.profile)
post | this.username == username
post | init'ed(this.username)
post | this.website == website
post | init'ed(this.website)
post | new HashMap(PebbleUserDetails#1) num objects == 1
unanalyzed | call on java.util.HashSet
unanalyzed | call on java.lang.String:trim
unanalyzed | call on org.acegisecurity.GrantedAuthorityImpl
unanalyzed | call on java.util.Set:add
unanalyzed | call on java.util.Set:toArray

method | String getUsername()
pre | init'ed(this.username)
post | return_value == this.username
post | init'ed(return_value)

method | String getPassword()
pre | init'ed(this.password)
post | return_value == this.password
post | init'ed(return_value)

method | bool isAccountNonExpired()
post | return_value == 1

method | bool isAccountNonLocked()
post | return_value == 1

method | bool isCredentialsNonExpired()
post | return_value == 1

method | bool isEnabled()
post | return_value == 1

method | String getName()
pre | init'ed(this.name)
post | return_value == this.name
post | init'ed(return_value)

method | String getEmailAddress()
pre | init'ed(this.emailAddress)
post | return_value == this.emailAddress
post | init'ed(return_value)

method | String getWebsite()
pre | init'ed(this.website)
post | return_value == this.website
post | init'ed(return_value)

method | String getProfile()
pre | init'ed(this.profile)
post | return_value == this.profile
post | init'ed(return_value)

method | GrantedAuthority[] getAuthorities()
pre | init'ed(this.grantedAuthories)
post | return_value == this.grantedAuthories
post | init'ed(return_value)

method | String[] getRoles()
pre | this.grantedAuthories != null
pre | this.grantedAuthories.length <= 232-1
pre | (soft) this.grantedAuthories[...] != null
post | return_value == &new String[](getRoles#1)
post | new String[](getRoles#1) num objects == 1
post | return_value.length == this.grantedAuthories. length
post | return_value.length <= 232-1
post | possibly_updated(return_value[...])

| info | method not available | -- call on String org.acegisecurity. GrantedAuthority:getAuthority()

method | String getRolesAsString()
pre | this.grantedAuthories != null
pre | this.grantedAuthories.length <= 232-1
pre | (soft) this.grantedAuthories[...] != null
post | return_value != null

| info | method not available | -- call on String org.acegisecurity. GrantedAuthority:getAuthority()

Prev Msg Next Msg

| warning
| test always goes same way | test predetermined because i - authorities.length in -232+1..-1

Prev Msg Next Msg

method | bool isUserInRole(String)
pre | init'ed(this.grantedAuthories)
pre | (soft) this.grantedAuthories.length <= 232-1
pre | (soft) this.grantedAuthories[...] != null
presumption | org.acegisecurity.GrantedAuthority:getAuthority(... )@161 != null
post | init'ed(return_value)
test_vector | this.grantedAuthories: Addr_Set{null}, Inverse{null}
test_vector | java.lang.String:equals(...)@161: {0}, {1}

| info | method not available | -- call on String org.acegisecurity. GrantedAuthority:getAuthority()

method | bool isBlogAdmin()
presumption | init'ed(net.sourceforge.pebble.Constants.BLOG_ ADMIN_ROLE)
pre | init'ed(this.grantedAuthories)
pre | (soft) this.grantedAuthories.length <= 232-1
pre | (soft) this.grantedAuthories[...] != null
post | init'ed(return_value)
unanalyzed | call on org.acegisecurity.GrantedAuthority:getAutho rity
unanalyzed | call on java.lang.String:equals

method | bool isBlogOwner()
presumption | init'ed(net.sourceforge.pebble.Constants.BLOG_ OWNER_ROLE)
pre | init'ed(this.grantedAuthories)
pre | (soft) this.grantedAuthories.length <= 232-1
pre | (soft) this.grantedAuthories[...] != null
post | init'ed(return_value)
unanalyzed | call on org.acegisecurity.GrantedAuthority:getAutho rity
unanalyzed | call on java.lang.String:equals

method | bool isBlogPublisher()
presumption | init'ed(net.sourceforge.pebble.Constants.BLOG_ PUBLISHER_ROLE)
pre | init'ed(this.grantedAuthories)
pre | (soft) this.grantedAuthories.length <= 232-1
pre | (soft) this.grantedAuthories[...] != null
post | init'ed(return_value)
unanalyzed | call on org.acegisecurity.GrantedAuthority:getAutho rity
unanalyzed | call on java.lang.String:equals

method | bool isBlogContributor()
presumption | init'ed(net.sourceforge.pebble.Constants.BLOG_ CONTRIBUTOR_ROLE)
pre | init'ed(this.grantedAuthories)
pre | (soft) this.grantedAuthories.length <= 232-1
pre | (soft) this.grantedAuthories[...] != null
post | init'ed(return_value)
unanalyzed | call on org.acegisecurity.GrantedAuthority:getAutho rity
unanalyzed | call on java.lang.String:equals

method | GrantedAuthority[] createGrantedAuthorities(String [])
presumption | init'ed(net.sourceforge.pebble.Constants.BLOG_ READER_ROLE)
pre | (soft) roles.length <= 232-1
pre | (soft) roles[...] != null
post | init'ed(return_value)
test_vector | roles: Addr_Set{null}, Inverse{null}

| info | method not available | -- call on void org.acegisecurity.GrantedAuthorityI mpl(String)

| info | method not available | -- call on void org.acegisecurity.GrantedAuthorityI mpl(String)

method | void setUsername(String)
post | this.username == username
post | init'ed(this.username)

method | void setPassword(String)
post | this.password == password
post | init'ed(this.password)

method | void setName(String)
post | this.name == name
post | init'ed(this.name)

method | void setEmailAddress(String)
post | this.emailAddress == emailAddress
post | init'ed(this.emailAddress)

method | void setWebsite(String)
post | this.website == website
post | init'ed(this.website)

method | void setProfile(String)
post | this.profile == profile
post | init'ed(this.profile)

method | void setGrantedAuthories(GrantedAuthority[])
post | this.grantedAuthories == grantedAuthories
post | init'ed(this.grantedAuthories)

method | bool isDetailsUpdateable()
pre | init'ed(this.detailsUpdateable)
post | return_value == this.detailsUpdateable
post | init'ed(return_value)

method | void setDetailsUpdateable(bool)
post | this.detailsUpdateable == detailsUpdateable
post | init'ed(this.detailsUpdateable)

method | Map getPreferences()
pre | init'ed(this.preferences)
post | return_value == &new HashMap(getPreferences#1)
post | new HashMap(getPreferences#1) num objects == 1

method | String getPreference(String)
pre | this.preferences != null
post | init'ed(return_value)

method | void setPreferences(Map)
post | this.preferences == &new HashMap(setPreferences #1)
post | new HashMap(setPreferences#1) num objects == 1