Messages

Last Msg First Msg

method

org.apache.roller.weblogger.webservices. adminprotocol.RollerMemberHandler$MemberURI__static _init

method

org.apache.roller.weblogger.webservices. adminprotocol.RollerMemberHandler__static_init

method	void org.apache.roller.weblogger.webservices. adminprotocol.RollerMemberHandler$MemberURI(HttpSer vletRequest)
pre	req != null
pre	(soft) org/apache/roller/weblogger/webservices/admi nprotocol/Handler$URI.PATHINFO_PATTERN != null
post	init'ed(this.entryId)
post	this.handle == null
post	init'ed(this.type)
post	init'ed(this.username)
unanalyzed	call on javax.servlet.http.HttpServletRequest:getPa thInfo
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.util.regex.Pattern:matcher
unanalyzed	call on java.util.regex.Matcher:matches
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.util.regex.Matcher:group

Prev Msg Next Msg

+

click for all messages in this file low

use of default init check might fail: requires init'ed(entryIds. length)

Prev Msg Next Msg

Prev Msg Next Msg

+

click for all messages in this file low

use of default init check might fail: requires init'ed(entryIds. length)

+

warning

test always goes same way test predetermined because entryIds.length == 0

Prev Msg Next Msg

Prev Msg Next Msg

+

click for all messages in this file warning

dead code dead code here because entryIds.length == 0

Prev Msg Next Msg

method	bool hasUsername()
pre	init'ed(this.username)
post	init'ed(return_value)

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

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

method	String getHandle()
pre	init'ed(this.handle)
post	return_value == this.handle
post	init'ed(return_value)

method	void setHandle(String)
post	this.handle == handle
post	init'ed(this.handle)

