Messages

Last Msg First Msg

method	String getId()
pre	init'ed(Param_0.id)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-4
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³²-4
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:trim
unanalyzed	call on java.lang.String:length
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

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

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

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

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

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

method	void setPath(String)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.path)
pre	(soft) pcInheritedFieldCount <= 2³²-7
post	Param_0.path == One-of{Param_1, old Param_0.path}
post	(soft) init'ed(Param_0.path)
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³²-8
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³²-8
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	WeblogBookmarkFolder getParent()
pre	init'ed(Param_0.parentFolder)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-6
post	return_value == Param_0.parentFolder
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

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

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

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

method	Set getBookmarks()
pre	init'ed(Param_0.bookmarks)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(pcInheritedFieldCount)
post	return_value == Param_0.bookmarks
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

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

method	int pcGetEnhancementContractVersion()
post	return_value == 2

method	void pcClearFields()
post	Param_0.bookmarks == null
post	Param_0.childFolders == null
post	Param_0.description == null
post	Param_0.id == null
post	Param_0.name == null
post	Param_0.parentFolder == null
post	Param_0.path == null
post	Param_0.website == null
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:length

method	PersistenceCapable pcNewInstance(StateManager, Object, bool)
pre	Param_2 != null
post	return_value == &new WeblogBookmarkFolder(pcNew Instance#1)
post	new TreeSet(WeblogBookmarkFolder#1) num objects == 1
post	new TreeSet(WeblogBookmarkFolder#2) num objects == 1
post	new WeblogBookmarkFolder(pcNewInstance#1) num objects == 1
post	return_value.bookmarks in Addr_Set{null,&new TreeSet(WeblogBookmarkFolder#2)}
post	return_value.childFolders in Addr_Set{null, &new TreeSet(WeblogBookmarkFolder#1)}
post	return_value.description == null
post	init'ed(return_value.id)
post	return_value.name == null
post	return_value.parentFolder == null
post	return_value.path == null
post	return_value.pcStateManager == Param_1
post	init'ed(return_value.pcStateManager)
post	return_value.website == null
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on java.util.TreeSet
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:length
unanalyzed	call on org.apache.openjpa.util.StringId:getId
test_vector	Param_3: {0}, {1}

method	PersistenceCapable pcNewInstance(StateManager, bool)
post	return_value == &new WeblogBookmarkFolder(pcNew Instance#1)
post	new TreeSet(WeblogBookmarkFolder#1) num objects == 1
post	new TreeSet(WeblogBookmarkFolder#2) num objects == 1
post	new WeblogBookmarkFolder(pcNewInstance#1) num objects == 1
post	return_value.bookmarks in Addr_Set{null,&new TreeSet(WeblogBookmarkFolder#2)}
post	return_value.childFolders in Addr_Set{null, &new TreeSet(WeblogBookmarkFolder#1)}
post	return_value.description == null
post	init'ed(return_value.id)
post	return_value.name == null
post	return_value.parentFolder == null
post	return_value.path == null
post	return_value.pcStateManager == Param_1
post	init'ed(return_value.pcStateManager)
post	return_value.website == null
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on java.util.TreeSet
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:length
test_vector	Param_2: {0}, {1}

method	int pcGetManagedFieldCount()
post	return_value == 8

method	void pcReplaceField(int)
pre	Param_0.pcStateManager != null
pre	Param_1 - pcInheritedFieldCount in 0..7
pre	init'ed(pcInheritedFieldCount)
post	possibly_updated(Param_0.bookmarks)
post	possibly_updated(Param_0.childFolders)
post	possibly_updated(Param_0.description)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.name)
post	possibly_updated(Param_0.parentFolder)
post	possibly_updated(Param_0.path)
post	possibly_updated(Param_0.website)
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:length
test_vector	Param_1 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}

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.bookmarks)
post	possibly_updated(Param_0.childFolders)
post	possibly_updated(Param_0.description)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.name)
post	possibly_updated(Param_0.parentFolder)
post	possibly_updated(Param_0.path)
post	possibly_updated(Param_0.website)
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:length
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..7
pre	init'ed(pcInheritedFieldCount)
pre	(soft) init'ed(Param_0.bookmarks)
pre	(soft) init'ed(Param_0.childFolders)
pre	(soft) init'ed(Param_0.description)
pre	(soft) init'ed(Param_0.id)
pre	(soft) init'ed(Param_0.name)
pre	(soft) init'ed(Param_0.parentFolder)
pre	(soft) init'ed(Param_0.path)
pre	(soft) init'ed(Param_0.website)
test_vector	Param_1 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}

method	void pcProvideFields(int[])
pre	Param_1 != null
pre	Param_1.length <= 2³²-1
pre	(soft) init'ed(Param_0.bookmarks)
pre	(soft) init'ed(Param_0.childFolders)
pre	(soft) init'ed(Param_0.description)
pre	(soft) init'ed(Param_0.id)
pre	(soft) init'ed(Param_0.name)
pre	(soft) init'ed(Param_0.parentFolder)
pre	(soft) init'ed(Param_0.path)
pre	(soft) Param_0.pcStateManager != null
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(WeblogBookmarkFolder, int)
pre	Param_1 != null
pre	Param_2 - pcInheritedFieldCount in 0..7
pre	init'ed(pcInheritedFieldCount)
pre	(soft) init'ed(Param_1.bookmarks)
pre	(soft) init'ed(Param_1.childFolders)
pre	(soft) init'ed(Param_1.description)
pre	(soft) init'ed(Param_1.id)
pre	(soft) init'ed(Param_1.name)
pre	(soft) init'ed(Param_1.parentFolder)
pre	(soft) init'ed(Param_1.path)
pre	(soft) init'ed(Param_1.website)
post	possibly_updated(Param_0.bookmarks)
post	possibly_updated(Param_0.childFolders)
post	possibly_updated(Param_0.description)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.name)
post	possibly_updated(Param_0.parentFolder)
post	possibly_updated(Param_0.path)
post	possibly_updated(Param_0.website)
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:length
test_vector	Param_2 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}

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.bookmarks)
pre	(soft) init'ed(Param_1.childFolders)
pre	(soft) init'ed(Param_1.description)
pre	(soft) init'ed(Param_1.id)
pre	(soft) init'ed(Param_1.name)
pre	(soft) init'ed(Param_1.parentFolder)
pre	(soft) init'ed(Param_1.path)
pre	(soft) init'ed(Param_1.website)
pre	(soft) init'ed(Param_2[...])
pre	(soft) init'ed(pcInheritedFieldCount)
post	possibly_updated(Param_0.bookmarks)
post	possibly_updated(Param_0.childFolders)
post	possibly_updated(Param_0.description)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.name)
post	possibly_updated(Param_0.parentFolder)
post	possibly_updated(Param_0.path)
post	possibly_updated(Param_0.website)
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:length

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³²-4

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

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.WeblogBookmarkFo lder__static_init
post	init'ed(log)
post	pcFieldFlags == &new byte[](WeblogBookmarkFolde r__static_init#3)
post	pcFieldNames == &new String[](WeblogBookmarkFol der__static_init#1)
post	pcFieldTypes == &new Class[](WeblogBookmarkFold er__static_init#2)
post	new Class[](WeblogBookmarkFolder__static_init#2) num objects == 1
post	new String[](WeblogBookmarkFolder__static_init#1) num objects == 1
post	new byte[](WeblogBookmarkFolder__static_init#3) num objects == 1
post	pcFieldTypes.length == 8
post	pcFieldNames.length == 8
post	pcFieldFlags.length == 8
post	pcFieldNames[0] == &"bookmarks"
post	pcFieldNames[1] == &"description"
post	pcFieldNames[2] == &"folders"
post	pcFieldNames[3] == &"id"
post	pcFieldNames[4] == &"name"
post	pcFieldNames[5] == &"parent"
post	pcFieldNames[6] == &"path"
post	pcFieldNames[7] == &"website"
post	pcFieldFlags[0] == 5
post	pcFieldFlags[2] == 5
post	pcFieldFlags[1] == 26
post	pcFieldFlags[3] == 26
post	pcFieldFlags[4] == 26
post	pcFieldFlags[5] == 26
post	pcFieldFlags[6] == 26
post	pcFieldFlags[7] == 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.util.TreeSet

info method not available -- call on Log org.apache.commons.logging. LogFactory:getLog(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. WeblogBookmarkFolder()
post	this.bookmarks == &new TreeSet(WeblogBookmarkFo lder#2)
post	this.childFolders == &new TreeSet(WeblogBookmar kFolder#1)
post	this.description == null
post	this.name == null
post	this.parentFolder == null
post	this.path == null
post	this.website == null
post	init'ed(this.id)
post	new TreeSet(WeblogBookmarkFolder#1) num objects == 1
post	new TreeSet(WeblogBookmarkFolder#2) num objects == 1

method	void org.apache.roller.weblogger.pojos. WeblogBookmarkFolder(WeblogBookmarkFolder, String, String, Weblog)
pre	(soft) init'ed(parent.path)
pre	(soft) init'ed(parent.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-7
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	this.bookmarks == &new TreeSet(WeblogBookmarkFo lder#2)
post	this.childFolders == &new TreeSet(WeblogBookmar kFolder#1)
post	this.description == desc
post	init'ed(this.description)
post	init'ed(this.id)
post	this.name == name
post	init'ed(this.name)
post	this.parentFolder == parent
post	init'ed(this.parentFolder)
post	this.path in Addr_Set{&".",&java.lang. StringBuilder:toString(...),&java.lang. StringBuilder:toString(...)}
post	this.website == website
post	init'ed(this.website)
post	new TreeSet(WeblogBookmarkFolder#1) num objects == 1
post	new TreeSet(WeblogBookmarkFolder#2) num objects == 1
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	parent: Inverse{null}, Addr_Set{null}
test_vector	java.lang.String:equals(...)@81: {0}, {1}

method	String toString()
pre	init'ed(this.id)
pre	init'ed(this.path)
post	java.lang.StringBuffer:toString(...)._tainted == this.id._tainted \| this.path._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.path)
pre	(soft) init'ed(other.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-7
pre	(soft) init'ed(this.path)
pre	(soft) init'ed(this.pcStateManager)
presumption	org.apache.commons.lang.builder.EqualsBuilder:appen d(...)@106 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	other: Inverse{null}, Addr_Set{null}

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.path)
pre	init'ed(this.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-7
presumption	org.apache.commons.lang.builder.HashCodeBuilder:app end(...)@117 != 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	int compareTo(Object)
pre	o != null
pre	init'ed(o.name)
pre	init'ed(o.pcStateManager)
pre	this.name != null
pre	init'ed(this.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-5
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField

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(...)@146: {1.. 2³²-1}, {0}

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

method	void pcsetName(String)
post	this.name == Param_1
post	init'ed(this.name)

method	String pcgetDescription()
pre	init'ed(this.description)
post	return_value == this.description
post	init'ed(return_value)

method	void pcsetDescription(String)
post	this.description == Param_1
post	init'ed(this.description)

method	String pcgetPath()
pre	init'ed(this.path)
post	return_value == this.path
post	init'ed(return_value)

method	void pcsetPath(String)
post	this.path == Param_1
post	init'ed(this.path)

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	WeblogBookmarkFolder pcgetParent()
pre	init'ed(this.parentFolder)
post	return_value == this.parentFolder
post	init'ed(return_value)

method	void pcsetParent(WeblogBookmarkFolder)
post	this.parentFolder == Param_1
post	init'ed(this.parentFolder)

method	Set pcgetFolders()
pre	init'ed(this.childFolders)
post	return_value == this.childFolders
post	init'ed(return_value)

method	void pcsetFolders(Set)
post	this.childFolders == Param_1
post	init'ed(this.childFolders)

method	Set pcgetBookmarks()
pre	init'ed(this.bookmarks)
post	return_value == this.bookmarks
post	init'ed(return_value)

method	void pcsetBookmarks(Set)
post	this.bookmarks == Param_1
post	init'ed(this.bookmarks)

method	void addFolder(WeblogBookmarkFolder)
pre	folder != null
pre	init'ed(folder.pcStateManager)
pre	this.childFolders != null
pre	init'ed(this.pcStateManager)
pre	(soft) folder.name != null
pre	(soft) init'ed(folder.parentFolder)
pre	(soft) pcInheritedFieldCount <= 2³²-6
presumption	java.util.Iterator:hasNext(...)@325 == 0
post	folder.parentFolder == One-of{this, old folder.parentFolder}
post	(soft) init'ed(folder.parentFolder)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingObjectField
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.String:equals

method	void addBookmark(WeblogBookmark)
pre	bookmark != null
pre	init'ed(bookmark.pcStateManager)
pre	this.bookmarks != null
pre	init'ed(this.pcStateManager)
pre	(soft) init'ed(bookmark.folder)
pre	(soft) org/apache/roller/weblogger/pojos/WeblogBook mark.pcInheritedFieldCount <= 2³²-3
pre	(soft) init'ed(pcInheritedFieldCount)
post	bookmark.folder == One-of{this, old bookmark.folder}
post	(soft) init'ed(bookmark.folder)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingObjectField

method	List retrieveBookmarks(bool)
presumption	org.apache.roller.weblogger.business. Weblogger:getBookmarkManager(...)@311 != null
presumption	org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@311 != null
post	init'ed(return_value)

info method not available -- call on List org.apache.roller.weblogger. business.BookmarkManager:getBookmarks(WeblogBookmar kFolder, bool)

method	bool hasFolder(String)
pre	this.childFolders != null
pre	init'ed(this.pcStateManager)
pre	(soft) name != null
pre	(soft) pcInheritedFieldCount <= 2³²-5
presumption	java.util.Iterator:next(...)@326 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	java.lang.String:equals(...)@327: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@325: {0}, {1}

method	bool descendentOf(WeblogBookmarkFolder)
pre	init'ed(this.parentFolder)
pre	init'ed(this.pcStateManager)
pre	(soft) ancestor != null
pre	(soft) init'ed(ancestor.path)
pre	(soft) init'ed(ancestor.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-7
pre	(soft) this.path != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	this.parentFolder: Inverse{null}, Addr_Set{null}

method	void updateName(String)
pre	log != null
pre	this.childFolders != null
pre	init'ed(this.parentFolder)
pre	init'ed(this.pcStateManager)
pre	(soft) init'ed(this.name)
pre	(soft) init'ed(this.path)
pre	(soft) pcInheritedFieldCount <= 2³²-7
pre	(soft) init'ed(this...path)
pre	(soft) init'ed(this...pcStateManager)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	this.name == One-of{newName, old this.name}
post	(soft) init'ed(this.name)
post	this.path == One-of{&".", old this.path, &java.lang.StringBuilder:toString(...)}
post	init'ed(this.path)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingStringField
unanalyzed	call on org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getBookmarkManager
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.String:equals
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on org.apache.roller.weblogger.business. BookmarkManager:saveFolder
unanalyzed	call on updatePathTree
test_vector	this.parentFolder: Inverse{null}, Addr_Set{null}
test_vector	java.lang.String:equals(...)@361: {0}, {1}

method	void updatePathTree(WeblogBookmarkFolder)
pre	folder != null
pre	folder.childFolders != null
pre	init'ed(folder.path)
pre	init'ed(folder.pcStateManager)
pre	log != null
pre	(soft) pcInheritedFieldCount <= 2³²-7
presumption	childFolder.childFolders@393 != null
presumption	java.util.Iterator:next(...)@381 != null
presumption	org.apache.roller.weblogger.business. Weblogger:getBookmarkManager(...)@391 != null
presumption	org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger(...)@391 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	possibly_updated(java.lang.StringBuilder:toString(. ..)._tainted)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingStringField
unanalyzed	call on org.apache.roller.weblogger.business. WebloggerFactory:getWeblogger
unanalyzed	call on org.apache.roller.weblogger.business. Weblogger:getBookmarkManager
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.lang.String:equals
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on org.apache.roller.weblogger.business. BookmarkManager:saveFolder
unanalyzed	call on updatePathTree
test_vector	java.lang.String:equals(...)@386: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@380: {0}, {1}

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

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

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

info method not available -- call on void org.apache.roller.weblogger. business.BookmarkManager:saveFolder(WeblogBookmarkF older)

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

Prev Msg Next Msg

+

click for all messages in this file low

precondition failure org/apache/roller/weblogger/pojos/WeblogBookmarkFol der.pcReplaceField: Param_1 - pcInheritedFieldCount in 0..7

+

low

precondition failure org/apache/roller/weblogger/pojos/WeblogBookmarkFol der.pcProvideField: Param_1 - pcInheritedFieldCount in 0..7

+

click for all messages in this file low

precondition failure org/apache/roller/weblogger/pojos/WeblogBookmarkFol der.pcCopyField: Param_2 - pcInheritedFieldCount in 0..7

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: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 Log org.apache.commons.logging. LogFactory:getLog(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 BookmarkManager org.apache.roller. weblogger.business.Weblogger:getBookmarkManager()