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 <= 2³²-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 <= 2³²-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 <= 2³²-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 <= 2³²-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 <= 2³²-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

click for all messages in this file warning

test always goes same way test predetermined because i - authorities.length in -2³²+1..-1

Prev Msg Next Msg

method	bool isUserInRole(String)
pre	init'ed(this.grantedAuthories)
pre	(soft) this.grantedAuthories.length <= 2³²-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 <= 2³²-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 <= 2³²-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 <= 2³²-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 <= 2³²-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 <= 2³²-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)

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