Messages

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

method	String getName()
pre	init'ed(this.name)
post	return_value == this.name
post	init'ed(return_value)

method	void setName(String)
post	this.name != null
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.String:replaceAll

method	String getPermalink()
pre	this.blog != null
pre	init'ed(this.name)
post	return_value != null
pre	(soft) net/sourceforge/pebble/domain/BlogManager. instance != null
pre	(soft) init'ed(net/sourceforge/pebble/domain/BlogMa nager.instance.multiBlog)
pre	(soft) init'ed(this.blog.id)
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on net.sourceforge.pebble.PebbleContext:getIns tance
unanalyzed	call on net.sourceforge.pebble.PebbleContext:getCon figuration
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring

method	int hashCode()
pre	this.name != null
post	init'ed(return_value)

method	bool equals(Object)
pre	(soft) o.name != null
pre	(soft) init'ed(this.name)
post	init'ed(return_value)

method	int compareTo(Object)
pre	o != null
pre	init'ed(o.name)
pre	this.name != null
post	init'ed(return_value)

method	String toString()
pre	init'ed(this.name)
post	return_value == this.name
post	init'ed(return_value)

method	int getRank()
pre	init'ed(this.rank)
post	return_value == this.rank
post	init'ed(return_value)

method	List parse(Blog, String)
presumption	s.length@168 <= 2³²-1
presumption	s[i]@168 != null
post	return_value == &new ArrayList(parse#1)
post	new ArrayList(parse#1) num objects == 1
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.String:replaceAll
test_vector	tags: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:length(...)@167: {0}, {1..2³²-1}
test_vector	java.util.List:contains(...)@171: {1}, {0}

info method not available -- call on String net.sourceforge.pebble.util. StringUtils:transformHTML(String)

method	String format(List)
presumption	java.util.Iterator:next(...)@192 != null
post	return_value != null
test_vector	tags: Addr_Set{null}, Inverse{null}
test_vector	java.util.Iterator:hasNext(...)@191: {1}, {0}
test_vector	java.util.Iterator:hasNext(...)@194: {0}, {1}

method	String encode(String)
post	return_value != null
test_vector	tag: Inverse{null}, Addr_Set{null}