Messages

Last Msg First Msg

method

net.sourceforge.pebble.security.DefaultSecurityRea lm$1__static_init

method

void net.sourceforge.pebble.security. DefaultSecurityRealm$1(DefaultSecurityRealm)

method

void net.sourceforge.pebble.security. DefaultSecurityRealm()

method	net.sourceforge.pebble.security.DefaultSecurityRea lm__static_init
post	init'ed(log)

info method not available -- call on Log org.apache.commons.logging. LogFactory:getLog(Class)

method	void init()
pre	(soft) this.configuration != null
pre	(soft) this.passwordEncoder != null
pre	(soft) this.saltSource != null
presumption	org.apache.commons.logging.LogFactory:getLog(... )@22 != null
presumption	defaultUser.grantedAuthories.length <= 2³²-1
unanalyzed	call on getUser
presumption	defaultUser.grantedAuthories[...] != null
presumption	java.util.Set:toArray(...)@194 != null
presumption	net.sourceforge.pebble.Constants.BLOG_ADMIN_ROLE != null
presumption	net.sourceforge.pebble.Constants.BLOG_CONTRIBUTOR_ ROLE != null
presumption	net.sourceforge.pebble.Constants.BLOG_OWNER_ROLE != null
unanalyzed	call on getFileForUser
presumption	net.sourceforge.pebble.Constants.BLOG_PUBLISHER_ ROLE != null
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on net.sourceforge.pebble.Configuration:getDat aDirectory
unanalyzed	call on java.util.Properties
unanalyzed	call on java.util.Properties:load
unanalyzed	call on updateUser
unanalyzed	call on java.io.FileInputStream:close
unanalyzed	call on java.util.Properties:getProperty
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Properties:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.util.Map:put
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
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File
unanalyzed	call on net.sourceforge.pebble.PebbleException
test_vector	java.io.File:exists(...)@47: {1}, {0}
unanalyzed	call on org.acegisecurity.providers.dao. SaltSource:getSalt
unanalyzed	call on org.acegisecurity.providers.encoding. PasswordEncoder:encodePassword
unanalyzed	call on java.util.Properties:setProperty
unanalyzed	call on org.acegisecurity.GrantedAuthority:getAutho rity
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.util.Properties:store
unanalyzed	call on java.io.FileOutputStream:flush
unanalyzed	call on java.io.FileOutputStream:close

info method not available -- call on void org.apache.commons.logging. Log:warn(Object)

info method not available -- call on void org.apache.commons.logging. Log:error(Object, Throwable)