method	void org.apache.roller.weblogger.webservices. adminprotocol.RollerMemberHandler(HttpServletReques t)
pre	request != null
pre	(soft) org/apache/roller/weblogger/webservices/admi nprotocol/Handler$URI.PATHINFO_PATTERN != null
post	init'ed(java.lang.String:substring(...)._tainted)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	this.memberUri == &new RollerMemberHandler$Memb erURI(RollerMemberHandler#1)
post	this.request == request
post	this.request != null
post	init'ed(this.roller)
post	this.uri == &new Handler$URI(Handler#1)
post	this.urlPrefix == &java.lang.StringBuilder:toSt ring(...)
post	this.userName == One-of{null, &java.lang. String:substring(...)}
post	this.userName in Addr_Set{null,&java.lang. String:substring(...)}
post	new Handler$URI(Handler#1) num objects == 1
post	new RollerMemberHandler$MemberURI(RollerMemberHandl er#1) num objects == 1
post	init'ed(new Handler$URI(Handler#1).entryId)
post	init'ed(new Handler$URI(Handler#1).type)
post	init'ed(this.memberUri.entryId)
post	this.memberUri.handle == null
post	init'ed(this.memberUri.type)
post	init'ed(this.memberUri.username)
unanalyzed	call on javax.servlet.http.HttpServletRequest:getPa thInfo
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.util.regex.Pattern:matcher
unanalyzed	call on java.util.regex.Matcher:matches
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.util.regex.Matcher:group
unanalyzed	call on java.lang.String:split
unanalyzed	call on org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger
unanalyzed	call on org.apache.roller.weblogger.config. WebloggerRuntimeConfig:getAbsoluteContextURL
unanalyzed	call on javax.servlet.http.HttpServletRequest:getHe ader
unanalyzed	call on java.util.StringTokenizer
unanalyzed	call on java.util.StringTokenizer:hasMoreTokens
unanalyzed	call on java.util.StringTokenizer:nextToken
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on java.lang.String:getBytes
unanalyzed	call on org.apache.commons.codec.binary. Base64:decodeBase64
unanalyzed	call on java.lang.String
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on getUserData
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getPassword
unanalyzed	call on org.apache.roller.weblogger.config. WebloggerConfig:getProperty
unanalyzed	call on java.lang.Boolean:valueOf
unanalyzed	call on java.lang.Boolean:booleanValue
unanalyzed	call on org.apache.roller.weblogger.util. Utilities:encodePassword
unanalyzed	call on java.lang.String:trim
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on java.lang.String:equals
unanalyzed	call on org.apache.roller.weblogger.pojos. User:hasRole
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getEnabled
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on authenticate

method	EntrySet getEntrySet(Document)
pre	d != null
pre	init'ed(this.urlPrefix)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(getEntrySet #1)
post	new MemberEntrySet(getEntrySet#1) num objects == 1
post	init'ed(return_value.entries)
post	return_value.href == &java.lang. StringBuilder:toString(...)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on setEntries
unanalyzed	call on org.jdom.Document:getRootElement
unanalyzed	call on org.jdom.Element:getName
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.Exception
unanalyzed	call on org.jdom.Element:getChildren
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.jdom.Element:getChild
unanalyzed	call on org.jdom.Element:getText
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:toArray

method	Handler$URI getUri()
pre	init'ed(this.memberUri)
post	return_value == this.memberUri
post	init'ed(return_value)

method	EntrySet processGet()
pre	this.memberUri != null
pre	init'ed(this.memberUri.entryId)
pre	this.roller != null
pre	init'ed(this.urlPrefix)
pre	(soft) init'ed(this.memberUri.handle)
pre	(soft) this.memberUri.type != null
pre	(soft) init'ed(this.memberUri.username)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	possibly_updated(new MemberEntrySet(toMemberEntrySe t#2).entries)
post	possibly_updated(new MemberEntrySet(toMemberEntrySe t#2).href)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on getUserData
unanalyzed	call on getWebsiteData
unanalyzed	call on getRoller
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:toArray
unanalyzed	call on toMemberEntrySet
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getAllPermissions
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getPermissions
unanalyzed	call on java.util.Collections:singletonList
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUsers
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle
test_vector	!(this.memberUri.entryId == null) \| (this.memberUri.type == null & this.memberUri.entryId == null): {1}, {0}
test_vector	!(this.memberUri.type == null) & this.memberUri.entryId == null: {0}, {1}
test_vector	this.memberUri.entryId: Inverse{null}, Addr_Set{null}

method	EntrySet processPost(Reader)
pre	this.memberUri != null
pre	this.memberUri.entryId == null
pre	(soft) this.memberUri.type != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	init'ed(return_value)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == undefined
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 0, if init'ed
post	new MemberEntrySet(toMemberEntrySet#2).entries == undefined
post	new MemberEntrySet(toMemberEntrySet#2).entries == null
post	new MemberEntrySet(toMemberEntrySet#2).href == new MemberEntrySet(toMemberEntrySet#2).entries

info call too complex - analysis skipped -- call on EntrySet postCollection(Reader)

method	EntrySet processPut(Reader)
pre	this.memberUri != null
pre	init'ed(this.memberUri.entryId)
pre	(soft) this.memberUri.type != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	init'ed(return_value)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == undefined
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 0, if init'ed
post	new MemberEntrySet(toMemberEntrySet#2).entries == undefined
post	new MemberEntrySet(toMemberEntrySet#2).entries == null
post	new MemberEntrySet(toMemberEntrySet#2).href == new MemberEntrySet(toMemberEntrySet#2).entries
test_vector	!(this.memberUri.entryId == null) \| (this.memberUri.type == null & this.memberUri.entryId == null): {1}, {0}
test_vector	!(this.memberUri.type == null) & this.memberUri.entryId == null: {0}, {1}
test_vector	this.memberUri.entryId: Inverse{null}, Addr_Set{null}

info call too complex - analysis skipped -- call on EntrySet putCollection(Reader)

info call too complex - analysis skipped -- call on EntrySet putEntry(Reader)

method	EntrySet processDelete()
pre	this.memberUri != null
pre	this.memberUri.entryId != null
pre	init'ed(this.memberUri.handle)
pre	this.memberUri.username != null
pre	this.roller != null
pre	init'ed(this.urlPrefix)
pre	(soft) this.memberUri.type != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	init'ed(new MemberEntrySet(toMemberEntrySet#2). entries)
post	new MemberEntrySet(toMemberEntrySet#2).href == &java.lang.StringBuilder:toString(...)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on getUserData
unanalyzed	call on getWebsiteData
unanalyzed	call on getRoller
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:flush
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.util.cache. CacheManager:invalidate
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:toArray
unanalyzed	call on toMemberEntrySet
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getPermissions
unanalyzed	call on getPermissionsData
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:removePermissions
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle

method	EntrySet getCollection()
pre	this.roller != null
pre	init'ed(this.urlPrefix)
presumption	java.util.List:toArray(...).length@152 <= 2³²-1
presumption	java.util.List:toArray(...)@152 != null
presumption	org.apache.roller.weblogger.business. UserManager:getAllPermissions(...)@146 != null
presumption	org.apache.roller.weblogger.business. UserManager:getUsers(...)@142 != null
presumption	org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@142 != null
presumption	org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@146 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	init'ed(new MemberEntrySet(toMemberEntrySet#2). entries)
post	new MemberEntrySet(toMemberEntrySet#2).href == &java.lang.StringBuilder:toString(...)
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:toArray
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
test_vector	java.util.Iterator:hasNext(...)@144: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@147: {0}, {1}

info method not available -- call on UserManager org.apache.roller.weblogger. business.Weblogger:getUserManager()

info method not available -- call on List org.apache.roller.weblogger. business.UserManager:getUsers(Weblog, Boolean, Date, Date, int, int)

method	EntrySet getEntry()
pre	this.memberUri != null
pre	init'ed(this.memberUri.handle)
pre	init'ed(this.memberUri.username)
pre	this.roller != null
pre	init'ed(this.urlPrefix)
presumption	java.util.Collections:singletonList(...)@187 != null
presumption	java.util.List:toArray(...).length@190 <= 2³²-1
presumption	java.util.List:toArray(...)@190 != null
presumption	org.apache.roller.weblogger.business. UserManager:getAllPermissions(...)@172 != null
presumption	org.apache.roller.weblogger.business. UserManager:getPermissions(...)@183 != null
presumption	org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@172 != null
presumption	org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@183 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	init'ed(new MemberEntrySet(toMemberEntrySet#2). entries)
post	new MemberEntrySet(toMemberEntrySet#2).href == &java.lang.StringBuilder:toString(...)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:toArray
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle
test_vector	this.memberUri.username: Inverse{null}, Addr_Set{null}

info method not available -- call on UserManager org.apache.roller.weblogger. business.Weblogger:getUserManager()

info method not available -- call on WeblogPermission org.apache.roller. weblogger.business.UserManager:getPermissions(Weblo g, User)

method	EntrySet postCollection(Reader)
pre	this.roller != null
pre	init'ed(this.urlPrefix)
presumption	c.entries@198 != null
presumption	c.entries@199 != null
presumption	java.util.List:size(...)@82 != 0
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(getEntrySet#1*) num objects == 1
post	init'ed(new MemberEntrySet(getEntrySet#1*). entries)
post	init'ed(new MemberEntrySet(getEntrySet#1*).href)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	init'ed(new MemberEntrySet(toMemberEntrySet#2). entries)
post	new MemberEntrySet(toMemberEntrySet#2).href == &java.lang.StringBuilder:toString(...)
post	new UserEntrySet(getEntrySet#1*) num objects == 0
post	init'ed(new UserEntrySet(getEntrySet#1*).entries)
post	init'ed(new UserEntrySet(getEntrySet#1*).href)
post	new WeblogEntrySet(getEntrySet#1*) num objects == 0
post	init'ed(new WeblogEntrySet(getEntrySet#1*). entries)
post	init'ed(new WeblogEntrySet(getEntrySet#1*).href)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on getUserData
unanalyzed	call on getWebsiteData
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setUser
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setWebsite
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setPermissionMask
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setPending
unanalyzed	call on getRoller
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:toArray
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:savePermissions
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:flush
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.util.cache. CacheManager:invalidate
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on java.util.List:add
unanalyzed	call on toMemberEntrySet
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:size
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on setEntries
unanalyzed	call on org.jdom.Document:getRootElement
unanalyzed	call on org.jdom.Element:getName
unanalyzed	call on java.lang.String:equals
unanalyzed	call on org.jdom.Element:getChildren
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.jdom.Element:getChild
unanalyzed	call on org.jdom.Element:getText
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle
unanalyzed	call on org.jdom.input.SAXBuilder
unanalyzed	call on org.jdom.input.SAXBuilder:build
unanalyzed	call on getEntrySet
unanalyzed	call on setHref
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.Entry
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.Locale
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.util.TimeZone:getTimeZone
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.Long:longValue
unanalyzed	call on java.util.Date
unanalyzed	call on java.lang.Boolean:valueOf

Prev Msg Next Msg

+

click for all messages in this file medium

null dereference check might fail: requires c != null

+

low

conditional throw check might fail: requires isEmpty(...) == 0

Prev Msg Next Msg

method	EntrySet putCollection(Reader)
pre	init'ed(this.urlPrefix)
pre	(soft) this.roller != null
presumption	c.entries@208 != null
presumption	c.entries@209 != null
presumption	java.util.List:size(...)@82 != 0
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(getEntrySet#1*) num objects == 1
post	init'ed(new MemberEntrySet(getEntrySet#1*). entries)
post	init'ed(new MemberEntrySet(getEntrySet#1*).href)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	init'ed(new MemberEntrySet(toMemberEntrySet#2). entries)
post	new MemberEntrySet(toMemberEntrySet#2).href == &java.lang.StringBuilder:toString(...)
post	new UserEntrySet(getEntrySet#1*) num objects == 0
post	init'ed(new UserEntrySet(getEntrySet#1*).entries)
post	init'ed(new UserEntrySet(getEntrySet#1*).href)
post	new WeblogEntrySet(getEntrySet#1*) num objects == 0
post	init'ed(new WeblogEntrySet(getEntrySet#1*). entries)
post	init'ed(new WeblogEntrySet(getEntrySet#1*).href)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on getUserData
unanalyzed	call on getWebsiteData
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setPermissionMask
unanalyzed	call on getRoller
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:toArray
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:savePermissions
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:flush
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.util.cache. CacheManager:invalidate
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on java.util.List:add
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:size
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getPermissions
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on setEntries
unanalyzed	call on org.jdom.Document:getRootElement
unanalyzed	call on org.jdom.Element:getName
unanalyzed	call on java.lang.String:equals
unanalyzed	call on org.jdom.Element:getChildren
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.jdom.Element:getChild
unanalyzed	call on org.jdom.Element:getText
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle
unanalyzed	call on org.jdom.input.SAXBuilder
unanalyzed	call on org.jdom.input.SAXBuilder:build
unanalyzed	call on getEntrySet
unanalyzed	call on setHref
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.Entry
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.Locale
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.util.TimeZone:getTimeZone
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.Long:longValue
unanalyzed	call on java.util.Date
unanalyzed	call on java.lang.Boolean:valueOf

method	EntrySet putEntry(Reader)
pre	this.memberUri != null
pre	init'ed(this.memberUri.handle)
pre	init'ed(this.memberUri.username)
pre	init'ed(this.urlPrefix)
pre	(soft) this.roller != null
presumption	c.entries@218 != null
presumption	c.entries@219 != null
presumption	c.entries@222 != null
presumption	c.entries@228 != null
presumption	getEntries(...).length@222 <= 1
presumption	getEntries(...).length@228 >= 1
presumption	java.lang.String:equals(...)@238 == 1
presumption	java.lang.String:equals(...)@252 == 1
presumption	java.util.List:size(...)@82 != 0
presumption	java.util.List:toArray(...)@72 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(getEntrySet#1*) num objects == 1
post	init'ed(new MemberEntrySet(getEntrySet#1*). entries)
post	init'ed(new MemberEntrySet(getEntrySet#1*).href)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	init'ed(new MemberEntrySet(toMemberEntrySet#2). entries)
post	new MemberEntrySet(toMemberEntrySet#2).href == &java.lang.StringBuilder:toString(...)
post	new UserEntrySet(getEntrySet#1*) num objects == 0
post	init'ed(new UserEntrySet(getEntrySet#1*).entries)
post	init'ed(new UserEntrySet(getEntrySet#1*).href)
post	new WeblogEntrySet(getEntrySet#1*) num objects == 0
post	init'ed(new WeblogEntrySet(getEntrySet#1*). entries)
post	init'ed(new WeblogEntrySet(getEntrySet#1*).href)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on getUserData
unanalyzed	call on getWebsiteData
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setPermissionMask
unanalyzed	call on getRoller
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:toArray
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:savePermissions
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:flush
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.util.cache. CacheManager:invalidate
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on java.util.List:add
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:size
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getPermissions
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on setEntries
unanalyzed	call on org.jdom.Document:getRootElement
unanalyzed	call on org.jdom.Element:getName
unanalyzed	call on java.lang.String:equals
unanalyzed	call on org.jdom.Element:getChildren
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.jdom.Element:getChild
unanalyzed	call on org.jdom.Element:getText
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle
unanalyzed	call on org.jdom.input.SAXBuilder
unanalyzed	call on org.jdom.input.SAXBuilder:build
unanalyzed	call on getEntrySet
unanalyzed	call on setHref
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.Entry
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.Locale
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.util.TimeZone:getTimeZone
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.Long:longValue
unanalyzed	call on java.util.Date
unanalyzed	call on java.lang.Boolean:valueOf
test_vector	this.memberUri.username: Addr_Set{null}, Inverse{null}

Prev Msg Next Msg

+

click for all messages in this file high

null dereference check fails here: requires entry != null

+

medium

null dereference check might fail: requires not_init'ed(entry)

+

warning

test always goes same way test predetermined because getHandle(...) != null

Prev Msg Next Msg

Prev Msg Next Msg

+

click for all messages in this file warning

unused assignment in callee unused assignment to (entry.handle) in setHandle

+

warning

dead code dead code here because getHandle(...) != null

Prev Msg Next Msg

Prev Msg Next Msg

+

click for all messages in this file warning

dead code dead code here because getName(...) != null

Prev Msg Next Msg

Prev Msg Next Msg

+

click for all messages in this file warning

unused assignment in callee unused assignment to (entry.name) in setName

Prev Msg Next Msg

method	MemberEntrySet createMembers(MemberEntrySet)
pre	c != null
pre	c.entries != null
pre	this.roller != null
pre	init'ed(this.urlPrefix)
presumption	getEntries(...).length@266 <= 2³²-1
presumption	getEntries(...).length@267 in range
presumption	getEntries(...).length@266 <= getEntries(...). length@267
presumption	java.util.List:toArray(...).length@275 <= 2³²-1
presumption	java.util.List:toArray(...)@275 != null
presumption	java.util.List:toArray(...)@72 != null
presumption	org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@263 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	init'ed(new MemberEntrySet(toMemberEntrySet#2). entries)
post	new MemberEntrySet(toMemberEntrySet#2).href == &java.lang.StringBuilder:toString(...)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on getUserData
unanalyzed	call on getWebsiteData
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setUser
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setWebsite
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setPermissionMask
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setPending
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:toArray
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on java.util.List:add
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle

info method not available -- call on UserManager org.apache.roller.weblogger. business.Weblogger:getUserManager()

Prev Msg Next Msg

+

click for all messages in this file high

precondition failure org/apache/roller/weblogger/webservices/adminprotoc ol/RollerMemberHandler.toPermissionsData: entry != null

Prev Msg Next Msg

info method not available -- call on void org.apache.roller.weblogger. business.UserManager:savePermissions(WeblogPermissi on)

info method not available -- call on void org.apache.roller.weblogger. business.Weblogger:flush()

info method not available -- call on User org.apache.roller.weblogger.pojos. WeblogPermission:getUser()

info method not available -- call on void org.apache.roller.weblogger.util. cache.CacheManager:invalidate(User)

info method not available -- call on Weblog org.apache.roller.weblogger. pojos.WeblogPermission:getWebsite()

info method not available -- call on void org.apache.roller.weblogger.util. cache.CacheManager:invalidate(Weblog)

method	WeblogPermission toPermissionsData(MemberEntry)
pre	entry != null
pre	init'ed(entry.handle)
pre	init'ed(entry.name)
pre	entry.permission != null
pre	this.roller != null
post	return_value == &new WeblogPermission(toPermiss ionsData#1)
post	new WeblogPermission(toPermissionsData#1) num objects == 1
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle

info method not available -- call on void org.apache.roller.weblogger.pojos. WeblogPermission()

info method not available -- call on void org.apache.roller.weblogger.pojos. WeblogPermission:setUser(User)

info method not available -- call on void org.apache.roller.weblogger.pojos. WeblogPermission:setWebsite(Weblog)

info method not available -- call on void org.apache.roller.weblogger.pojos. WeblogPermission:setPermissionMask(short)

info method not available -- call on void org.apache.roller.weblogger.pojos. WeblogPermission:setPending(bool)

method	WeblogPermission getPermissionsData(MemberEntry)
pre	entry != null
pre	init'ed(entry.handle)
pre	init'ed(entry.name)
pre	this.roller != null
post	init'ed(return_value)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on getUserData
unanalyzed	call on getWebsiteData
unanalyzed	call on getRoller
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getPermissions
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle

method	WeblogPermission getPermissionsData(String, String)
pre	this.roller != null
presumption	org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@302 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle

method	MemberEntrySet updateMembers(MemberEntrySet)
pre	c != null
pre	c.entries != null
pre	init'ed(this.urlPrefix)
pre	(soft) this.roller != null
presumption	getEntries(...).length@312 <= 2³²-1
presumption	getEntries(...).length@312 <= getEntries(...). length@313
presumption	java.util.List:toArray(...).length@321 <= 2³²-1
presumption	java.util.List:toArray(...)@321 != null
presumption	java.util.List:toArray(...)@72 != null
presumption	org.apache.roller.weblogger.business. UserManager:getPermissions(...)@302 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	init'ed(new MemberEntrySet(toMemberEntrySet#2). entries)
post	new MemberEntrySet(toMemberEntrySet#2).href == &java.lang.StringBuilder:toString(...)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on getUserData
unanalyzed	call on getWebsiteData
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:setPermissionMask
unanalyzed	call on getRoller
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:toArray
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:savePermissions
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:flush
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.util.cache. CacheManager:invalidate
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on java.util.List:add
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getPermissions
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle

Prev Msg Next Msg

+

click for all messages in this file high

precondition failure org/apache/roller/weblogger/webservices/adminprotoc ol/RollerMemberHandler.getPermissionsData: entry != null

Prev Msg Next Msg

Prev Msg Next Msg

+

click for all messages in this file high

precondition failure org/apache/roller/weblogger/webservices/adminprotoc ol/RollerMemberHandler.updatePermissionsData: entry != null

Prev Msg Next Msg

method	void updatePermissionsData(WeblogPermission, MemberEntry)
pre	entry != null
pre	init'ed(entry.handle)
pre	init'ed(entry.name)
pre	init'ed(entry.permission)
pre	this.roller != null
pre	(soft) pd != null
presumption	org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@336 != null
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.String:equalsIgnoreCase
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle
test_vector	entry.permission: Addr_Set{null}, Inverse{null}

info method not available -- call on void org.apache.roller.weblogger.pojos. WeblogPermission:setPermissionMask(short)

info method not available -- call on UserManager org.apache.roller.weblogger. business.Weblogger:getUserManager()

info method not available -- call on void org.apache.roller.weblogger. business.UserManager:savePermissions(WeblogPermissi on)

info method not available -- call on void org.apache.roller.weblogger. business.Weblogger:flush()

info method not available -- call on void org.apache.roller.weblogger.util. cache.CacheManager:invalidate(User)

info method not available -- call on void org.apache.roller.weblogger.util. cache.CacheManager:invalidate(Weblog)

method	EntrySet deleteEntry()
pre	this.memberUri != null
pre	init'ed(this.memberUri.handle)
pre	this.memberUri.username != null
pre	this.roller != null
pre	init'ed(this.urlPrefix)
presumption	org.apache.roller.weblogger.business. UserManager:getPermissions(...)@302 != null
presumption	org.apache.roller.weblogger.business. Weblogger:getUserManager(...)@362 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	init'ed(new MemberEntrySet(toMemberEntrySet#2). entries)
post	new MemberEntrySet(toMemberEntrySet#2).href == &java.lang.StringBuilder:toString(...)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.HandlerException
unanalyzed	call on java.lang.Exception
unanalyzed	call on getUserData
unanalyzed	call on getWebsiteData
unanalyzed	call on getRoller
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getUserManager
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:toArray
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getPermissions
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getUserByUserName
unanalyzed	call on org.apache.roller.weblogger.business. UserManager:getWebsiteByHandle

info method not available -- call on UserManager org.apache.roller.weblogger. business.Weblogger:getUserManager()

info method not available -- call on void org.apache.roller.weblogger. business.UserManager:removePermissions(WeblogPermis sion)

info method not available -- call on void org.apache.roller.weblogger. business.Weblogger:flush()

info method not available -- call on void org.apache.roller.weblogger.util. cache.CacheManager:invalidate(User)

info method not available -- call on void org.apache.roller.weblogger.util. cache.CacheManager:invalidate(Weblog)

method	MemberEntry toMemberEntry(WeblogPermission)
pre	pd != null
pre	init'ed(this.urlPrefix)
presumption	org.apache.roller.weblogger.pojos.WeblogPermission: getUser(...)@386 != null
presumption	org.apache.roller.weblogger.pojos.WeblogPermission: getWebsite(...)@386 != null
post	java.lang.StringBuilder:toString(...)._tainted == this.urlPrefix._tainted
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntry(toMemberEntry# 1)
post	new MemberEntry(toMemberEntry#1) num objects == 1
post	init'ed(return_value.handle)
post	return_value.href == &java.lang. StringBuilder:toString(...)
post	init'ed(return_value.name)
post	return_value.permission == One-of{&"ADMIN", &"AUTHOR", &"LIMITED", null}
post	return_value.permission in Addr_Set{null, &"ADMIN",&"AUTHOR",&"LIMITED"}

info method not available -- call on Weblog org.apache.roller.weblogger. pojos.WeblogPermission:getWebsite()

info method not available -- call on String org.apache.roller.weblogger. pojos.Weblog:getHandle()

info method not available -- call on User org.apache.roller.weblogger.pojos. WeblogPermission:getUser()

info method not available -- call on String org.apache.roller.weblogger. pojos.User:getUserName()

info method not available -- call on short org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask()

method	MemberEntrySet toMemberEntrySet(WeblogPermission[] )
pre	pds != null
pre	pds.length <= 2³²-1
pre	init'ed(this.urlPrefix)
pre	(soft) pds[...] != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &new MemberEntrySet(toMemberEnt rySet#2)
post	new MemberEntrySet(toMemberEntrySet#2) num objects == 1
post	init'ed(return_value.entries)
post	return_value.href == &java.lang. StringBuilder:toString(...)
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getUser
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getWebsite
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on org.apache.roller.weblogger.pojos. User:getUserName
unanalyzed	call on getUrlPrefix
unanalyzed	call on org.apache.roller.weblogger.pojos. WeblogPermission:getPermissionMask
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on java.util.Arrays:asList

Prev Msg Next Msg

+

click for all messages in this file warning

unused assignment in callee unused assignment to (new MemberEntry(toMemberEntry #1).permission) in toMemberEntry

Prev Msg Next Msg

method	String maskToString(short)
presumption	init'ed(org.apache.roller.weblogger.pojos. WeblogPermission.ADMIN)
presumption	init'ed(org.apache.roller.weblogger.pojos. WeblogPermission.AUTHOR)
presumption	init'ed(org.apache.roller.weblogger.pojos. WeblogPermission.LIMITED)
post	return_value in Addr_Set{null,&"LIMITED", &"AUTHOR",&"ADMIN"}

method	short stringToMask(String)
pre	s != null
presumption	init'ed(org.apache.roller.weblogger.pojos. WeblogPermission.ADMIN)
presumption	init'ed(org.apache.roller.weblogger.pojos. WeblogPermission.AUTHOR)
presumption	init'ed(org.apache.roller.weblogger.pojos. WeblogPermission.LIMITED)
post	return_value == One-of{org.apache.roller.weblogger. pojos.WeblogPermission.ADMIN, org.apache.roller. weblogger.pojos.WeblogPermission.AUTHOR, org.apache.roller.weblogger.pojos.WeblogPermission .LIMITED, 0}
post	(soft) init'ed(return_value)
test_vector	java.lang.String:equalsIgnoreCase(...)@426: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@429: {0}, {1}
test_vector	java.lang.String:equalsIgnoreCase(...)@432: {0}, {1}

	info	method not available	-- call on UserManager org.apache.roller.weblogger. business.Weblogger:getUserManager()
	info	method not available	-- call on List org.apache.roller.weblogger. business.UserManager:getUsers(Weblog, Boolean, Date, Date, int, int)

	info	method not available	-- call on User org.apache.roller.weblogger.pojos. WeblogPermission:getUser()
	info	method not available	-- call on void org.apache.roller.weblogger.util. cache.CacheManager:invalidate(User)

	info	method not available	-- call on Weblog org.apache.roller.weblogger. pojos.WeblogPermission:getWebsite()
	info	method not available	-- call on void org.apache.roller.weblogger.util. cache.CacheManager:invalidate(Weblog)