Messages

Last Msg First Msg

method

org.apache.roller.weblogger.webservices. atomprotocol.Collection__static_init

method	void org.apache.roller.weblogger.webservices. atomprotocol.Collection(String, String, String)
post	this.accept == &"entry"
post	this.accepts == &new ArrayList(Collection#2)
post	this.categories == &new ArrayList(Collection#1)
post	this.href == href
post	init'ed(this.href)
post	this.listTemplate == null
post	this.title == title
post	init'ed(this.title)
post	this.titleType == titleType
post	init'ed(this.titleType)
post	new ArrayList(Collection#1) num objects == 1
post	new ArrayList(Collection#2) num objects == 1

method	List getAccepts()
pre	init'ed(this.accepts)
post	return_value == this.accepts
post	init'ed(return_value)

method	void addAccept(String)
pre	this.accepts != null

method	void setAccepts(List)
post	this.accepts == accepts
post	init'ed(this.accepts)

method	String getHref()
pre	init'ed(this.href)
post	return_value == this.href
post	init'ed(return_value)

method	void setHref(String)
post	this.href == href
post	init'ed(this.href)

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	String getTitleType()
pre	init'ed(this.titleType)
post	return_value == this.titleType
post	init'ed(return_value)

method	void setTitleType(String)
post	this.titleType == titleType
post	init'ed(this.titleType)

method	void addCategories(Categories)
pre	this.categories != null

method	List getCategories()
pre	init'ed(this.categories)
post	return_value == this.categories
post	init'ed(return_value)

method	bool accepts(String)
pre	init'ed(this.accept)
pre	(soft) ct != null
pre	(soft) this.accepts != null
presumption	java.lang.String:indexOf(...)@128 <= 2³²-2
presumption	java.util.List:size(...)@124 >= 0
presumption	java.util.List:toArray(...)@124 != null
presumption	rules.length@124 <= 2³²-1
post	init'ed(return_value)
test_vector	this.accept: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:equals(...)@114: {0}, {1}
test_vector	java.lang.String:equals(...)@116: {0}, {1}
test_vector	java.lang.String:equals(...)@119: {0}, {1}
test_vector	java.lang.String:equals(...)@121: {0}, {1}
test_vector	java.lang.String:equals(...)@127: {0}, {1}
test_vector	java.lang.String:indexOf(...)@128: {-2³¹. .0}, {1..2³²-2}
test_vector	java.lang.String:startsWith(...)@131: {0}, {1}

Prev Msg Next Msg

+

click for all messages in this file medium

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

Prev Msg Next Msg

method	Element collectionToElement(Collection)
pre	collection != null
pre	collection.accepts != null
pre	collection.categories != null
pre	init'ed(collection.href)
pre	init'ed(collection.title)
pre	init'ed(collection.titleType)
pre	init'ed(org/apache/roller/weblogger/webservices/ato mprotocol/AtomService.ATOM_FORMAT)
pre	init'ed(org/apache/roller/weblogger/webservices/ato mprotocol/AtomService.ATOM_PROTOCOL)
presumption	cats.categories@154 != null
presumption	java.util.Iterator:next(...)@154 != null
presumption	java.util.Iterator:next(...)@162 != null
post	return_value == &new Element(collectionToElemen t#1)
post	new Element(collectionToElement#1) num objects == 1
test_vector	collection.titleType: Addr_Set{null}, Inverse{null}
test_vector	cats.scheme@154: Addr_Set{null}, Inverse{null}
test_vector	com.sun.syndication.feed.atom.Category:getLabel(... )@168: Addr_Set{null}, Inverse{null}
test_vector	com.sun.syndication.feed.atom.Category:getScheme(.. .)@165: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:equals(...)@148: {1}, {0}
test_vector	java.util.Iterator:hasNext(...)@153: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@161: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@176: {0}, {1}

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

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)

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:setAttribute(St ring, String)

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

info method not available -- call on String com.sun.syndication.feed.atom. Category:getTerm()

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

info method not available -- call on String com.sun.syndication.feed.atom. Category:getScheme()

info method not available -- call on String com.sun.syndication.feed.atom. Category:getScheme()

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

info method not available -- call on String com.sun.syndication.feed.atom. Category:getLabel()

info method not available -- call on String com.sun.syndication.feed.atom. Category:getLabel()

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

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

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	Collection elementToCollection(Element)
pre	element != null
pre	init'ed(org/apache/roller/weblogger/webservices/ato mprotocol/AtomService.ATOM_FORMAT)
pre	init'ed(org/apache/roller/weblogger/webservices/ato mprotocol/AtomService.ATOM_PROTOCOL)
presumption	java.util.Iterator:next(...)@200 != null
presumption	java.util.Iterator:next(...)@208 != null
presumption	java.util.Iterator:next(...)@216 != null
presumption	org.jdom.Element:getAttribute(...)@188 != null
presumption	org.jdom.Element:getAttribute(...)@193 != null
presumption	org.jdom.Element:getChild(...)@189 != null
presumption	org.jdom.Element:getChildren(...)@206 != null
presumption	org.jdom.Element:getChildren(...)@214 != null
post	return_value == &new Collection(elementToCollec tion#1)
post	new ArrayList(Collection#1) num objects == 1
post	new ArrayList(Collection#2) num objects == 1
post	new Collection(elementToCollection#1) num objects == 1
post	return_value.accept == &"entry"
post	return_value.accepts == &new ArrayList(Collecti on#2)
post	return_value.categories == &new ArrayList(Collection#1)
post	init'ed(return_value.href)
post	return_value.listTemplate == null
post	init'ed(return_value.title)
post	init'ed(return_value.titleType)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:add
test_vector	java.lang.String:equals(...)@210: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@199: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@207: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@215: {0}, {1}
test_vector	java.util.List:size(...)@198: {-2³¹..0}, {1..2³²-1}
test_vector	org.jdom.Element:getAttribute(...)@192: Addr_Set{null}, Inverse{null}
test_vector	org.jdom.Element:getChildren(...)@197: Addr_Set{null}, Inverse{null}

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

info method not available -- call on String org.jdom.Attribute:getValue()

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

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

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

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

info method not available -- call on String org.jdom.Attribute:getValue()

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

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

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

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

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

info method not available -- call on void com.sun.syndication.feed.atom. Category()

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

info method not available -- call on void com.sun.syndication.feed.atom. Category:setTerm(String)

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

info method not available -- call on void com.sun.syndication.feed.atom. Category:setLabel(String)

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

info method not available -- call on void com.sun.syndication.feed.atom. Category:setScheme(String)

	info	method not available	-- call on String com.sun.syndication.feed.atom. Category:getTerm()
	info	method not available	-- call on Element org.jdom.Element:setAttribute(St ring, String)

	info	method not available	-- call on Attribute org.jdom.Element:getAttribute( String)
	info	method not available	-- call on String org.jdom.Attribute:getValue()

	info	method not available	-- call on String org.jdom.Element:getAttributeValu e(String)
	info	method not available	-- call on void com.sun.syndication.feed.atom. Category:setTerm(String)