method	Collection getUsers()
pre	this.configuration != null
presumption	Local_7[Local_5]@68 != null
presumption	files.length@68 <= 2³²-1
presumption	java.io.File:getName(...)@83 != null
presumption	java.io.File:listFiles(...)@68 != null
post	return_value == &new LinkedList(getUsers#1)
post	new LinkedList(getUsers#1) num objects == 1
unanalyzed	call on getFileForUser
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.util.Properties
unanalyzed	call on java.util.Properties:load
unanalyzed	call on java.io.FileInputStream:close
unanalyzed	call on java.util.Properties:getProperty
unanalyzed	call on net.sourceforge.pebble.Configuration:getDat aDirectory
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Properties:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.util.Map:put
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
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File
unanalyzed	call on net.sourceforge.pebble.PebbleException

method	bool accept(File, String)
pre	name != null
post	init'ed(return_value)

info method not available -- call on void net.sourceforge.pebble.comparator. PebbleUserDetailsComparator()

method	PebbleUserDetails getUser(String)
pre	this.configuration != null
presumption	java.util.Iterator:next(...)@126 != null
presumption	java.util.Properties:getProperty(...)@114 != null
presumption	java.util.Properties:keySet(...)@126 != null
presumption	roles.length@114 <= 2³²-1
presumption	roles[...]@114 != null
post	return_value in Addr_Set{null,&new PebbleUserDetails(getUser#4)}
post	new HashMap(PebbleUserDetails#1) num objects <= 1
post	new HashMap(getUser#3) num objects <= 1
post	new PebbleUserDetails(getUser#4) num objects <= 1
post	init'ed(new PebbleUserDetails(getUser#4). detailsUpdateable)
post	init'ed(new PebbleUserDetails(getUser#4). emailAddress)
post	init'ed(new PebbleUserDetails(getUser#4). grantedAuthories)
post	init'ed(new PebbleUserDetails(getUser#4).name)
post	init'ed(new PebbleUserDetails(getUser#4).password)
post	new PebbleUserDetails(getUser#4).preferences == &new HashMap(getUser#3)
post	init'ed(new PebbleUserDetails(getUser#4).profile)
post	new PebbleUserDetails(getUser#4).username == username
post	init'ed(new PebbleUserDetails(getUser#4).username)
unanalyzed	call on net.sourceforge.pebble.Configuration:getDat aDirectory
post	init'ed(new PebbleUserDetails(getUser#4).website)
unanalyzed	call on java.util.HashMap
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
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File
unanalyzed	call on net.sourceforge.pebble.PebbleException
test_vector	java.io.File:exists(...)@103: {1}, {0}
test_vector	java.lang.String:startsWith(...)@128: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@126: {1}, {0}
test_vector	java.util.Properties:getProperty(...)@119: Addr_Set{null}, Inverse{null}

method	void createUser(PebbleUserDetails)
pre	pud != null
pre	init'ed(pud.username)
pre	this.configuration != null
presumption	java.io.File:exists(...)@103 == 0
unanalyzed	call on getFileForUser
pre	init'ed(pud.detailsUpdateable)
unanalyzed	call on java.io.File:exists
pre	init'ed(pud.emailAddress)
unanalyzed	call on java.io.FileInputStream
pre	pud.grantedAuthories != null
unanalyzed	call on java.util.Properties
unanalyzed	call on java.util.Properties:load
pre	pud.grantedAuthories.length <= 2³²-1
pre	init'ed(pud.name)
unanalyzed	call on java.io.FileInputStream:close
unanalyzed	call on java.util.Properties:getProperty
pre	init'ed(pud.preferences)
pre	init'ed(pud.profile)
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:equalsIgnoreCase
pre	init'ed(pud.website)
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Properties:keySet
unanalyzed	call on java.util.Set:iterator
pre	(soft) pud.grantedAuthories[...] != null
pre	(soft) init'ed(pud.password)
unanalyzed	call on java.lang.String:startsWith
pre	(soft) this.passwordEncoder != null
unanalyzed	call on java.lang.String:length
pre	(soft) this.saltSource != null
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.util.Map:put
unanalyzed	call on net.sourceforge.pebble.Configuration:getDat aDirectory
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
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File
unanalyzed	call on net.sourceforge.pebble.PebbleException
unanalyzed	call on org.acegisecurity.providers.dao. SaltSource:getSalt
unanalyzed	call on org.acegisecurity.providers.encoding. PasswordEncoder:encodePassword
unanalyzed	call on java.util.Properties:setProperty
unanalyzed	call on org.acegisecurity.GrantedAuthority:getAutho rity
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.util.Properties:store
unanalyzed	call on java.io.FileOutputStream:flush
unanalyzed	call on java.io.FileOutputStream:close

method	void updateUser(PebbleUserDetails)
pre	pud != null
pre	init'ed(pud.detailsUpdateable)
pre	init'ed(pud.emailAddress)
pre	pud.grantedAuthories != null
pre	pud.grantedAuthories.length <= 2³²-1
pre	init'ed(pud.name)
pre	init'ed(pud.preferences)
pre	init'ed(pud.profile)
pre	init'ed(pud.username)
pre	init'ed(pud.website)
pre	this.configuration != null
pre	(soft) pud.grantedAuthories[...] != null
pre	(soft) init'ed(pud.password)
pre	(soft) this.passwordEncoder != null
pre	(soft) this.saltSource != null
unanalyzed	call on net.sourceforge.pebble.Configuration:getDat aDirectory
unanalyzed	call on java.io.File
unanalyzed	call on getFileForUser
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.util.Properties
unanalyzed	call on java.util.Properties:load
unanalyzed	call on java.io.FileInputStream:close
unanalyzed	call on java.util.Properties:getProperty
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Properties:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.util.Map:put
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
unanalyzed	call on net.sourceforge.pebble.PebbleException
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on org.acegisecurity.providers.dao. SaltSource:getSalt
unanalyzed	call on org.acegisecurity.providers.encoding. PasswordEncoder:encodePassword
unanalyzed	call on java.util.Properties:setProperty
unanalyzed	call on org.acegisecurity.GrantedAuthority:getAutho rity
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.util.Properties:store
unanalyzed	call on java.io.FileOutputStream:flush
unanalyzed	call on java.io.FileOutputStream:close

method	void updateUser(PebbleUserDetails, bool)
pre	pud != null
pre	init'ed(pud.detailsUpdateable)
pre	init'ed(pud.emailAddress)
pre	pud.grantedAuthories != null
pre	pud.grantedAuthories.length <= 2³²-1
pre	init'ed(pud.name)
pre	init'ed(pud.preferences)
pre	init'ed(pud.profile)
pre	init'ed(pud.username)
pre	init'ed(pud.website)
pre	this.configuration != null
pre	(soft) pud.grantedAuthories[...] != null
pre	(soft) init'ed(pud.password)
pre	(soft) this.passwordEncoder != null
pre	(soft) this.saltSource != null
presumption	java.io.File:exists(...)@103 == 1
presumption	java.util.Iterator:hasNext(...)@126 == 0
presumption	java.util.Map:keySet(...)@184 != null
unanalyzed	call on net.sourceforge.pebble.Configuration:getDat aDirectory
unanalyzed	call on java.io.File
unanalyzed	call on getFileForUser
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.util.Properties
unanalyzed	call on java.util.Properties:load
unanalyzed	call on java.io.FileInputStream:close
unanalyzed	call on java.util.Properties:getProperty
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Properties:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.util.Map:put
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
unanalyzed	call on net.sourceforge.pebble.PebbleException
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on org.acegisecurity.GrantedAuthority:getAutho rity
test_vector	updatePassword: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@184: {1}, {0}

info method not available -- call on Object org.acegisecurity.providers.dao. SaltSource:getSalt(UserDetails)

info method not available -- call on String org.acegisecurity.providers. encoding.PasswordEncoder:encodePassword(String, Object)

method	void changePassword(String, String)
unanalyzed	call on getFileForUser
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.util.Properties
unanalyzed	call on java.util.Properties:load
unanalyzed	call on java.io.FileInputStream:close
unanalyzed	call on java.util.Properties:getProperty
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.Properties:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.util.Map:put
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
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File
unanalyzed	call on net.sourceforge.pebble.PebbleException
pre	(soft) this.configuration != null
pre	(soft) this.passwordEncoder != null
pre	(soft) this.saltSource != null
presumption	pud.grantedAuthories.length@206 <= 2³²-1
presumption	pud.grantedAuthories[...]@206 != null
unanalyzed	call on net.sourceforge.pebble.Configuration:getDat aDirectory
unanalyzed	call on org.acegisecurity.providers.dao. SaltSource:getSalt
unanalyzed	call on org.acegisecurity.providers.encoding. PasswordEncoder:encodePassword
unanalyzed	call on java.util.Properties:setProperty
unanalyzed	call on org.acegisecurity.GrantedAuthority:getAutho rity
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.util.Properties:store
unanalyzed	call on java.io.FileOutputStream:flush
unanalyzed	call on java.io.FileOutputStream:close

Prev Msg Next Msg

+

click for all messages in this file medium

precondition failure net/sourceforge/pebble/security/DefaultSecurityReal m.updateUser: pud.grantedAuthories != null

Prev Msg Next Msg

method	void removeUser(String)
pre	this.configuration != null
presumption	java.io.File:exists(...)@224 == 0
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File
unanalyzed	call on net.sourceforge.pebble.PebbleException
test_vector	java.io.File:exists(...)@220: {0}, {1}
unanalyzed	call on net.sourceforge.pebble.Configuration:getDat aDirectory

method	File getFileForRealm()
pre	this.configuration != null
post	return_value == &new File(getFileForRealm#1)
post	new File(getFileForRealm#1) num objects == 1

info method not available -- call on String net.sourceforge.pebble. Configuration:getDataDirectory()

method	File getFileForUser(String)
pre	this.configuration != null
post	return_value == &new File(getFileForUser#1)
post	new File(getFileForUser#1) num objects == 1
unanalyzed	call on java.io.File
unanalyzed	call on net.sourceforge.pebble.Configuration:getDat aDirectory

method	Configuration getConfiguration()
pre	init'ed(this.configuration)
post	return_value == this.configuration
post	init'ed(return_value)

method	void setConfiguration(Configuration)
post	this.configuration == configuration
post	init'ed(this.configuration)

method	PasswordEncoder getPasswordEncoder()
pre	init'ed(this.passwordEncoder)
post	return_value == this.passwordEncoder
post	init'ed(return_value)

method	void setPasswordEncoder(PasswordEncoder)
post	this.passwordEncoder == passwordEncoder
post	init'ed(this.passwordEncoder)

method	SaltSource getSaltSource()
pre	init'ed(this.saltSource)
post	return_value == this.saltSource
post	init'ed(return_value)

method	void setSaltSource(SaltSource)
post	this.saltSource == saltSource
post	init'ed(this.saltSource)

	info	method not available	-- call on Object org.acegisecurity.providers.dao. SaltSource:getSalt(UserDetails)
	info	method not available	-- call on String org.acegisecurity.providers. encoding.PasswordEncoder:encodePassword(String, Object)