Messages

method

void org.apache.roller.weblogger.ui.core.util. menu.MenuHelper()

method	org.apache.roller.weblogger.ui.core.util.menu. MenuHelper__static_init
presumption	java.lang.Class:getResourceAsStream(...)@53 != null
presumption	java.lang.Class:getResourceAsStream(...)@56 != null
presumption	org.apache.commons.logging.LogFactory:getLog(... )@44 != null
post	(soft) log != null
post	menus == &new Hashtable(MenuHelper__static_ init#1)
post	new Hashtable(MenuHelper__static_init#1) num objects == 1
unanalyzed	call on org.jdom.Element:getAttributeValue
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.jdom.Element:getChildren
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add
unanalyzed	call on org.jdom.input.SAXBuilder
unanalyzed	call on org.jdom.input.SAXBuilder:build
unanalyzed	call on org.jdom.Document:getRootElement

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

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

method	Menu getMenu(String, String, User, Weblog)
pre	(soft) currentAction != null
pre	(soft) log != null
pre	(soft) menus != null
pre	(soft) user != null
pre	(soft) weblog != null
presumption	menuConfig.tabs@75 != null
post	return_value in Addr_Set{null,&new Menu(buildMenu#2)}
post	new ArrayList(Menu#1) num objects <= 1
post	new Menu(buildMenu#2) num objects <= 1
post	new Menu(buildMenu#2).tabs == &new ArrayList(Menu#1)
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.apache.roller.weblogger.config. WebloggerRuntimeConfig:getProperty
unanalyzed	call on org.apache.roller.weblogger.config. WebloggerRuntimeConfig:getBooleanProperty
unanalyzed	call on org.apache.roller.weblogger.config. WebloggerConfig:getBooleanProperty
unanalyzed	call on java.lang.String:equals
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:hasUserPermissions
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.apache.roller.weblogger.pojos. User:hasRole
unanalyzed	call on java.util.List:add
test_vector	menuId: Inverse{null}, Addr_Set{null}
test_vector	java.util.Hashtable:get(...)@75: Addr_Set{null}, Inverse{null}

method	Menu buildMenu(ParsedMenu, String, User, Weblog)
pre	log != null
pre	menuConfig != null
pre	menuConfig.tabs != null
pre	(soft) currentAction != null
pre	(soft) user != null
pre	(soft) weblog != null
presumption	configTab.tabItems@95 != null
presumption	configTabItem.subActions.length@133 <= 2³²-1
presumption	java.util.Iterator:next(...)@133 != null
presumption	java.util.Iterator:next(...)@95 != null
post	return_value == &new Menu(buildMenu#2)
post	new ArrayList(Menu#1) num objects == 1
post	new Menu(buildMenu#2) num objects == 1
post	return_value.tabs == &new ArrayList(Menu#1)
unanalyzed	call on org.apache.roller.weblogger.config. WebloggerRuntimeConfig:getProperty
unanalyzed	call on org.apache.roller.weblogger.config. WebloggerRuntimeConfig:getBooleanProperty
unanalyzed	call on org.apache.roller.weblogger.config. WebloggerConfig:getBooleanProperty
unanalyzed	call on java.lang.String:equals
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:hasUserPermissions
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:add
test_vector	configTab.disabledProperty@95: Addr_Set{null}, Inverse{null}
test_vector	configTab.enabledProperty@95: Addr_Set{null}, Inverse{null}
test_vector	configTab.role@95: Addr_Set{null}, Inverse{null}
test_vector	configTabItem.disabledProperty@133: Addr_Set{null}, Inverse{null}
test_vector	configTabItem.enabledProperty@133: Addr_Set{null}, Inverse{null}
test_vector	configTabItem.role@133: Addr_Set{null}, Inverse{null}
test_vector	java.util.Iterator:hasNext(...)@132: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@94: {0}, {1}
test_vector	org.apache.roller.weblogger.pojos.User:hasRole(... )@110: {1}, {0}
test_vector	org.apache.roller.weblogger.pojos.User:hasRole(... )@147: {1}, {0}

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

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

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

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

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

method	bool isPermitted(String, User, Weblog)
pre	(soft) weblog != 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	init'ed(return_value)
test_vector	perm: Inverse{null}, Addr_Set{null}
test_vector	java.lang.String:equals(...)@198: {0}, {1}
test_vector	java.lang.String:equals(...)@200: {0}, {1}
test_vector	java.lang.String:equals(...)@202: {0}, {1}

info method not available -- call on bool org.apache.roller.weblogger.pojos. Weblog:hasUserPermissions(User, short)

method	bool getBooleanProperty(String)
post	init'ed(return_value)
test_vector	org.apache.roller.weblogger.config.WebloggerRuntime Config:getProperty(...)@214: Addr_Set{null}, Inverse{null}

info method not available -- call on String org.apache.roller.weblogger. config.WebloggerRuntimeConfig:getProperty(String)

info method not available -- call on bool org.apache.roller.weblogger.config. WebloggerRuntimeConfig:getBooleanProperty(String)

info method not available -- call on bool org.apache.roller.weblogger.config. WebloggerConfig:getBooleanProperty(String)

method	bool isSelected(String, ParsedTabItem)
pre	currentAction != null
pre	tabItem != null
pre	init'ed(tabItem.action)
pre	(soft) init'ed(tabItem.subActions)
pre	(soft) tabItem.subActions.length <= 2³²-1
pre	(soft) init'ed(tabItem.subActions[...])
post	init'ed(return_value)
test_vector	tabItem.subActions: Addr_Set{null}, Inverse{null}
test_vector	tabItem.subActions.length: {0}, {1..2³²-1}
test_vector	java.lang.String:equals(...)@222: {0}, {1}
test_vector	java.lang.String:equals(...)@230: {0}, {1}

method	ParsedMenu unmarshall(InputStream)
pre	instream != null
presumption	java.util.Iterator:next(...)@259 != null
presumption	org.jdom.Document:getRootElement(...)@255 != null
presumption	org.jdom.Element:getChildren(...)@256 != null
presumption	org.jdom.input.SAXBuilder:build(...)@253 != null
post	return_value == &new ParsedMenu(unmarshall#1)
post	new ArrayList(ParsedMenu#1) num objects == 1
post	new ParsedMenu(unmarshall#1) num objects == 1
post	return_value.tabs == &new ArrayList(ParsedMenu# 1)
unanalyzed	call on org.jdom.Element:getAttributeValue
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.jdom.Element:getChildren
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add
test_vector	java.util.Iterator:hasNext(...)@258: {0}, {1}

info method not available -- call on void org.jdom.input.SAXBuilder()

info method not available -- call on Document org.jdom.input.SAXBuilder:build (InputStream)

info method not available -- call on Element org.jdom.Document:getRootElement ()

info method not available -- call on List org.jdom.Element:getChildren(String )

method	ParsedTab elementToParsedTab(Element)
pre	element != null
presumption	java.util.Iterator:next(...)@280 != null
presumption	org.jdom.Element:getChildren(...)@277 != null
post	return_value == &new ParsedTab(elementToParsedT ab#1)
post	new ArrayList(ParsedTab#1) num objects == 1
post	new ParsedTab(elementToParsedTab#1) num objects == 1
post	init'ed(return_value.disabledProperty)
post	init'ed(return_value.enabledProperty)
post	init'ed(return_value.name)
post	init'ed(return_value.perm)
post	init'ed(return_value.role)
post	return_value.tabItems == &new ArrayList(ParsedT ab#1)
unanalyzed	call on org.jdom.Element:getAttributeValue
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:add
test_vector	java.util.Iterator:hasNext(...)@279: {0}, {1}

info method not available -- call on String org.jdom.Element:getAttributeValu e(String)

info method not available -- call on List org.jdom.Element:getChildren(String )

method	ParsedTabItem elementToParsedTabItem(Element)
pre	element != null
post	java.lang.String:split(...)._tainted == 0
post	return_value == &new ParsedTabItem(elementToPar sedTabItem#1)
post	new ParsedTabItem(elementToParsedTabItem#1) num objects == 1
post	init'ed(return_value.action)
post	init'ed(return_value.disabledProperty)
post	init'ed(return_value.enabledProperty)
post	init'ed(return_value.name)
post	init'ed(return_value.perm)
post	init'ed(return_value.role)
post	return_value.subActions in Addr_Set{null,&java. lang.String:split(...)}
test_vector	org.jdom.Element:getAttributeValue(...)@295: Addr_Set{null}, Inverse{null}

info method not available -- call on String org.jdom.Element:getAttributeValu e(String)