Messages

Last Msg First Msg

method

org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet$Types__static_init

method

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

method	void org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet()
post	this.entries == null
post	this.href == null

method	Entry[] getEntries()
pre	this.entries != null
post	init'ed(return_value)

method	void setEntries(Entry[])
post	init'ed(this.entries)

method	bool isEmpty()
pre	init'ed(this.entries)
post	init'ed(return_value)

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

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

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

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

Prev Msg Next Msg

+

click for all messages in this file high

null dereference check fails here: requires getEntries(...)[i] != null

+

medium

null dereference check might fail: requires not_init'ed(getEntries(. ..)[i])

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	bool equals(Object)
pre	(soft) o.entries != null
pre	(soft) init'ed(o.href)
pre	(soft) this.entries != null
pre	(soft) init'ed(this.href)
post	init'ed(return_value)
unanalyzed	call on java.util.List:toArray
test_vector	o: Addr_Set{null}, Inverse{null}
test_vector	org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet:areEqual(...)@108: {1}, {0}
test_vector	org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet:areEqual(...)@111: {1}, {0}
test_vector	org.apache.roller.weblogger.webservices. adminprotocol.sdk.EntrySet:areEqual(...)@114: {1}, {0}

info method not available -- call on bool org.apache.roller.weblogger. webservices.adminprotocol.sdk.EntrySet:areEqual(Obj ect, Object)

info method not available -- call on bool org.apache.roller.weblogger. webservices.adminprotocol.sdk.EntrySet:areEqual(Obj ect[], Object[])