Messages

Last Msg First Msg

method	String getId()
pre	init'ed(Param_0.id)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-9
post	return_value == Param_0.id
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setId(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.id)
pre	(soft) pcInheritedFieldCount <= 2³²-9
post	Param_0.id == One-of{old Param_0.id, Param_1}
post	(soft) init'ed(Param_0.id)
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	WeblogCategory getCategory()
pre	init'ed(Param_0.category)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-3
post	return_value == Param_0.category
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setCategory(WeblogCategory)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.category)
pre	(soft) pcInheritedFieldCount <= 2³²-3
post	Param_0.category == One-of{Param_1, old Param_0.category}
post	(soft) init'ed(Param_0.category)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	Weblog getWebsite()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.website)
pre	(soft) pcInheritedFieldCount <= 2³²-22
post	return_value == Param_0.website
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setWebsite(Weblog)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.website)
pre	(soft) pcInheritedFieldCount <= 2³²-22
post	Param_0.website == One-of{Param_1, old Param_0.website}
post	(soft) init'ed(Param_0.website)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	User getCreator()
pre	init'ed(Param_0.creator)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-7
post	return_value == Param_0.creator
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setCreator(User)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.creator)
pre	(soft) pcInheritedFieldCount <= 2³²-7
post	Param_0.creator == One-of{Param_1, old Param_0.creator}
post	(soft) init'ed(Param_0.creator)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	String getTitle()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.title)
pre	(soft) pcInheritedFieldCount <= 2³²-20
post	return_value == Param_0.title
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setTitle(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.title)
pre	(soft) pcInheritedFieldCount <= 2³²-20
post	Param_0.title == One-of{Param_1, old Param_0.title}
post	(soft) init'ed(Param_0.title)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	String getSummary()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.summary)
pre	(soft) pcInheritedFieldCount <= 2³²-17
post	return_value == Param_0.summary
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setSummary(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.summary)
pre	(soft) pcInheritedFieldCount <= 2³²-17
post	Param_0.summary == One-of{Param_1, old Param_0.summary}
post	(soft) init'ed(Param_0.summary)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	String getText()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.text)
pre	(soft) pcInheritedFieldCount <= 2³²-19
post	return_value == Param_0.text
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setText(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.text)
pre	(soft) pcInheritedFieldCount <= 2³²-19
post	Param_0.text == One-of{Param_1, old Param_0.text}
post	(soft) init'ed(Param_0.text)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	String getContentType()
pre	init'ed(Param_0.contentType)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-6
post	return_value == Param_0.contentType
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setContentType(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.contentType)
pre	(soft) pcInheritedFieldCount <= 2³²-6
post	Param_0.contentType == One-of{Param_1, old Param_0.contentType}
post	(soft) init'ed(Param_0.contentType)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	String getContentSrc()
pre	init'ed(Param_0.contentSrc)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-5
post	return_value == Param_0.contentSrc
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setContentSrc(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.contentSrc)
pre	(soft) pcInheritedFieldCount <= 2³²-5
post	Param_0.contentSrc == One-of{Param_1, old Param_0.contentSrc}
post	(soft) init'ed(Param_0.contentSrc)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	String getAnchor()
pre	init'ed(Param_0.anchor)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-2
post	return_value == Param_0.anchor
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setAnchor(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.anchor)
pre	(soft) pcInheritedFieldCount <= 2³²-2
post	Param_0.anchor == One-of{Param_1, old Param_0.anchor}
post	(soft) init'ed(Param_0.anchor)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	Set getEntryAttributes()
pre	init'ed(Param_0.attSet)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-8
post	return_value == Param_0.attSet
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setEntryAttributes(Set)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.attSet)
pre	(soft) pcInheritedFieldCount <= 2³²-8
post	Param_0.attSet == One-of{Param_1, old Param_0.attSet}
post	(soft) init'ed(Param_0.attSet)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	Timestamp getPubTime()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.pubTime)
pre	(soft) pcInheritedFieldCount <= 2³²-14
post	return_value == Param_0.pubTime
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setPubTime(Timestamp)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.pubTime)
pre	(soft) pcInheritedFieldCount <= 2³²-14
post	Param_0.pubTime == One-of{Param_1, old Param_0.pubTime}
post	(soft) init'ed(Param_0.pubTime)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	Timestamp getUpdateTime()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.updateTime)
pre	(soft) pcInheritedFieldCount <= 2³²-21
post	return_value == Param_0.updateTime
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setUpdateTime(Timestamp)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.updateTime)
pre	(soft) pcInheritedFieldCount <= 2³²-21
post	Param_0.updateTime == One-of{Param_1, old Param_0.updateTime}
post	(soft) init'ed(Param_0.updateTime)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	String getStatus()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.status)
pre	(soft) pcInheritedFieldCount <= 2³²-16
post	return_value == Param_0.status
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setStatus(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.status)
pre	(soft) pcInheritedFieldCount <= 2³²-16
post	Param_0.status == One-of{Param_1, old Param_0.status}
post	(soft) init'ed(Param_0.status)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	String getLink()
pre	init'ed(Param_0.link)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-10
post	return_value == Param_0.link
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setLink(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.link)
pre	(soft) pcInheritedFieldCount <= 2³²-10
post	Param_0.link == One-of{Param_1, old Param_0.link}
post	(soft) init'ed(Param_0.link)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	String getPlugins()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.plugins)
pre	(soft) pcInheritedFieldCount <= 2³²-13
post	return_value == Param_0.plugins
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setPlugins(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.plugins)
pre	(soft) pcInheritedFieldCount <= 2³²-13
post	Param_0.plugins == One-of{Param_1, old Param_0.plugins}
post	(soft) init'ed(Param_0.plugins)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	Boolean getAllowComments()
pre	init'ed(Param_0.allowComments)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(pcInheritedFieldCount)
post	return_value == Param_0.allowComments
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setAllowComments(Boolean)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.allowComments)
pre	(soft) init'ed(pcInheritedFieldCount)
post	Param_0.allowComments == One-of{Param_1, old Param_0.allowComments}
post	(soft) init'ed(Param_0.allowComments)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	Integer getCommentDays()
pre	init'ed(Param_0.commentDays)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-4
post	return_value == Param_0.commentDays
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setCommentDays(Integer)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.commentDays)
pre	(soft) pcInheritedFieldCount <= 2³²-4
post	Param_0.commentDays == One-of{Param_1, old Param_0.commentDays}
post	(soft) init'ed(Param_0.commentDays)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	Boolean getRightToLeft()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.rightToLeft)
pre	(soft) pcInheritedFieldCount <= 2³²-15
post	return_value == Param_0.rightToLeft
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setRightToLeft(Boolean)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.rightToLeft)
pre	(soft) pcInheritedFieldCount <= 2³²-15
post	Param_0.rightToLeft == One-of{Param_1, old Param_0.rightToLeft}
post	(soft) init'ed(Param_0.rightToLeft)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	Boolean getPinnedToMain()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.pinnedToMain)
pre	(soft) pcInheritedFieldCount <= 2³²-12
post	return_value == Param_0.pinnedToMain
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setPinnedToMain(Boolean)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.pinnedToMain)
pre	(soft) pcInheritedFieldCount <= 2³²-12
post	Param_0.pinnedToMain == One-of{Param_1, old Param_0.pinnedToMain}
post	(soft) init'ed(Param_0.pinnedToMain)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	String getLocale()
pre	init'ed(Param_0.locale)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-11
post	return_value == Param_0.locale
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setLocale(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.locale)
pre	(soft) pcInheritedFieldCount <= 2³²-11
post	Param_0.locale == One-of{Param_1, old Param_0.locale}
post	(soft) init'ed(Param_0.locale)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	Set getTags()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.tagSet)
pre	(soft) pcInheritedFieldCount <= 2³²-18
post	return_value == Param_0.tagSet
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setTags(Set)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.tagSet)
pre	(soft) pcInheritedFieldCount <= 2³²-18
post	Param_0.addedTags == One-of{&new HashSet(pcsetTags#2*), old Param_0.addedTags}
post	Param_0.removedTags == One-of{&new HashSet(pcsetTags#1*), old Param_0.removedTags}
post	Param_0.tagSet == One-of{Param_1, old Param_0.tagSet}
post	(soft) init'ed(Param_0.tagSet)
post	new HashSet(pcsetTags#1*) num objects <= 1
post	new HashSet(pcsetTags#2*) num objects <= 1
unanalyzed	call on java.util.HashSet
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	int pcGetEnhancementContractVersion()
post	return_value == 2

method	void pcClearFields()
post	Param_0.addedTags == &new HashSet(pcsetTags#2)
post	Param_0.allowComments == null
post	Param_0.anchor == null
post	Param_0.attSet == null
post	Param_0.category == null
post	Param_0.commentDays == null
post	Param_0.contentSrc == null
post	Param_0.contentType == null
post	Param_0.creator == null
post	Param_0.id == null
post	Param_0.link == null
post	Param_0.locale == null
post	Param_0.pinnedToMain == null
post	Param_0.plugins == null
post	Param_0.pubTime == null
post	Param_0.rightToLeft == null
post	Param_0.status == null
post	Param_0.summary == null
post	Param_0.tagSet == null
post	Param_0.text == null
post	Param_0.title == null
post	Param_0.updateTime == null
post	Param_0.website == null
post	Param_0.removedTags == &new HashSet(pcsetTags#1 )
post	new HashSet(pcsetTags#1) num objects == 1
post	new HashSet(pcsetTags#2) num objects == 1
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim

method	PersistenceCapable pcNewInstance(StateManager, Object, bool)
pre	Param_2 != null
post	return_value == &new WeblogEntry(pcNewInstance# 1)
post	new HashSet(WeblogEntry#3) num objects == 1
post	new HashSet(WeblogEntry#4) num objects == 1
post	new HashSet(WeblogEntry#5) num objects == 1
post	new Integer(WeblogEntry#1) num objects == 1
post	new TreeSet(WeblogEntry#2) num objects == 1
post	new WeblogEntry(pcNewInstance#1) num objects == 1
post	new HashSet(pcsetTags#1) num objects <= 1
post	new HashSet(pcsetTags#2) num objects <= 1
post	return_value.addedTags in Addr_Set{&new HashSet(WeblogEntry#5),&new HashSet(pcsetTags# 2)}
post	return_value.allowComments == One-of{java.lang. Boolean.TRUE, null}
post	init'ed(return_value.allowComments)
post	return_value.anchor == null
post	return_value.attSet in Addr_Set{null,&new TreeSet(WeblogEntry#2)}
post	return_value.category == null
post	return_value.commentDays in Addr_Set{null,&new Integer(WeblogEntry#1)}
post	return_value.contentSrc == null
post	return_value.contentType == null
post	return_value.creator == null
post	init'ed(return_value.id)
post	return_value.link == null
post	return_value.locale == null
post	return_value.pcStateManager == Param_1
post	init'ed(return_value.pcStateManager)
post	return_value.pinnedToMain == One-of{java.lang. Boolean.FALSE, null}
post	init'ed(return_value.pinnedToMain)
post	return_value.plugins == null
post	return_value.pubTime == null
post	return_value.removedTags in Addr_Set{&new HashSet(WeblogEntry#4),&new HashSet(pcsetTags# 1)}
post	return_value.rightToLeft == One-of{java.lang. Boolean.FALSE, null}
post	init'ed(return_value.rightToLeft)
post	return_value.status in Addr_Set{null,&"DRAFT"}
post	return_value.summary == null
post	return_value.tagSet in Addr_Set{null,&new HashSet(WeblogEntry#3)}
post	return_value.text == null
post	return_value.title == null
post	return_value.updateTime == null
post	return_value.website == null
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on java.lang.Integer
unanalyzed	call on java.util.TreeSet
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim
unanalyzed	call on org.apache.openjpa.util.StringId:getId
test_vector	Param_3: {0}, {1}

method	PersistenceCapable pcNewInstance(StateManager, bool)
post	return_value == &new WeblogEntry(pcNewInstance# 1)
post	new HashSet(WeblogEntry#3) num objects == 1
post	new HashSet(WeblogEntry#4) num objects == 1
post	new HashSet(WeblogEntry#5) num objects == 1
post	new Integer(WeblogEntry#1) num objects == 1
post	new TreeSet(WeblogEntry#2) num objects == 1
post	new WeblogEntry(pcNewInstance#1) num objects == 1
post	new HashSet(pcsetTags#1) num objects <= 1
post	new HashSet(pcsetTags#2) num objects <= 1
post	return_value.addedTags in Addr_Set{&new HashSet(WeblogEntry#5),&new HashSet(pcsetTags# 2)}
post	return_value.allowComments == One-of{java.lang. Boolean.TRUE, null}
post	init'ed(return_value.allowComments)
post	return_value.anchor == null
post	return_value.attSet in Addr_Set{null,&new TreeSet(WeblogEntry#2)}
post	return_value.category == null
post	return_value.commentDays in Addr_Set{null,&new Integer(WeblogEntry#1)}
post	return_value.contentSrc == null
post	return_value.contentType == null
post	return_value.creator == null
post	init'ed(return_value.id)
post	return_value.link == null
post	return_value.locale == null
post	return_value.pcStateManager == Param_1
post	init'ed(return_value.pcStateManager)
post	return_value.pinnedToMain == One-of{java.lang. Boolean.FALSE, null}
post	init'ed(return_value.pinnedToMain)
post	return_value.plugins == null
post	return_value.pubTime == null
post	return_value.removedTags in Addr_Set{&new HashSet(WeblogEntry#4),&new HashSet(pcsetTags# 1)}
post	return_value.rightToLeft == One-of{java.lang. Boolean.FALSE, null}
post	init'ed(return_value.rightToLeft)
post	return_value.status in Addr_Set{null,&"DRAFT"}
post	return_value.summary == null
post	return_value.tagSet in Addr_Set{null,&new HashSet(WeblogEntry#3)}
post	return_value.text == null
post	return_value.title == null
post	return_value.updateTime == null
post	return_value.website == null
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on java.lang.Integer
unanalyzed	call on java.util.TreeSet
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim
test_vector	Param_2: {0}, {1}

method	int pcGetManagedFieldCount()
post	return_value == 22

method	void pcReplaceField(int)
pre	Param_0.pcStateManager != null
pre	Param_1 - pcInheritedFieldCount in 0..21
pre	init'ed(pcInheritedFieldCount)
post	possibly_updated(Param_0.addedTags)
post	possibly_updated(Param_0.allowComments)
post	possibly_updated(Param_0.anchor)
post	possibly_updated(Param_0.attSet)
post	possibly_updated(Param_0.category)
post	possibly_updated(Param_0.commentDays)
post	possibly_updated(Param_0.contentSrc)
post	possibly_updated(Param_0.contentType)
post	possibly_updated(Param_0.creator)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.link)
post	possibly_updated(Param_0.locale)
post	possibly_updated(Param_0.pinnedToMain)
post	possibly_updated(Param_0.plugins)
post	possibly_updated(Param_0.pubTime)
post	possibly_updated(Param_0.removedTags)
post	possibly_updated(Param_0.rightToLeft)
post	possibly_updated(Param_0.status)
post	possibly_updated(Param_0.summary)
post	possibly_updated(Param_0.tagSet)
post	possibly_updated(Param_0.text)
post	possibly_updated(Param_0.title)
post	possibly_updated(Param_0.updateTime)
post	possibly_updated(Param_0.website)
post	new HashSet(pcsetTags#1) num objects <= 1
post	new HashSet(pcsetTags#2) num objects <= 1
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim
test_vector	Param_1 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {10}, {11}, {12}, {13}, {14}, {15}, {16}, {17}, {18}, {19}, {20}, {21}

method	void pcReplaceFields(int[])
pre	Param_1 != null
pre	Param_1.length <= 2³²-1
pre	(soft) Param_0.pcStateManager != null
pre	(soft) init'ed(Param_1[...])
pre	(soft) init'ed(pcInheritedFieldCount)
post	possibly_updated(Param_0.addedTags)
post	possibly_updated(Param_0.allowComments)
post	possibly_updated(Param_0.anchor)
post	possibly_updated(Param_0.attSet)
post	possibly_updated(Param_0.category)
post	possibly_updated(Param_0.commentDays)
post	possibly_updated(Param_0.contentSrc)
post	possibly_updated(Param_0.contentType)
post	possibly_updated(Param_0.creator)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.link)
post	possibly_updated(Param_0.locale)
post	possibly_updated(Param_0.pinnedToMain)
post	possibly_updated(Param_0.plugins)
post	possibly_updated(Param_0.pubTime)
post	possibly_updated(Param_0.removedTags)
post	possibly_updated(Param_0.rightToLeft)
post	possibly_updated(Param_0.status)
post	possibly_updated(Param_0.summary)
post	possibly_updated(Param_0.tagSet)
post	possibly_updated(Param_0.text)
post	possibly_updated(Param_0.title)
post	possibly_updated(Param_0.updateTime)
post	possibly_updated(Param_0.website)
post	init'ed(new HashSet(pcsetTags#1) num objects)
post	init'ed(new HashSet(pcsetTags#2) num objects)
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim
unanalyzed	call on org.apache.openjpa.enhance.StateManager:rep laceObjectField
unanalyzed	call on org.apache.openjpa.enhance.StateManager:rep laceStringField

method	void pcProvideField(int)
pre	Param_0.pcStateManager != null
pre	Param_1 - pcInheritedFieldCount in 0..21
pre	init'ed(pcInheritedFieldCount)
pre	(soft) init'ed(Param_0.allowComments)
pre	(soft) init'ed(Param_0.anchor)
pre	(soft) init'ed(Param_0.attSet)
pre	(soft) init'ed(Param_0.category)
pre	(soft) init'ed(Param_0.commentDays)
pre	(soft) init'ed(Param_0.contentSrc)
pre	(soft) init'ed(Param_0.contentType)
pre	(soft) init'ed(Param_0.creator)
pre	(soft) init'ed(Param_0.id)
pre	(soft) init'ed(Param_0.link)
pre	(soft) init'ed(Param_0.locale)
pre	(soft) init'ed(Param_0.pinnedToMain)
pre	(soft) init'ed(Param_0.plugins)
pre	(soft) init'ed(Param_0.pubTime)
pre	(soft) init'ed(Param_0.rightToLeft)
pre	(soft) init'ed(Param_0.status)
pre	(soft) init'ed(Param_0.summary)
pre	(soft) init'ed(Param_0.tagSet)
pre	(soft) init'ed(Param_0.text)
pre	(soft) init'ed(Param_0.title)
pre	(soft) init'ed(Param_0.updateTime)
pre	(soft) init'ed(Param_0.website)
test_vector	Param_1 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {10}, {11}, {12}, {13}, {14}, {15}, {16}, {17}, {18}, {19}, {20}, {21}

method	void pcProvideFields(int[])
pre	Param_1 != null
pre	Param_1.length <= 2³²-1
pre	(soft) init'ed(Param_0.allowComments)
pre	(soft) init'ed(Param_0.anchor)
pre	(soft) init'ed(Param_0.attSet)
pre	(soft) init'ed(Param_0.category)
pre	(soft) init'ed(Param_0.commentDays)
pre	(soft) init'ed(Param_0.contentSrc)
pre	(soft) init'ed(Param_0.contentType)
pre	(soft) init'ed(Param_0.creator)
pre	(soft) init'ed(Param_0.id)
pre	(soft) init'ed(Param_0.link)
pre	(soft) init'ed(Param_0.locale)
pre	(soft) Param_0.pcStateManager != null
pre	(soft) init'ed(Param_0.pinnedToMain)
pre	(soft) init'ed(Param_0.plugins)
pre	(soft) init'ed(Param_0.pubTime)
pre	(soft) init'ed(Param_0.rightToLeft)
pre	(soft) init'ed(Param_0.status)
pre	(soft) init'ed(Param_0.summary)
pre	(soft) init'ed(Param_0.tagSet)
pre	(soft) init'ed(Param_0.text)
pre	(soft) init'ed(Param_0.title)
pre	(soft) init'ed(Param_0.updateTime)
pre	(soft) init'ed(Param_0.website)
pre	(soft) init'ed(Param_1[...])
pre	(soft) init'ed(pcInheritedFieldCount)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:pro videdObjectField
unanalyzed	call on org.apache.openjpa.enhance.StateManager:pro videdStringField

method	void pcCopyField(WeblogEntry, int)
pre	Param_1 != null
pre	Param_2 - pcInheritedFieldCount in 0..21
pre	init'ed(pcInheritedFieldCount)
pre	(soft) init'ed(Param_1.allowComments)
pre	(soft) init'ed(Param_1.anchor)
pre	(soft) init'ed(Param_1.attSet)
pre	(soft) init'ed(Param_1.category)
pre	(soft) init'ed(Param_1.commentDays)
pre	(soft) init'ed(Param_1.contentSrc)
pre	(soft) init'ed(Param_1.contentType)
pre	(soft) init'ed(Param_1.creator)
pre	(soft) init'ed(Param_1.id)
pre	(soft) init'ed(Param_1.link)
pre	(soft) init'ed(Param_1.locale)
pre	(soft) init'ed(Param_1.pinnedToMain)
pre	(soft) init'ed(Param_1.plugins)
pre	(soft) init'ed(Param_1.pubTime)
pre	(soft) init'ed(Param_1.rightToLeft)
pre	(soft) init'ed(Param_1.status)
pre	(soft) init'ed(Param_1.summary)
pre	(soft) init'ed(Param_1.tagSet)
pre	(soft) init'ed(Param_1.text)
pre	(soft) init'ed(Param_1.title)
pre	(soft) init'ed(Param_1.updateTime)
pre	(soft) init'ed(Param_1.website)
post	possibly_updated(Param_0.addedTags)
post	possibly_updated(Param_0.allowComments)
post	possibly_updated(Param_0.anchor)
post	possibly_updated(Param_0.attSet)
post	possibly_updated(Param_0.category)
post	possibly_updated(Param_0.commentDays)
post	possibly_updated(Param_0.contentSrc)
post	possibly_updated(Param_0.contentType)
post	possibly_updated(Param_0.creator)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.link)
post	possibly_updated(Param_0.locale)
post	possibly_updated(Param_0.pinnedToMain)
post	possibly_updated(Param_0.plugins)
post	possibly_updated(Param_0.pubTime)
post	possibly_updated(Param_0.removedTags)
post	possibly_updated(Param_0.rightToLeft)
post	possibly_updated(Param_0.status)
post	possibly_updated(Param_0.summary)
post	possibly_updated(Param_0.tagSet)
post	possibly_updated(Param_0.text)
post	possibly_updated(Param_0.title)
post	possibly_updated(Param_0.updateTime)
post	possibly_updated(Param_0.website)
post	new HashSet(pcsetTags#1) num objects <= 1
post	new HashSet(pcsetTags#2) num objects <= 1
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim
test_vector	Param_2 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {10}, {11}, {12}, {13}, {14}, {15}, {16}, {17}, {18}, {19}, {20}, {21}

method	void pcCopyFields(Object, int[])
pre	Param_0.pcStateManager != null
pre	Param_0.pcStateManager == Param_1.pcStateManager
pre	Param_1 != null
pre	Param_1.pcStateManager != null
pre	Param_2 != null
pre	Param_2.length <= 2³²-1
pre	(soft) init'ed(Param_1.allowComments)
pre	(soft) init'ed(Param_1.anchor)
pre	(soft) init'ed(Param_1.attSet)
pre	(soft) init'ed(Param_1.category)
pre	(soft) init'ed(Param_1.commentDays)
pre	(soft) init'ed(Param_1.contentSrc)
pre	(soft) init'ed(Param_1.contentType)
pre	(soft) init'ed(Param_1.creator)
pre	(soft) init'ed(Param_1.id)
pre	(soft) init'ed(Param_1.link)
pre	(soft) init'ed(Param_1.locale)
pre	(soft) init'ed(Param_1.pinnedToMain)
pre	(soft) init'ed(Param_1.plugins)
pre	(soft) init'ed(Param_1.pubTime)
pre	(soft) init'ed(Param_1.rightToLeft)
pre	(soft) init'ed(Param_1.status)
pre	(soft) init'ed(Param_1.summary)
pre	(soft) init'ed(Param_1.tagSet)
pre	(soft) init'ed(Param_1.text)
pre	(soft) init'ed(Param_1.title)
pre	(soft) init'ed(Param_1.updateTime)
pre	(soft) init'ed(Param_1.website)
pre	(soft) init'ed(Param_2[...])
pre	(soft) init'ed(pcInheritedFieldCount)
post	possibly_updated(Param_0.addedTags)
post	possibly_updated(Param_0.allowComments)
post	possibly_updated(Param_0.anchor)
post	possibly_updated(Param_0.attSet)
post	possibly_updated(Param_0.category)
post	possibly_updated(Param_0.commentDays)
post	possibly_updated(Param_0.contentSrc)
post	possibly_updated(Param_0.contentType)
post	possibly_updated(Param_0.creator)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.link)
post	possibly_updated(Param_0.locale)
post	possibly_updated(Param_0.pinnedToMain)
post	possibly_updated(Param_0.plugins)
post	possibly_updated(Param_0.pubTime)
post	possibly_updated(Param_0.removedTags)
post	possibly_updated(Param_0.rightToLeft)
post	possibly_updated(Param_0.status)
post	possibly_updated(Param_0.summary)
post	possibly_updated(Param_0.tagSet)
post	possibly_updated(Param_0.text)
post	possibly_updated(Param_0.title)
post	possibly_updated(Param_0.updateTime)
post	possibly_updated(Param_0.website)
post	init'ed(new HashSet(pcsetTags#1) num objects)
post	init'ed(new HashSet(pcsetTags#2) num objects)
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim

method	Object pcGetGenericContext()
pre	init'ed(Param_0.pcStateManager)
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	Object pcFetchObjectId()
pre	init'ed(Param_0.pcStateManager)
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	bool pcIsDeleted()
pre	init'ed(Param_0.pcStateManager)
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	bool pcIsDirty()
pre	init'ed(Param_0.pcStateManager)
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	bool pcIsNew()
pre	init'ed(Param_0.pcStateManager)
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	bool pcIsPersistent()
pre	init'ed(Param_0.pcStateManager)
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	bool pcIsTransactional()
pre	init'ed(Param_0.pcStateManager)
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	bool pcSerializing()
pre	init'ed(Param_0.pcStateManager)
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void pcDirty(String)
pre	init'ed(Param_0.pcStateManager)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	StateManager pcGetStateManager()
pre	init'ed(Param_0.pcStateManager)
post	return_value == Param_0.pcStateManager
post	init'ed(return_value)

method	Object pcGetVersion()
pre	init'ed(Param_0.pcStateManager)
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void pcReplaceStateManager(StateManager)
pre	init'ed(Param_0.pcStateManager)
post	init'ed(Param_0.pcStateManager)
test_vector	Param_0.pcStateManager: Addr_Set{null}, Inverse{null}

method

void pcCopyKeyFieldsToObjectId(FieldSupplier, Object)

method

void pcCopyKeyFieldsToObjectId(Object)

method	void pcCopyKeyFieldsFromObjectId(FieldConsumer, Object)
pre	Param_1 != null
pre	Param_2 != null
pre	pcInheritedFieldCount <= 2³²-9

method	void pcCopyKeyFieldsFromObjectId(Object)
pre	Param_1 != null
post	possibly_updated(Param_0.id)
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:trim

method	Object pcNewObjectIdInstance(Object)
post	return_value == &new StringId(pcNewObjectIdInst ance#1)
post	new StringId(pcNewObjectIdInstance#1) num objects == 1
unanalyzed	call on java.lang.Class:forName
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.Throwable:getMessage
unanalyzed	call on java.lang.NoClassDefFoundError

method	Object pcNewObjectIdInstance()
pre	init'ed(Param_0.id)
post	return_value == &new StringId(pcNewObjectIdInst ance#1)
post	new StringId(pcNewObjectIdInstance#1) num objects == 1
unanalyzed	call on java.lang.Class:forName
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.Throwable:getMessage
unanalyzed	call on java.lang.NoClassDefFoundError

method	Boolean pcIsDetached()
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.pcDetachedState)
presumption	init'ed(java.lang.Boolean.FALSE)
presumption	init'ed(java.lang.Boolean.TRUE)
presumption	init'ed(org.apache.openjpa.enhance.PersistenceCapab le.DESERIALIZED)
post	return_value == One-of{java.lang.Boolean.TRUE, java.lang.Boolean.FALSE, null}
post	(soft) init'ed(return_value)
test_vector	Param_0.pcDetachedState: Addr_Set{null}, Inverse{null}
test_vector	Param_0.pcStateManager: Addr_Set{null}, Inverse{null}
test_vector	org.apache.openjpa.enhance.StateManager:isDetached( ...): {0}, {1}

method	Object pcGetDetachedState()
pre	init'ed(Param_0.pcDetachedState)
post	return_value == Param_0.pcDetachedState
post	init'ed(return_value)

method	void pcSetDetachedState(Object)
post	Param_0.pcDetachedState == Param_1
post	init'ed(Param_0.pcDetachedState)

method	void writeObject(ObjectOutputStream)
pre	init'ed(Param_0.pcStateManager)
pre	Param_1 != null
post	Param_0.pcDetachedState == One-of{old Param_0.pcDetachedState, null}
unanalyzed	call on org.apache.openjpa.enhance.StateManager:ser ializing

method	void readObject(ObjectInputStream)
pre	Param_1 != null
presumption	init'ed(org.apache.openjpa.enhance.PersistenceCapab le.DESERIALIZED)
post	Param_0.pcDetachedState == org.apache.openjpa. enhance.PersistenceCapable.DESERIALIZED
post	(soft) init'ed(Param_0.pcDetachedState)

method	org.apache.roller.weblogger.pojos.WeblogEntry__ static_init
presumption	org.apache.commons.logging.LogFactory:getFactory(.. .)@66 != null
post	init'ed(mLogger)
post	pcFieldFlags == &new byte[](WeblogEntry__ static_init#3)
post	pcFieldNames == &new String[](WeblogEntry__ static_init#1)
post	pcFieldTypes == &new Class[](WeblogEntry__ static_init#2)
post	new Class[](WeblogEntry__static_init#2) num objects == 1
post	new String[](WeblogEntry__static_init#1) num objects == 1
post	new byte[](WeblogEntry__static_init#3) num objects == 1
post	pcFieldTypes.length == 22
post	pcFieldNames.length == 22
post	pcFieldFlags.length == 22
post	pcFieldNames[...] in Addr_Set{&"allowComments ",&"anchor",&"category",&"commentDays", &"contentSrc",&"contentType", &"creator",&"entryAttributes",&"id", &"link",&"locale",&"pinnedToMain", &"plugins"...
post	pcFieldFlags[...] in {5, 26}
unanalyzed	call on java.lang.Class:forName
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.Throwable:getMessage
unanalyzed	call on java.lang.NoClassDefFoundError
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on java.lang.Integer
unanalyzed	call on java.util.TreeSet
unanalyzed	call on java.util.HashSet

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

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

info method not available -- call on void org.apache.openjpa.enhance. PCRegistry:register(Class, String[], Class[], byte[], Class, String, PersistenceCapable)

info method not available -- call on String org.apache.roller.util. UUIDGenerator:generateUUID()

method	void org.apache.roller.weblogger.pojos. WeblogEntry()
presumption	init'ed(java.lang.Boolean.FALSE)
presumption	init'ed(java.lang.Boolean.TRUE)
post	this.addedTags == &new HashSet(WeblogEntry#5)
post	this.allowComments == java.lang.Boolean.TRUE
post	(soft) init'ed(this.allowComments)
post	this.anchor == null
post	this.category == null
post	this.contentSrc == null
post	this.contentType == null
post	this.creator == null
post	this.link == null
post	this.locale == null
post	this.plugins == null
post	this.pubTime == null
post	this.summary == null
post	this.text == null
post	this.title == null
post	this.updateTime == null
post	this.website == null
post	this.attSet == &new TreeSet(WeblogEntry#2)
post	this.commentDays == &new Integer(WeblogEntry#1)
post	init'ed(this.id)
post	this.pinnedToMain == java.lang.Boolean.FALSE
post	(soft) init'ed(this.pinnedToMain)
post	this.rightToLeft == this.pinnedToMain
post	this.removedTags == &new HashSet(WeblogEntry#4)
post	this.status == &"DRAFT"
post	this.tagSet == &new HashSet(WeblogEntry#3)
post	new HashSet(WeblogEntry#3) num objects == 1
post	new HashSet(WeblogEntry#4) num objects == 1
post	new HashSet(WeblogEntry#5) num objects == 1
post	new Integer(WeblogEntry#1) num objects == 1
post	new TreeSet(WeblogEntry#2) num objects == 1

method	void org.apache.roller.weblogger.pojos. WeblogEntry(String, WeblogCategory, Weblog, User, String, String, String, String, Timestamp, Timestamp, String)
presumption	init'ed(java.lang.Boolean.FALSE)
presumption	init'ed(java.lang.Boolean.TRUE)
post	this.addedTags == &new HashSet(WeblogEntry#5)
post	this.allowComments == java.lang.Boolean.TRUE
post	(soft) init'ed(this.allowComments)
post	this.anchor == anchor
post	init'ed(this.anchor)
post	this.attSet == &new TreeSet(WeblogEntry#2)
post	this.category == category
post	init'ed(this.category)
post	this.commentDays == &new Integer(WeblogEntry#1)
post	this.contentSrc == null
post	this.contentType == null
post	this.locale == null
post	this.plugins == null
post	this.summary == null
post	this.creator == creator
post	init'ed(this.creator)
post	init'ed(this.id)
post	this.link == link
post	init'ed(this.link)
post	this.pinnedToMain == java.lang.Boolean.FALSE
post	(soft) init'ed(this.pinnedToMain)
post	this.rightToLeft == this.pinnedToMain
post	this.pubTime == pubTime
post	init'ed(this.pubTime)
post	this.removedTags == &new HashSet(WeblogEntry#4)
post	this.status == status
post	init'ed(this.status)
post	this.tagSet == &new HashSet(WeblogEntry#3)
post	this.text == text
post	init'ed(this.text)
post	this.title == title
post	init'ed(this.title)
post	this.updateTime == updateTime
post	init'ed(this.updateTime)
post	this.website == website
post	init'ed(this.website)
post	new HashSet(WeblogEntry#3) num objects == 1
post	new HashSet(WeblogEntry#4) num objects == 1
post	new HashSet(WeblogEntry#5) num objects == 1
post	new Integer(WeblogEntry#1) num objects == 1
post	new TreeSet(WeblogEntry#2) num objects == 1

method	void org.apache.roller.weblogger.pojos. WeblogEntry(WeblogEntry)
pre	otherData != null
pre	init'ed(otherData.allowComments)
pre	init'ed(otherData.anchor)
pre	init'ed(otherData.category)
pre	init'ed(otherData.commentDays)
pre	init'ed(otherData.creator)
pre	init'ed(otherData.id)
pre	init'ed(otherData.link)
pre	init'ed(otherData.locale)
pre	init'ed(otherData.pcStateManager)
pre	init'ed(otherData.pinnedToMain)
pre	init'ed(otherData.plugins)
pre	init'ed(otherData.pubTime)
pre	init'ed(otherData.rightToLeft)
pre	init'ed(otherData.status)
pre	init'ed(otherData.text)
pre	init'ed(otherData.title)
pre	init'ed(otherData.updateTime)
pre	init'ed(otherData.website)
pre	(soft) pcInheritedFieldCount <= 2³²-22
presumption	init'ed(java.lang.Boolean.FALSE)
presumption	init'ed(java.lang.Boolean.TRUE)
post	this.addedTags == &new HashSet(WeblogEntry#5)
post	this.allowComments == otherData.allowComments
post	init'ed(this.allowComments)
post	this.anchor == otherData.anchor
post	init'ed(this.anchor)
post	this.attSet == &new TreeSet(WeblogEntry#2)
post	this.category == otherData.category
post	init'ed(this.category)
post	this.commentDays == otherData.commentDays
post	init'ed(this.commentDays)
post	init'ed(this.contentSrc)
post	init'ed(this.contentType)
post	this.creator == otherData.creator
post	init'ed(this.creator)
post	this.id == otherData.id
post	init'ed(this.id)
post	this.link == otherData.link
post	init'ed(this.link)
post	this.locale == otherData.locale
post	init'ed(this.locale)
post	this.pinnedToMain == otherData.pinnedToMain
post	init'ed(this.pinnedToMain)
post	this.plugins == otherData.plugins
post	init'ed(this.plugins)
post	this.pubTime == otherData.pubTime
post	init'ed(this.pubTime)
post	this.removedTags == &new HashSet(WeblogEntry#4)
post	this.rightToLeft == otherData.rightToLeft
post	init'ed(this.rightToLeft)
post	this.status == otherData.status
post	init'ed(this.status)
post	init'ed(this.summary)
post	this.tagSet == &new HashSet(WeblogEntry#3)
post	this.text == otherData.text
post	init'ed(this.text)
post	this.title == otherData.title
post	init'ed(this.title)
post	this.updateTime == otherData.updateTime
post	init'ed(this.updateTime)
post	this.website == otherData.website
post	init'ed(this.website)
post	new HashSet(WeblogEntry#3) num objects == 1
post	new HashSet(WeblogEntry#4) num objects == 1
post	new HashSet(WeblogEntry#5) num objects == 1
post	new Integer(WeblogEntry#1) num objects == 1
post	new TreeSet(WeblogEntry#2) num objects == 1
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

method	void setData(WeblogEntry)
pre	other != null
pre	init'ed(other.allowComments)
pre	init'ed(other.anchor)
pre	init'ed(other.category)
pre	init'ed(other.commentDays)
pre	init'ed(other.creator)
pre	init'ed(other.id)
pre	init'ed(other.link)
pre	init'ed(other.locale)
pre	init'ed(other.pcStateManager)
pre	init'ed(other.pinnedToMain)
pre	init'ed(other.plugins)
pre	init'ed(other.pubTime)
pre	init'ed(other.rightToLeft)
pre	init'ed(other.status)
pre	init'ed(other.text)
pre	init'ed(other.title)
pre	init'ed(other.updateTime)
pre	init'ed(other.website)
pre	(soft) pcInheritedFieldCount <= 2³²-22
post	this.allowComments == other.allowComments
post	init'ed(this.allowComments)
post	this.anchor == other.anchor
post	init'ed(this.anchor)
post	this.category == other.category
post	init'ed(this.category)
post	this.commentDays == other.commentDays
post	init'ed(this.commentDays)
post	this.creator == other.creator
post	init'ed(this.creator)
post	this.id == other.id
post	init'ed(this.id)
post	this.link == other.link
post	init'ed(this.link)
post	this.locale == other.locale
post	init'ed(this.locale)
post	this.pinnedToMain == other.pinnedToMain
post	init'ed(this.pinnedToMain)
post	this.plugins == other.plugins
post	init'ed(this.plugins)
post	this.pubTime == other.pubTime
post	init'ed(this.pubTime)
post	this.rightToLeft == other.rightToLeft
post	init'ed(this.rightToLeft)
post	this.status == other.status
post	init'ed(this.status)
post	this.text == other.text
post	init'ed(this.text)
post	this.title == other.title
post	init'ed(this.title)
post	this.updateTime == other.updateTime
post	init'ed(this.updateTime)
post	this.website == other.website
post	init'ed(this.website)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

method	String toString()
pre	init'ed(this.anchor)
pre	init'ed(this.id)
pre	init'ed(this.pubTime)
pre	init'ed(this.title)
post	java.lang.StringBuffer:toString(...)._tainted == this.title._tainted \| this.id._tainted \| this.anchor._tainted
post	init'ed(java.lang.StringBuffer:toString(...)._ tainted)
post	return_value == &java.lang.StringBuffer:toStrin g(...)

method	bool equals(Object)
pre	(soft) init'ed(other.anchor)
pre	(soft) init'ed(other.pcStateManager)
pre	(soft) init'ed(other.website)
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) init'ed(this.anchor)
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) init'ed(this.website)
presumption	org.apache.commons.lang.builder.EqualsBuilder:appen d(...)@184 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	other == this: {0}, {1}

info method not available -- call on void org.apache.commons.lang.builder. EqualsBuilder()

info method not available -- call on EqualsBuilder org.apache.commons.lang. builder.EqualsBuilder:append(Object, Object)

info method not available -- call on bool org.apache.commons.lang.builder. EqualsBuilder:isEquals()

method	int hashCode()
pre	init'ed(this.anchor)
pre	init'ed(this.pcStateManager)
pre	init'ed(this.website)
pre	(soft) pcInheritedFieldCount <= 2³²-22
presumption	org.apache.commons.lang.builder.HashCodeBuilder:app end(...)@191 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

info method not available -- call on void org.apache.commons.lang.builder. HashCodeBuilder()

info method not available -- call on HashCodeBuilder org.apache.commons.lang. builder.HashCodeBuilder:append(Object)

info method not available -- call on int org.apache.commons.lang.builder. HashCodeBuilder:toHashCode()

method	String pcgetId()
pre	init'ed(this.id)
post	return_value == this.id
post	init'ed(return_value)

method	void pcsetId(String)
post	this.id == One-of{old this.id, Param_1}
test_vector	Param_1: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:length(...)@211: {1.. 2³²-1}, {0}

method	WeblogCategory pcgetCategory()
pre	init'ed(this.category)
post	return_value == this.category
post	init'ed(return_value)

method	void pcsetCategory(WeblogCategory)
post	this.category == Param_1
post	init'ed(this.category)

method	List getCategories()
pre	init'ed(this.category)
pre	init'ed(this.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-3
post	return_value == &new ArrayList(getCategories#1)
post	new ArrayList(getCategories#1) num objects == 1
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

method

void setCategories(List)

method	Weblog pcgetWebsite()
pre	init'ed(this.website)
post	return_value == this.website
post	init'ed(return_value)

method	void pcsetWebsite(Weblog)
post	this.website == Param_1
post	init'ed(this.website)

method	User pcgetCreator()
pre	init'ed(this.creator)
post	return_value == this.creator
post	init'ed(return_value)

method	void pcsetCreator(User)
post	this.creator == Param_1
post	init'ed(this.creator)

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

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

method	String pcgetSummary()
pre	init'ed(this.summary)
post	return_value == this.summary
post	init'ed(return_value)

method	void pcsetSummary(String)
post	this.summary == Param_1
post	init'ed(this.summary)

method	String pcgetText()
pre	init'ed(this.text)
post	return_value == this.text
post	init'ed(return_value)

method	void pcsetText(String)
post	this.text == Param_1
post	init'ed(this.text)

method	String pcgetContentType()
pre	init'ed(this.contentType)
post	return_value == this.contentType
post	init'ed(return_value)

method	void pcsetContentType(String)
post	this.contentType == Param_1
post	init'ed(this.contentType)

method	String pcgetContentSrc()
pre	init'ed(this.contentSrc)
post	return_value == this.contentSrc
post	init'ed(return_value)

method	void pcsetContentSrc(String)
post	this.contentSrc == Param_1
post	init'ed(this.contentSrc)

method	String pcgetAnchor()
pre	init'ed(this.anchor)
post	return_value == this.anchor
post	init'ed(return_value)

method	void pcsetAnchor(String)
post	this.anchor == Param_1
post	init'ed(this.anchor)

method	Set pcgetEntryAttributes()
pre	init'ed(this.attSet)
post	return_value == this.attSet
post	init'ed(return_value)

method	void pcsetEntryAttributes(Set)
post	this.attSet == Param_1
post	init'ed(this.attSet)

method	String findEntryAttribute(String)
pre	init'ed(this.attSet)
pre	init'ed(this.pcStateManager)
pre	(soft) name != null
pre	(soft) org/apache/roller/weblogger/pojos/WeblogEntr yAttribute.pcInheritedFieldCount <= 2³²-4
pre	(soft) pcInheritedFieldCount <= 2³²-8
presumption	java.util.Iterator:next(...)@401 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	this.attSet: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:equals(...)@402: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@400: {0}, {1}

method	void putEntryAttribute(String, String)
pre	this.attSet != null
pre	init'ed(this.pcStateManager)
pre	(soft) name != null
pre	(soft) org/apache/roller/weblogger/pojos/WeblogEntr yAttribute.pcInheritedFieldCount <= 2³²-4
pre	(soft) pcInheritedFieldCount <= 2³²-8
presumption	java.util.Iterator:next(...)@411 != null
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingObjectField
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingStringField
test_vector	java.lang.String:equals(...)@412: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@410: {0}, {1}

method	Timestamp pcgetPubTime()
pre	init'ed(this.pubTime)
post	return_value == this.pubTime
post	init'ed(return_value)

method	void pcsetPubTime(Timestamp)
post	this.pubTime == Param_1
post	init'ed(this.pubTime)

method	Timestamp pcgetUpdateTime()
pre	init'ed(this.updateTime)
post	return_value == this.updateTime
post	init'ed(return_value)

method	void pcsetUpdateTime(Timestamp)
post	this.updateTime == Param_1
post	init'ed(this.updateTime)

method	String pcgetStatus()
pre	init'ed(this.status)
post	return_value == this.status
post	init'ed(return_value)

method	void pcsetStatus(String)
post	this.status == Param_1
post	init'ed(this.status)

method	String pcgetLink()
pre	init'ed(this.link)
post	return_value == this.link
post	init'ed(return_value)

method	void pcsetLink(String)
post	this.link == Param_1
post	init'ed(this.link)

method	String pcgetPlugins()
pre	init'ed(this.plugins)
post	return_value == this.plugins
post	init'ed(return_value)

method	void pcsetPlugins(String)
post	this.plugins == Param_1
post	init'ed(this.plugins)

method	Boolean pcgetAllowComments()
pre	init'ed(this.allowComments)
post	return_value == this.allowComments
post	init'ed(return_value)

method	void pcsetAllowComments(Boolean)
post	this.allowComments == Param_1
post	init'ed(this.allowComments)

method	Integer pcgetCommentDays()
pre	init'ed(this.commentDays)
post	return_value == this.commentDays
post	init'ed(return_value)

method	void pcsetCommentDays(Integer)
post	this.commentDays == Param_1
post	init'ed(this.commentDays)

method	Boolean pcgetRightToLeft()
pre	init'ed(this.rightToLeft)
post	return_value == this.rightToLeft
post	init'ed(return_value)

method	void pcsetRightToLeft(Boolean)
post	this.rightToLeft == Param_1
post	init'ed(this.rightToLeft)

method	Boolean pcgetPinnedToMain()
pre	init'ed(this.pinnedToMain)
post	return_value == this.pinnedToMain
post	init'ed(return_value)

method	void pcsetPinnedToMain(Boolean)
post	this.pinnedToMain == Param_1
post	init'ed(this.pinnedToMain)

method	String pcgetLocale()
pre	init'ed(this.locale)
post	return_value == this.locale
post	init'ed(return_value)

method	void pcsetLocale(String)
post	this.locale == Param_1
post	init'ed(this.locale)

method	Set pcgetTags()
pre	init'ed(this.tagSet)
post	return_value == this.tagSet
post	init'ed(return_value)

method	void pcsetTags(Set)
post	this.addedTags == &new HashSet(pcsetTags#2)
post	this.removedTags == &new HashSet(pcsetTags#1)
post	this.tagSet == Param_1
post	init'ed(this.tagSet)
post	new HashSet(pcsetTags#1) num objects == 1
post	new HashSet(pcsetTags#2) num objects == 1

method	void addTag(String)
pre	init'ed(this.pcStateManager)
pre	init'ed(this.website)
pre	(soft) org/apache/roller/weblogger/pojos/WeblogEntr yTag.pcInheritedFieldCount <= 2³²-6
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) this.addedTags != null
pre	(soft) init'ed(this.creator)
pre	(soft) this.tagSet != null
pre	(soft) init'ed(this.updateTime)
presumption	java.util.Iterator:next(...)@653 != null
presumption	org.apache.roller.weblogger.util.Utilities:normaliz eTag(...)@648 != null
presumption	tag.name@653 != null
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingStringField
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingObjectField
test_vector	this.website: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:equals(...)@654: {0}, {1}
test_vector	java.lang.String:length(...)@649: {1.. 2³²-1}, {0}
test_vector	java.util.Iterator:hasNext(...)@652: {0}, {1}

info method not available -- call on Locale getLocaleInstance()

info method not available -- call on String org.apache.roller.weblogger.util. Utilities:normalizeTag(String, Locale)

method	void onRemoveTag(String)
pre	this.removedTags != null

method	Set getAddedTags()
pre	init'ed(this.addedTags)
post	return_value == this.addedTags
post	init'ed(return_value)

method	Set getRemovedTags()
pre	init'ed(this.removedTags)
post	return_value == this.removedTags
post	init'ed(return_value)

method	void updateTags(List)
pre	(soft) org/apache/roller/weblogger/pojos/WeblogEntr yTag.pcInheritedFieldCount <= 2³²-6
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) this.addedTags != null
pre	(soft) init'ed(this.creator)
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) this.tagSet != null
pre	(soft) init'ed(this.updateTime)
pre	(soft) init'ed(this.website)
presumption	java.util.Iterator:next(...)@698 != null
presumption	org.apache.roller.weblogger.business. Weblogger:getWeblogManager(...)@706 != null
presumption	org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@706 != null
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.Set:add
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on getLocaleInstance
unanalyzed	call on java.util.Locale:getDefault
unanalyzed	call on org.apache.roller.weblogger.util. Utilities:normalizeTag
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingStringField
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingObjectField
test_vector	tags: Inverse{null}, Addr_Set{null}
test_vector	this.website: Addr_Set{null}, Inverse{null}
test_vector	java.util.HashSet:contains(...)@699: {1}, {0}
test_vector	java.util.Iterator:hasNext(...)@689: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@697: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@707: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@711: {0}, {1}

info method not available -- call on Locale getLocaleInstance()

info method not available -- call on String org.apache.roller.weblogger.util. Utilities:normalizeTag(String, Locale)

info method not available -- call on void org.apache.roller.weblogger. business.WeblogManager:removeWeblogEntryTag(String, WeblogEntry)

method	String getTagsAsString()
pre	init'ed(this.pcStateManager)
pre	this.tagSet != null
pre	(soft) org/apache/roller/weblogger/pojos/WeblogEntr yTag.pcInheritedFieldCount <= 2³²-2
pre	(soft) pcInheritedFieldCount <= 2³²-18
presumption	java.lang.StringBuffer:length(...)@725 >= -2³¹+1
presumption	java.util.Iterator:next(...)@722 != null
post	java.lang.StringBuffer:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuffer:toStrin g(...)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	java.lang.StringBuffer:length(...)@724: {-2³¹..0}, {1..2³²-1}
test_vector	java.util.Iterator:hasNext(...)@721: {0}, {1}

method	void setTagsAsString(String)
pre	(soft) org/apache/roller/weblogger/pojos/WeblogEntr yTag.pcInheritedFieldCount <= 2³²-6
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) this.addedTags != null
pre	(soft) init'ed(this.creator)
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) this.tagSet != null
pre	(soft) init'ed(this.updateTime)
pre	(soft) init'ed(this.website)
unanalyzed	call on java.util.HashSet
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.Set:add
unanalyzed	call on org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getWeblogManager
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on getLocaleInstance
unanalyzed	call on java.util.Locale:getDefault
unanalyzed	call on org.apache.roller.weblogger.util. Utilities:normalizeTag
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingStringField
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingObjectField
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.HashSet:add
unanalyzed	call on java.util.HashSet:contains
unanalyzed	call on java.util.HashSet:remove
unanalyzed	call on java.util.HashSet:iterator
unanalyzed	call on org.apache.roller.weblogger.business. WeblogManager:removeWeblogEntryTag
test_vector	tags: Inverse{null}, Addr_Set{null}

info method not available -- call on List org.apache.roller.weblogger.util. Utilities:splitStringAsTags(String)

method	bool getCommentsStillAllowed()
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) init'ed(this.allowComments)
pre	(soft) init'ed(this.commentDays)
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) init'ed(this.pubTime)
pre	(soft) init'ed(this.updateTime)
pre	(soft) this.website != null
presumption	getAllowComments(...)@753 != null
presumption	java.util.Calendar:getInstance(...)@770 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	this.allowComments: Addr_Set{null}, Inverse{null}
test_vector	this.commentDays: Addr_Set{null}, Inverse{null}
test_vector	this.pubTime: Inverse{null}, Addr_Set{null}
test_vector	getAllowComments(...)@753: Addr_Set{null}, Inverse{null}
test_vector	java.lang.Boolean:booleanValue(...)@753: {1}, {0}
test_vector	java.lang.Boolean:booleanValue(...)@756: {1}, {0}
test_vector	java.lang.Integer:intValue(...)@760: {-2³¹..-1, 1..2³²-1}, {0}
test_vector	java.util.Date:before(...)@776: {0}, {1}
test_vector	org.apache.roller.weblogger.config.WebloggerRuntime Config:getBooleanProperty(...)@750: {1}, {0}

info method not available -- call on bool org.apache.roller.weblogger.config. WebloggerRuntimeConfig:getBooleanProperty(String)

info method not available -- call on Boolean getAllowComments()

info method not available -- call on Locale getLocaleInstance()

method

void setCommentsStillAllowed(bool)

method	String formatPubTime(String)
pre	(soft) mLogger != null
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) init'ed(this.pubTime)
pre	(soft) this.website != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

info method not available -- call on Locale getLocaleInstance()

info method not available -- call on void org.apache.commons.logging. Log:error(Object, Throwable)

method	String formatUpdateTime(String)
pre	(soft) mLogger != null
pre	(soft) pcInheritedFieldCount <= 2³²-21
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) init'ed(this.updateTime)
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

info method not available -- call on void org.apache.commons.logging. Log:error(Object, Throwable)

method	List getComments()
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) init'ed(this.website)
post	init'ed(return_value)
post	new ArrayList(getComments#1*) num objects == 1
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getWeblogManager
unanalyzed	call on org.apache.roller.weblogger.business. WeblogManager:getComments

method	List getComments(bool, bool)
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) init'ed(this.website)
presumption	org.apache.roller.weblogger.business. Weblogger:getWeblogManager(...)@849 != null
presumption	org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@849 != null
post	init'ed(return_value)
post	new ArrayList(getComments#1) num objects == 1
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

info method not available -- call on List org.apache.roller.weblogger. business.WeblogManager:getComments(Weblog, WeblogEntry, String, Date, Date, String, bool, int, int)

method	int getCommentCount()
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) init'ed(this.website)
post	init'ed(return_value)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on java.util.ArrayList
unanalyzed	call on org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getWeblogManager
unanalyzed	call on org.apache.roller.weblogger.business. WeblogManager:getComments

Prev Msg Next Msg

+

click for all messages in this file medium

null dereference check might fail: requires comments != null

Prev Msg Next Msg

method

void setCommentCount(int)

method	List getReferers()
pre	(soft) mLogger != null
pre	(soft) pcInheritedFieldCount <= 2³²-9
pre	(soft) init'ed(this.id)
pre	(soft) init'ed(this.pcStateManager)
presumption	org.apache.roller.weblogger.business. Weblogger:getRefererManager(...)@885 != null
presumption	org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@885 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

info method not available -- call on Weblogger org.apache.roller.weblogger. business.WebloggerFactory:getWeblogger()

info method not available -- call on RefererManager org.apache.roller. weblogger.business.Weblogger:getRefererManager()

info method not available -- call on List org.apache.roller.weblogger. business.referrers.RefererManager:getReferersToEntr y(String)

info method not available -- call on void org.apache.commons.logging. Log:error(Object, Throwable)

method	String getPermalink()
pre	init'ed(this.anchor)
pre	init'ed(this.pcStateManager)
pre	init'ed(this.website)
pre	(soft) pcInheritedFieldCount <= 2³²-22
presumption	org.apache.roller.weblogger.business. Weblogger:getUrlStrategy(...)@898 != null
presumption	org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@898 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

info method not available -- call on Weblogger org.apache.roller.weblogger. business.WebloggerFactory:getWeblogger()

info method not available -- call on URLStrategy org.apache.roller.weblogger. business.Weblogger:getUrlStrategy()

info method not available -- call on String org.apache.roller.weblogger. business.URLStrategy:getWeblogEntryURL(Weblog, String, String, bool)

method	String getPermaLink()
pre	init'ed(this.anchor)
pre	init'ed(this.pcStateManager)
pre	this.website != null
pre	(soft) pcInheritedFieldCount <= 2³²-22
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &java.lang.StringBuilder:toStri ng(...)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

Prev Msg Next Msg

+

click for all messages in this file warning

unused assignment unused assignment into website

Prev Msg Next Msg

info method not available -- call on String getHandle()

method	String getCommentsLink()
pre	init'ed(this.anchor)
pre	init'ed(this.pcStateManager)
pre	this.website != null
pre	(soft) pcInheritedFieldCount <= 2³²-22
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &java.lang.StringBuilder:toStri ng(...)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on java.net.URLEncoder:encode
unanalyzed	call on getHandle

method

void setCommentsLink(String)

method	String getDisplayTitle()
pre	init'ed(this.pcStateManager)
pre	init'ed(this.title)
pre	(soft) pcInheritedFieldCount <= 2³²-20
pre	(soft) init'ed(this.text)
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	this.title: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:equals(...)@941: {0}, {1}

info method not available -- call on String org.apache.roller.weblogger.util. Utilities:removeHTML(String)

info method not available -- call on String org.apache.commons.lang. StringUtils:left(String, int)

info method not available -- call on String org.apache.roller.weblogger.util. Utilities:removeHTML(String)

method	String getRss09xDescription()
pre	init'ed(this.text)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value != null
unanalyzed	call on org.apache.commons.lang.StringEscapeUtils:e scapeHtml
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring

method	String getRss09xDescription(int)
pre	maxLength >= -2³¹+3
pre	init'ed(this.text)
presumption	org.apache.commons.lang.StringEscapeUtils:escapeHtm l(...)@962 != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	(soft) return_value != null
test_vector	maxLength: {-1}, {0..2³²-2}

info method not available -- call on String org.apache.commons.lang. StringEscapeUtils:escapeHtml(String)

method	String createAnchor()
presumption	org.apache.roller.weblogger.business. Weblogger:getWeblogManager(...)@971 != null
presumption	org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@971 != null
post	init'ed(return_value)

info method not available -- call on Weblogger org.apache.roller.weblogger. business.WebloggerFactory:getWeblogger()

info method not available -- call on WeblogManager org.apache.roller. weblogger.business.Weblogger:getWeblogManager()

info method not available -- call on String org.apache.roller.weblogger. business.WeblogManager:createAnchor(WeblogEntry)

method	String createAnchorBase()
pre	init'ed(this.pcStateManager)
pre	init'ed(this.title)
pre	(soft) pcInheritedFieldCount <= 2³²-20
pre	(soft) init'ed(this.pubTime)
pre	(soft) init'ed(this.text)
presumption	org.apache.roller.weblogger.util.Utilities:replaceN onAlphanumeric(...)@980 != null
presumption	org.apache.roller.weblogger.util.Utilities:replaceN onAlphanumeric(...)@984 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	java.util.StringTokenizer:nextToken(...)._tainted == 0
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	java.util.StringTokenizer:hasMoreTokens(...)@993: {0}, {1}
test_vector	org.apache.commons.lang.StringUtils:isEmpty(... )@979: {1}, {0}
test_vector	org.apache.commons.lang.StringUtils:isEmpty(... )@983: {0}, {1}
test_vector	org.apache.commons.lang.StringUtils:isEmpty(... )@983: {1}, {0}
test_vector	org.apache.commons.lang.StringUtils:isEmpty(... )@987: {1}, {0}

info method not available -- call on bool org.apache.commons.lang. StringUtils:isEmpty(String)

info method not available -- call on String org.apache.roller.weblogger.util. Utilities:replaceNonAlphanumeric(String, char)

info method not available -- call on bool org.apache.commons.lang. StringUtils:isEmpty(String)

info method not available -- call on String org.apache.roller.weblogger.util. Utilities:replaceNonAlphanumeric(String, char)

info method not available -- call on bool org.apache.commons.lang. StringUtils:isEmpty(String)

info method not available -- call on String org.apache.roller.util. DateUtil:format8chars(Date)

method

void setPermalink(String)

method

void setPermaLink(String)

method

void setDisplayTitle(String)

method

void setRss09xDescription(String)

method	List getPluginsList()
pre	init'ed(this.plugins)
post	init'ed(return_value)
post	new ArrayList(getPluginsList#1) num objects <= 1
test_vector	this.plugins: Addr_Set{null}, Inverse{null}

info method not available -- call on String[] org.apache.commons.lang. StringUtils:split(String, String)

method	bool isDraft()
pre	this.status != null
post	init'ed(return_value)

method

void setDraft(bool)

method	bool isPending()
pre	this.status != null
post	init'ed(return_value)

method

void setPending(bool)

method	bool isPublished()
pre	this.status != null
post	init'ed(return_value)

method

void setPublished(bool)

method	String getTransformedText()
pre	mLogger != null
pre	init'ed(this.text)
pre	this.website != null
pre	(soft) init'ed(this.plugins)
post	init'ed(return_value)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.commons.lang.StringUtils:split
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on getInitializedPlugins
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.util.Map:get
unanalyzed	call on org.apache.roller.weblogger.business. plugins.entry.WeblogEntryPlugin:render
unanalyzed	call on org.apache.roller.weblogger.business. plugins.entry.WeblogEntryPlugin:getName

method

void setTransformedText(String)

method	String getTransformedSummary()
pre	mLogger != null
pre	init'ed(this.summary)
pre	this.website != null
pre	(soft) init'ed(this.plugins)
post	init'ed(return_value)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.commons.lang.StringUtils:split
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on getInitializedPlugins
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.util.Map:get
unanalyzed	call on org.apache.roller.weblogger.business. plugins.entry.WeblogEntryPlugin:render
unanalyzed	call on org.apache.roller.weblogger.business. plugins.entry.WeblogEntryPlugin:getName

method

void setTransformedSummary(String)

method	bool hasWritePermissions(User)
pre	user != null
pre	init'ed(user.pcStateManager)
pre	user.roles != null
pre	(soft) org/apache/roller/weblogger/pojos/User. pcInheritedFieldCount <= 2³²-10
pre	(soft) org/apache/roller/weblogger/pojos/UserRole. pcInheritedFieldCount <= 2³²-2
pre	(soft) init'ed(org/apache/roller/weblogger/pojos/We blogPermission.AUTHOR)
pre	(soft) init'ed(org/apache/roller/weblogger/pojos/We blogPermission.LIMITED)
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) this.status != null
pre	(soft) this.website != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.Set:iterator
test_vector	hasUserPermissions(...)@1112: {1}, {0}
test_vector	hasUserPermissions(...)@1115: {0}, {1}
test_vector	java.lang.String:equals(...)@1052: {1}, {0}
test_vector	java.lang.String:equals(...)@1060: {0}, {1}

info method not available -- call on bool hasUserPermissions(User, short)

method	String render(String)
pre	mLogger != null
pre	this.website != null
pre	(soft) init'ed(this.plugins)
presumption	java.util.Map:get(...)@1146 != null
presumption	java.util.Map:keySet(...)@1142 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.commons.lang.StringUtils:split
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on java.util.ArrayList
test_vector	str: Addr_Set{null}, Inverse{null}
test_vector	getInitializedPlugins(...)@1132: Addr_Set{null}, Inverse{null}
test_vector	java.util.Iterator:hasNext(...)@1143: {0}, {1}
test_vector	java.util.List:contains(...)@1145: {0}, {1}
test_vector	java.util.List:isEmpty(...)@1137: {1}, {0}

info method not available -- call on void org.apache.commons.logging. Log:debug(Object)

info method not available -- call on Map getInitializedPlugins()

info method not available -- call on String org.apache.roller.weblogger. business.plugins.entry.WeblogEntryPlugin:render(Web logEntry, String)

info method not available -- call on String org.apache.roller.weblogger. business.plugins.entry.WeblogEntryPlugin:getName()

info method not available -- call on void org.apache.commons.logging. Log:error(Object, Throwable)

method	String displayContent(String)
pre	mLogger != null
pre	init'ed(this.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) init'ed(this.plugins)
pre	(soft) init'ed(this.summary)
pre	(soft) init'ed(this.text)
pre	(soft) this.website != null
presumption	org.apache.roller.weblogger.util.I18nMessages:getMe ssages(...)@1194 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	init'ed(return_value)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on org.apache.commons.lang.StringUtils:split
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on render
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on getInitializedPlugins
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.util.Map:get
unanalyzed	call on org.apache.roller.weblogger.business. plugins.entry.WeblogEntryPlugin:render
unanalyzed	call on org.apache.roller.weblogger.business. plugins.entry.WeblogEntryPlugin:getName
test_vector	readMoreLink: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:equals(...)@1174: {0}, {1}
test_vector	java.lang.String:length(...)@1174: {0}, {1..2³²-1}
test_vector	org.apache.commons.lang.StringUtils:isNotEmpty(... )@1178: {0}, {1}
test_vector	org.apache.commons.lang.StringUtils:isNotEmpty(... )@1186: {0}, {1}
test_vector	org.apache.commons.lang.StringUtils:isNotEmpty(... )@1188: {0}, {1}

info method not available -- call on bool org.apache.commons.lang. StringUtils:isNotEmpty(String)

info method not available -- call on Locale getLocaleInstance()

info method not available -- call on I18nMessages org.apache.roller. weblogger.util.I18nMessages:getMessages(Locale)

info method not available -- call on String org.apache.roller.weblogger.util. I18nMessages:getString(String, List)

method	String getDisplayContent()
pre	mLogger != null
pre	init'ed(this.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-22
pre	(soft) init'ed(this.plugins)
pre	(soft) init'ed(this.summary)
pre	(soft) init'ed(this.text)
pre	(soft) this.website != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	init'ed(return_value)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:trim
unanalyzed	call on org.apache.commons.lang.StringUtils:split
unanalyzed	call on java.util.Arrays:asList
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on getLocaleInstance
unanalyzed	call on org.apache.commons.lang.StringUtils:isNotEm pty
unanalyzed	call on getTransformedText
unanalyzed	call on getTransformedSummary
unanalyzed	call on java.util.List:add
unanalyzed	call on org.apache.roller.weblogger.util. I18nMessages:getMessages
unanalyzed	call on org.apache.roller.weblogger.util. I18nMessages:getString
unanalyzed	call on render
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on getInitializedPlugins
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.util.Map:get
unanalyzed	call on org.apache.roller.weblogger.business. plugins.entry.WeblogEntryPlugin:render
unanalyzed	call on org.apache.roller.weblogger.business. plugins.entry.WeblogEntryPlugin:getName

method

void setDisplayContent(String)

Prev Msg Next Msg

+

click for all messages in this file low

precondition failure org/apache/roller/weblogger/pojos/WeblogEntry. pcReplaceField: Param_1 - pcInheritedFieldCount in 0..21

+

low

precondition failure org/apache/roller/weblogger/pojos/WeblogEntry. pcProvideField: Param_1 - pcInheritedFieldCount in 0..21

+

click for all messages in this file low

precondition failure org/apache/roller/weblogger/pojos/WeblogEntry. pcCopyField: Param_2 - pcInheritedFieldCount in 0..21

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)

info method not available -- call on Object org.apache.openjpa.enhance. StateManager:replaceObjectField(PersistenceCapable, int)

info method not available -- call on String org.apache.openjpa.enhance. StateManager:replaceStringField(PersistenceCapable, int)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:providedObjectField(PersistenceCapable , int, Object)

info method not available -- call on void org.apache.openjpa.enhance. StateManager:providedStringField(PersistenceCapable , int, String)

info method not available -- call on Object org.apache.openjpa.enhance. StateManager:getGenericContext()

info method not available -- call on Object org.apache.openjpa.enhance. StateManager:fetchObjectId()

info method not available -- call on bool org.apache.openjpa.enhance. StateManager:isDeleted()

info method not available -- call on bool org.apache.openjpa.enhance. StateManager:isDirty()

info method not available -- call on bool org.apache.openjpa.enhance. StateManager:isNew()

info method not available -- call on bool org.apache.openjpa.enhance. StateManager:isPersistent()

info method not available -- call on bool org.apache.openjpa.enhance. StateManager:isTransactional()

info method not available -- call on bool org.apache.openjpa.enhance. StateManager:serializing()

info method not available -- call on void org.apache.openjpa.enhance. StateManager:dirty(String)

info method not available -- call on Object org.apache.openjpa.enhance. StateManager:getVersion()

info method not available -- call on StateManager org.apache.openjpa.enhance. StateManager:replaceStateManager(StateManager)

info method not available -- call on String org.apache.openjpa.util. StringId:getId()

info method not available -- call on void org.apache.openjpa.enhance. FieldConsumer:storeStringField(int, String)

info method not available -- call on String org.apache.openjpa.util. StringId:getId()

info method not available -- call on void org.apache.openjpa.util. StringId(Class, String)

info method not available -- call on bool org.apache.openjpa.enhance. StateManager:isDetached()

Prev Msg Next Msg

info	method not available	-- call on LogFactory org.apache.commons.logging. LogFactory:getFactory()
info	method not available	-- call on Log org.apache.commons.logging. LogFactory:getInstance(Class)
info	method not available	-- call on void org.apache.openjpa.enhance. PCRegistry:register(Class, String[], Class[], byte[], Class, String, PersistenceCapable)

info	method not available	-- call on void org.apache.commons.lang.builder. EqualsBuilder()
info	method not available	-- call on EqualsBuilder org.apache.commons.lang. builder.EqualsBuilder:append(Object, Object)
info	method not available	-- call on bool org.apache.commons.lang.builder. EqualsBuilder:isEquals()

	info	method not available	-- call on Weblogger org.apache.roller.weblogger. business.WebloggerFactory:getWeblogger()
	info	method not available	-- call on WeblogManager org.apache.roller. weblogger.business.Weblogger:getWeblogManager()

	info	method not available	-- call on String org.apache.roller.weblogger.util. Utilities:removeHTML(String)
	info	method not available	-- call on String org.apache.commons.lang. StringUtils:left(String, int)

info	method not available	-- call on Locale getLocaleInstance()
info	method not available	-- call on I18nMessages org.apache.roller. weblogger.util.I18nMessages:getMessages(Locale)
info	method not available	-- call on String org.apache.roller.weblogger.util. I18nMessages:getString(String, List)