Messages

Last Msg First Msg

method

net.sourceforge.pebble.domain.CategoryBuilder__ static_init

method	void net.sourceforge.pebble.domain. CategoryBuilder(Blog)
post	this.blog == blog
post	init'ed(this.blog)

method	void net.sourceforge.pebble.domain. CategoryBuilder(Blog, Category)
post	this.blog == blog
post	init'ed(this.blog)
post	this.rootCategory == rootCategory
post	init'ed(this.rootCategory)

method	void addCategory(Category)
pre	category != null
pre	category.id != null
pre	(soft) init'ed(this.rootCategory)
pre	(soft) this.blog != null
post	possibly_updated(category.blog)
post	possibly_updated(category.parent)
post	(soft) init'ed(this.rootCategory)
post	init'ed(new ArrayList(Category#1) num objects)
post	init'ed(new ArrayList(Category#2) num objects)
post	init'ed(new ArrayList(Category#3) num objects)
post	init'ed(new Category(getCategory#2) num objects)
post	possibly_updated(new Category(getCategory#2). subCategories)
post	possibly_updated(new Category(getCategory#2).blog)
post	init'ed(new Category(getCategory#2).blogEntries)
post	possibly_updated(new Category(getCategory#2).id)
post	init'ed(new Category(getCategory#2).name)
post	possibly_updated(new Category(getCategory#2). parent)
post	init'ed(new Category(getCategory#2).tags)
post	init'ed(new Category(getCategory#2).tagsAsList)
post	init'ed(new Category(getCategory#3) num objects)
post	possibly_updated(new Category(getCategory#3).blog)
post	init'ed(new Category(getCategory#3).blogEntries)
post	possibly_updated(new Category(getCategory#3).id)
unanalyzed	call on getSubCategories
post	init'ed(new Category(getCategory#3).name)
post	possibly_updated(new Category(getCategory#3). parent)
post	possibly_updated(new Category(getCategory#3). subCategories)
post	init'ed(new Category(getCategory#3).tags)
post	init'ed(new Category(getCategory#3).tagsAsList)
unanalyzed	call on java.util.Collections:unmodifiableList
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getCategory
unanalyzed	call on java.util.List:contains
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getLocale
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on net.sourceforge.pebble.domain.Category
unanalyzed	call on java.lang.String:equals
unanalyzed	call on net.sourceforge.pebble.util. I18n:getMessage
unanalyzed	call on getId
unanalyzed	call on java.util.ArrayList
unanalyzed	call on addCategory
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on setBlog
unanalyzed	call on isRootCategory
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on addSubCategory
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.util.List:add
test_vector	java.lang.String:equals(...)@142: {0}, {1}

Prev Msg Next Msg

click for all messages in this file medium

null dereference check might fail: requires parent != null

Prev Msg Next Msg

method	void removeCategory(Category)
pre	category != null
pre	category.id != null
pre	(soft) init'ed(this.rootCategory)
pre	(soft) this.blog != null
post	possibly_updated(category.parent)
post	init'ed(this.rootCategory)
post	init'ed(new ArrayList(Category#1) num objects)
post	init'ed(new ArrayList(Category#2) num objects)
post	init'ed(new ArrayList(Category#3) num objects)
post	init'ed(new Category(getCategory#2) num objects)
post	possibly_updated(new Category(getCategory#2).blog)
post	init'ed(new Category(getCategory#2).blogEntries)
post	possibly_updated(new Category(getCategory#2).id)
post	init'ed(new Category(getCategory#2).name)
post	possibly_updated(new Category(getCategory#2). parent)
post	(soft) init'ed(new Category(getCategory#2). subCategories)
post	init'ed(new Category(getCategory#2).tags)
post	init'ed(new Category(getCategory#2).tagsAsList)
post	init'ed(new Category(getCategory#3) num objects)
post	possibly_updated(new Category(getCategory#3).blog)
post	init'ed(new Category(getCategory#3).blogEntries)
post	possibly_updated(new Category(getCategory#3).id)
post	init'ed(new Category(getCategory#3).name)
unanalyzed	call on getSubCategories
post	possibly_updated(new Category(getCategory#3). parent)
post	(soft) init'ed(new Category(getCategory#3). subCategories)
post	init'ed(new Category(getCategory#3).tags)
post	init'ed(new Category(getCategory#3).tagsAsList)
unanalyzed	call on java.util.Collections:unmodifiableList
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getCategory
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.util.List:remove
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getLocale
unanalyzed	call on getParent
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on net.sourceforge.pebble.domain.Category
unanalyzed	call on java.lang.String:equals
unanalyzed	call on net.sourceforge.pebble.util. I18n:getMessage
unanalyzed	call on java.util.ArrayList
unanalyzed	call on getId
unanalyzed	call on addCategory
unanalyzed	call on setBlog
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on isRootCategory
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on addSubCategory
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.util.List:add

Prev Msg Next Msg

click for all messages in this file medium

null dereference check might fail: requires parent != null

Prev Msg Next Msg

method	Category getParent(Category, bool)
pre	category != null
pre	category.id != null
pre	(soft) init'ed(this.rootCategory)
pre	(soft) this.blog != null
post	init'ed(return_value)
post	init'ed(this.rootCategory)
post	init'ed(new ArrayList(Category#1) num objects)
post	init'ed(new ArrayList(Category#2) num objects)
post	init'ed(new ArrayList(Category#3) num objects)
post	init'ed(new Category(getCategory#2) num objects)
post	possibly_updated(new Category(getCategory#2).blog)
post	init'ed(new Category(getCategory#2).blogEntries)
post	possibly_updated(new Category(getCategory#2).id)
post	init'ed(new Category(getCategory#2).name)
post	possibly_updated(new Category(getCategory#2). parent)
post	possibly_updated(new Category(getCategory#2). subCategories)
post	init'ed(new Category(getCategory#2).tags)
post	init'ed(new Category(getCategory#2).tagsAsList)
post	init'ed(new Category(getCategory#3) num objects)
post	possibly_updated(new Category(getCategory#3).blog)
post	init'ed(new Category(getCategory#3).blogEntries)
post	possibly_updated(new Category(getCategory#3).id)
post	init'ed(new Category(getCategory#3).name)
post	possibly_updated(new Category(getCategory#3). parent)
post	possibly_updated(new Category(getCategory#3). subCategories)
post	init'ed(new Category(getCategory#3).tags)
unanalyzed	call on getSubCategories
post	init'ed(new Category(getCategory#3).tagsAsList)
unanalyzed	call on java.util.Collections:unmodifiableList
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getCategory
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getLocale
unanalyzed	call on net.sourceforge.pebble.domain.Category
unanalyzed	call on java.lang.String:equals
unanalyzed	call on net.sourceforge.pebble.util. I18n:getMessage
unanalyzed	call on java.util.ArrayList
unanalyzed	call on addCategory
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on getId
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on setBlog
unanalyzed	call on isRootCategory
unanalyzed	call on java.util.List:add
test_vector	java.lang.String:equals(...)@111: {0}, {1}
unanalyzed	call on addSubCategory

method	Category getParent(Category)
pre	category != null
pre	category.id != null
pre	(soft) init'ed(this.rootCategory)
pre	(soft) this.blog != null
post	init'ed(return_value)
post	init'ed(this.rootCategory)
post	init'ed(new ArrayList(Category#1) num objects)
post	init'ed(new ArrayList(Category#2) num objects)
post	init'ed(new ArrayList(Category#3) num objects)
post	init'ed(new Category(getCategory#2) num objects)
post	possibly_updated(new Category(getCategory#2).blog)
post	init'ed(new Category(getCategory#2).blogEntries)
post	possibly_updated(new Category(getCategory#2).id)
post	init'ed(new Category(getCategory#2).name)
post	possibly_updated(new Category(getCategory#2). parent)
post	possibly_updated(new Category(getCategory#2). subCategories)
post	init'ed(new Category(getCategory#2).tags)
post	init'ed(new Category(getCategory#2).tagsAsList)
post	init'ed(new Category(getCategory#3) num objects)
post	possibly_updated(new Category(getCategory#3).blog)
post	init'ed(new Category(getCategory#3).blogEntries)
post	possibly_updated(new Category(getCategory#3).id)
post	init'ed(new Category(getCategory#3).name)
post	possibly_updated(new Category(getCategory#3). parent)
post	possibly_updated(new Category(getCategory#3). subCategories)
post	init'ed(new Category(getCategory#3).tags)
post	init'ed(new Category(getCategory#3).tagsAsList)
unanalyzed	call on java.util.Collections:unmodifiableList
unanalyzed	call on getSubCategories
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getCategory
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:equals
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getLocale
unanalyzed	call on net.sourceforge.pebble.util. I18n:getMessage
unanalyzed	call on java.util.ArrayList
unanalyzed	call on net.sourceforge.pebble.domain.Category
unanalyzed	call on addCategory
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on getId
unanalyzed	call on java.util.List:add
unanalyzed	call on setBlog
unanalyzed	call on isRootCategory
unanalyzed	call on addSubCategory

method	Category getCategory(String, bool)
pre	(soft) init'ed(this.rootCategory)
pre	(soft) this.blog != null
presumption	category.id@165 != null
presumption	java.util.Collections:unmodifiableList(...)@230 != null
presumption	java.util.Iterator:next(...)@165 != null
post	init'ed(return_value)
post	(soft) init'ed(this.rootCategory)
post	init'ed(new ArrayList(Category#1) num objects)
post	init'ed(new ArrayList(Category#2) num objects)
post	init'ed(new ArrayList(Category#3) num objects)
post	new Category(getCategory#2) num objects <= 1
post	init'ed(new Category(getCategory#2) num objects)
post	possibly_updated(new Category(getCategory#2).blog)
post	init'ed(new Category(getCategory#2).blogEntries)
post	possibly_updated(new Category(getCategory#2).id)
post	init'ed(new Category(getCategory#2).name)
post	possibly_updated(new Category(getCategory#2). parent)
post	possibly_updated(new Category(getCategory#2). subCategories)
post	init'ed(new Category(getCategory#2).tags)
post	init'ed(new Category(getCategory#2).tagsAsList)
post	init'ed(new Category(getCategory#3) num objects)
post	possibly_updated(new Category(getCategory#3).blog)
post	init'ed(new Category(getCategory#3).blogEntries)
post	possibly_updated(new Category(getCategory#3).id)
post	init'ed(new Category(getCategory#3).name)
post	possibly_updated(new Category(getCategory#3). parent)
post	possibly_updated(new Category(getCategory#3). subCategories)
post	init'ed(new Category(getCategory#3).tags)
post	init'ed(new Category(getCategory#3).tagsAsList)
unanalyzed	call on java.util.Collections:unmodifiableList
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSubCategories
unanalyzed	call on getCategory
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:equals
unanalyzed	call on net.sourceforge.pebble.util. I18n:getMessage
unanalyzed	call on java.util.ArrayList
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getLocale
unanalyzed	call on addCategory
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on net.sourceforge.pebble.domain.Category
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.util.List:add
test_vector	create: {0}, {1}
unanalyzed	call on getId
test_vector	id: Addr_Set{null}, Inverse{null}
test_vector	this.rootCategory: Inverse{null}, Addr_Set{null}
unanalyzed	call on setBlog
test_vector	java.lang.String:equals(...)@141: {0}, {1}
unanalyzed	call on isRootCategory
test_vector	java.lang.String:equals(...)@166: {0}, {1}
unanalyzed	call on addSubCategory
test_vector	java.lang.String:indexOf(...)@154: {-2³¹. .-2, 0..2³²-2}, {-1}
test_vector	java.lang.String:startsWith(...)@137: {1}, {0}
test_vector	java.util.Iterator:hasNext(...)@164: {1}, {0}

info method not available -- call on String net.sourceforge.pebble.util. I18n:getMessage(Locale, String)

info method not available -- call on Locale net.sourceforge.pebble.domain. Blog:getLocale()

Prev Msg Next Msg

click for all messages in this file medium

null dereference check might fail: requires parentCategory != null

Prev Msg Next Msg

method	Category getCategory(String)
pre	(soft) init'ed(this.rootCategory)
pre	(soft) this.blog != null
post	init'ed(return_value)
post	init'ed(this.rootCategory)
post	init'ed(new ArrayList(Category#1) num objects)
post	init'ed(new ArrayList(Category#2) num objects)
post	init'ed(new ArrayList(Category#3) num objects)
post	init'ed(new Category(getCategory#2*) num objects)
post	possibly_updated(new Category(getCategory#2*). blog)
post	init'ed(new Category(getCategory#2*).blogEntries)
post	possibly_updated(new Category(getCategory#2*).id)
post	init'ed(new Category(getCategory#2*).name)
post	possibly_updated(new Category(getCategory#2*). parent)
post	possibly_updated(new Category(getCategory#2*). subCategories)
post	init'ed(new Category(getCategory#2*).tags)
post	init'ed(new Category(getCategory#2*).tagsAsList)
post	init'ed(new Category(getCategory#3*) num objects)
post	possibly_updated(new Category(getCategory#3*). blog)
post	init'ed(new Category(getCategory#3*).blogEntries)
post	possibly_updated(new Category(getCategory#3*).id)
post	init'ed(new Category(getCategory#3*).name)
post	possibly_updated(new Category(getCategory#3*). parent)
post	possibly_updated(new Category(getCategory#3*). subCategories)
post	init'ed(new Category(getCategory#3*).tags)
post	init'ed(new Category(getCategory#3*).tagsAsList)
unanalyzed	call on java.util.Collections:unmodifiableList
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getCategory
unanalyzed	call on java.util.List:contains
unanalyzed	call on getSubCategories
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:equals
unanalyzed	call on net.sourceforge.pebble.util. I18n:getMessage
unanalyzed	call on java.util.ArrayList
unanalyzed	call on addCategory
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:length
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getLocale
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on net.sourceforge.pebble.domain.Category
unanalyzed	call on java.util.List:add
unanalyzed	call on getId
unanalyzed	call on setBlog
unanalyzed	call on isRootCategory
unanalyzed	call on addSubCategory

method	Category getRootCategory()
pre	(soft) init'ed(this.rootCategory)
pre	(soft) this.blog != null
post	init'ed(return_value)
post	init'ed(this.rootCategory)
post	init'ed(new ArrayList(Category#1) num objects)
post	init'ed(new ArrayList(Category#2) num objects)
post	init'ed(new ArrayList(Category#3) num objects)
post	init'ed(new Category(getCategory#2) num objects)
post	possibly_updated(new Category(getCategory#2).blog)
post	init'ed(new Category(getCategory#2).blogEntries)
post	possibly_updated(new Category(getCategory#2).id)
post	init'ed(new Category(getCategory#2).name)
post	possibly_updated(new Category(getCategory#2). parent)
post	possibly_updated(new Category(getCategory#2). subCategories)
post	init'ed(new Category(getCategory#2).tags)
post	init'ed(new Category(getCategory#2).tagsAsList)
post	init'ed(new Category(getCategory#3) num objects)
post	possibly_updated(new Category(getCategory#3).blog)
post	init'ed(new Category(getCategory#3).blogEntries)
post	possibly_updated(new Category(getCategory#3).id)
post	init'ed(new Category(getCategory#3).name)
post	possibly_updated(new Category(getCategory#3). parent)
post	possibly_updated(new Category(getCategory#3). subCategories)
post	init'ed(new Category(getCategory#3).tags)
post	init'ed(new Category(getCategory#3).tagsAsList)
unanalyzed	call on java.util.Collections:unmodifiableList
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getCategory
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on getSubCategories
unanalyzed	call on java.lang.String:equals
unanalyzed	call on net.sourceforge.pebble.util. I18n:getMessage
unanalyzed	call on java.util.ArrayList
unanalyzed	call on addCategory
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getLocale
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.util.List:add
unanalyzed	call on net.sourceforge.pebble.domain.Category
unanalyzed	call on getId
unanalyzed	call on setBlog
unanalyzed	call on isRootCategory
unanalyzed	call on addSubCategory

method	List getCategories()
pre	(soft) init'ed(this.rootCategory)
pre	(soft) this.blog != null
post	return_value == &new ArrayList(getCategories#1)
post	init'ed(this.rootCategory)
post	init'ed(new ArrayList(Category#1) num objects)
post	init'ed(new ArrayList(Category#2) num objects)
post	init'ed(new ArrayList(Category#3) num objects)
post	new ArrayList(getCategories#1) num objects == 1
post	init'ed(new Category(getCategory#2) num objects)
post	possibly_updated(new Category(getCategory#2).blog)
post	init'ed(new Category(getCategory#2).blogEntries)
post	possibly_updated(new Category(getCategory#2).id)
post	init'ed(new Category(getCategory#2).name)
post	possibly_updated(new Category(getCategory#2). parent)
post	(soft) init'ed(new Category(getCategory#2). subCategories)
post	init'ed(new Category(getCategory#2).tags)
post	init'ed(new Category(getCategory#2).tagsAsList)
post	init'ed(new Category(getCategory#3) num objects)
post	possibly_updated(new Category(getCategory#3).blog)
post	init'ed(new Category(getCategory#3).blogEntries)
post	possibly_updated(new Category(getCategory#3).id)
post	init'ed(new Category(getCategory#3).name)
post	possibly_updated(new Category(getCategory#3). parent)
post	(soft) init'ed(new Category(getCategory#3). subCategories)
post	init'ed(new Category(getCategory#3).tags)
post	init'ed(new Category(getCategory#3).tagsAsList)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Collections:unmodifiableList
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getCategories
unanalyzed	call on java.util.List:addAll
unanalyzed	call on getCategory
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on getSubCategories
unanalyzed	call on java.lang.String:equals
unanalyzed	call on net.sourceforge.pebble.util. I18n:getMessage
unanalyzed	call on addCategory
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getLocale
unanalyzed	call on net.sourceforge.pebble.domain.Category
unanalyzed	call on getId
unanalyzed	call on setBlog
unanalyzed	call on isRootCategory
unanalyzed	call on addSubCategory

Prev Msg Next Msg

click for all messages in this file medium

precondition failure net/sourceforge/pebble/domain/CategoryBuilder. getCategories: category != null

Prev Msg Next Msg

method	List getCategories(Category)
pre	category != null
pre	init'ed(category.subCategories)
presumption	java.util.Collections:unmodifiableList(...)@230 != null
presumption	java.util.Iterator:next(...)@226 != null
post	return_value == &new ArrayList(getCategories#1)
post	new ArrayList(getCategories#1) num objects == 1
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Collections:unmodifiableList
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getCategories
unanalyzed	call on java.util.List:addAll
test_vector	java.util.Iterator:hasNext(...)@225: {1}, {0}
unanalyzed	call on getSubCategories

	info	method not available	-- call on String net.sourceforge.pebble.util. I18n:getMessage(Locale, String)
	info	method not available	-- call on Locale net.sourceforge.pebble.domain. Blog:getLocale()