Messages

Last Msg First Msg

method

org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service$Workspace$Attributes__sta tic_init

method

org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service$Workspace$Collection$Tags __static_init

method

org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service$Workspace$Collection$Attr ibutes__static_init

method

org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service$Workspace$Collection__sta tic_init

method

org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service__static_init

method

org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service$Workspace__static_init

method	void org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service(String)
post	this.entries == null
post	this.href == href
post	init'ed(this.href)

method	void org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service(Document)
pre	d != null
post	init'ed(this.entries)
post	init'ed(this.href)
unanalyzed	call on org.jdom.Document:getRootElement
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.jdom.Element:getChildren
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service$Workspace
unanalyzed	call on populate
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:toArray
unanalyzed	call on setEntries
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on org.jdom.Element:getAttributeValue
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.Entry
unanalyzed	call on setHref
unanalyzed	call on org.jdom.Element:getChild
unanalyzed	call on org.jdom.Element:getText
unanalyzed	call on java.util.Arrays:asList

method	void org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service(InputStream)
presumption	org.jdom.input.SAXBuilder:build(...)@57 != null
post	init'ed(this.entries)
post	init'ed(this.href)
unanalyzed	call on org.jdom.Document:getRootElement
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.jdom.Element:getChildren
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service$Workspace
unanalyzed	call on populate
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:toArray
unanalyzed	call on setEntries
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on org.jdom.Element:getAttributeValue
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.Entry
unanalyzed	call on setHref
unanalyzed	call on org.jdom.Element:getChild
unanalyzed	call on org.jdom.Element:getText
unanalyzed	call on java.util.Arrays:asList

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

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

method	String getType()
post	return_value == &"service"

method	Document toDocument()
pre	this.entries != null
presumption	getEntries(...).length@70 <= 2³²-1
presumption	getEntries(...).length@71 >= 1
presumption	getEntries(...).length@70 <= getEntries(...). length@71
presumption	java.util.List:toArray(...)@72 != null
presumption	toDocument(...)@72 != null
post	return_value == &new Document(toDocument#1)
post	new Document(toDocument#1) num objects == 1
unanalyzed	call on java.util.List:toArray

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

info method not available -- call on void org.jdom.Element(String, Namespace)

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

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)

info call too complex - analysis skipped -- call on Document toDocument()

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

info method not available -- call on Element org.jdom.Element:addContent(Cont ent)

Prev Msg Next Msg

method	void populate(Document)
pre	doc != null
presumption	java.util.Iterator:next(...)@84 != null
presumption	org.jdom.Document:getRootElement(...)@79 != null
presumption	org.jdom.Element:getChildren(...)@81 != null
post	init'ed(this.entries)
unanalyzed	call on setEntries
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet
unanalyzed	call on org.jdom.Element:getAttributeValue
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.jdom.Element:getChildren
unanalyzed	call on java.util.List:iterator
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.Entry
unanalyzed	call on setHref
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
unanalyzed	call on java.util.Arrays:asList
test_vector	java.util.Iterator:hasNext(...)@83: {0}, {1}

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

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

method	void org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service$Workspace()
post	this.entries == null
post	this.href == null
post	this.title == null

method	String getType()
post	return_value == &"workspace"

method	String getTitle()
pre	init'ed(this.title)
post	return_value == this.title
post	init'ed(return_value)

method	void setTitle(String)
post	this.title == title
post	init'ed(this.title)

method	Document toDocument()
pre	this.entries != null
pre	init'ed(this.title)
presumption	getEntries(...).length@123 <= 2³²-1
presumption	getEntries(...).length@124 >= 1
presumption	getEntries(...).length@123 <= getEntries(...). length@124
presumption	java.util.List:toArray(...)@72 != null
presumption	toDocument(...)@125 != null
post	return_value == &new Document(toDocument#1)
post	new Document(toDocument#1) num objects == 1
unanalyzed	call on java.util.List:toArray

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

info method not available -- call on void org.jdom.Element(String, Namespace)

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

info method not available -- call on Element org.jdom.Element:setAttribute(St ring, String)

method	void populate(Element)
pre	elem != null
presumption	java.util.Iterator:next(...)@137 != null
presumption	org.jdom.Element:getChildren(...)@134 != null
post	init'ed(this.entries)
post	init'ed(this.title)
unanalyzed	call on org.apache.roller.weblogger.webservices. adminprotocol.sdk.Entry
unanalyzed	call on org.jdom.Element:getAttributeValue
unanalyzed	call on setHref
unanalyzed	call on org.jdom.Element:getChild
unanalyzed	call on org.jdom.Element:getText
unanalyzed	call on java.util.Arrays:asList
test_vector	java.util.Iterator:hasNext(...)@136: {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 , Namespace)

method	void org.apache.roller.weblogger.webservices. adminprotocol.sdk.Service$Workspace$Collection()
post	this.href == null

method	String getType()
post	return_value == &"collection"

method	String getTitle()
pre	init'ed(this.title)
post	return_value == this.title
post	init'ed(return_value)

method	void setTitle(String)
post	this.title == title
post	init'ed(this.title)

method	Document toDocument()
pre	init'ed(this.href)
pre	init'ed(this.memberType)
pre	init'ed(this.title)
post	return_value == &new Document(toDocument#1)
post	new Document(toDocument#1) num objects == 1

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

info method not available -- call on void org.jdom.Element(String, Namespace)

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

info method not available -- call on Element org.jdom.Element:setAttribute(St ring, String)

info method not available -- call on void org.jdom.Element(String, Namespace)

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

info method not available -- call on Element org.jdom.Element:addContent(Cont ent)

method	void populate(Element)
pre	elem != null
presumption	org.jdom.Element:getChild(...)@196 != null
post	init'ed(this.href)
post	init'ed(this.memberType)
post	init'ed(this.title)

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

info method not available -- call on Element org.jdom.Element:getChild(String , Namespace)

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

method	String getMemberType()
pre	init'ed(this.memberType)
post	return_value == this.memberType
post	init'ed(return_value)

method	void setMemberType(String)
post	this.memberType == memberType
post	init'ed(this.memberType)