Messages

Last Msg First Msg

method	String getId()
pre	init'ed(Param_0.id)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-6
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³²-6
post	Param_0.id == One-of{Param_1, old Param_0.id}
post	(soft) init'ed(Param_0.id)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

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

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

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

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

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

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

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

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

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

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

method	Date getDateCreated()
pre	init'ed(Param_0.dateCreated)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) pcInheritedFieldCount <= 2³²-2
post	init'ed(return_value)
unanalyzed	call on java.util.Date:clone
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

method	void setDateCreated(Date)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(Param_0.dateCreated)
pre	(soft) pcInheritedFieldCount <= 2³²-2
post	init'ed(Param_0.dateCreated)
unanalyzed	call on java.util.Date:clone
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³²-7
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³²-7
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	String getTimeZone()
pre	init'ed(Param_0.pcStateManager)
pre	init'ed(Param_0.timeZone)
pre	(soft) pcInheritedFieldCount <= 2³²-12
post	return_value == Param_0.timeZone
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

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

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

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

method	String getActivationCode()
pre	init'ed(Param_0.activationCode)
pre	init'ed(Param_0.pcStateManager)
pre	(soft) init'ed(pcInheritedFieldCount)
post	return_value == Param_0.activationCode
post	init'ed(return_value)
test_vector	Param_0.pcStateManager: Inverse{null}, Addr_Set{null}

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

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

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

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

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

method	int pcGetEnhancementContractVersion()
post	return_value == 2

method	org.apache.roller.weblogger.pojos.User__static_ init
post	pcFieldFlags == &new byte[](User__static_ init#3)
post	pcFieldNames == &new String[](User__static_ init#1)
post	pcFieldTypes == &new Class[](User__static_ init#2)
post	new Class[](User__static_init#2) num objects == 1
post	new String[](User__static_init#1) num objects == 1
post	new byte[](User__static_init#3) num objects == 1
post	pcFieldTypes.length == 13
post	pcFieldNames.length == 13
post	pcFieldFlags.length == 13
post	pcFieldNames[0] == &"activationCode"
post	pcFieldNames[10] == &"screenName"
post	pcFieldNames[11] == &"timeZone"
post	pcFieldNames[12] == &"userName"
post	pcFieldNames[1] == &"dateCreated"
post	pcFieldNames[2] == &"emailAddress"
post	pcFieldNames[3] == &"enabled"
post	pcFieldNames[4] == &"fullName"
post	pcFieldNames[5] == &"id"
post	pcFieldNames[6] == &"locale"
post	pcFieldNames[7] == &"password"
post	pcFieldNames[8] == &"permissions"
post	pcFieldNames[9] == &"roles"
post	pcFieldFlags[0] == 26
post	pcFieldFlags[10] == 26
post	pcFieldFlags[11] == 26
post	pcFieldFlags[12] == 26
post	pcFieldFlags[1] == 26
post	pcFieldFlags[2] == 26
post	pcFieldFlags[3] == 26
post	pcFieldFlags[4] == 26
post	pcFieldFlags[5] == 26
post	pcFieldFlags[6] == 26
post	pcFieldFlags[7] == 26
post	pcFieldFlags[8] == 5
post	pcFieldFlags[9] == 5
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.HashSet
unanalyzed	call on java.util.ArrayList

method	void pcClearFields()
post	Param_0.activationCode == null
post	Param_0.emailAddress == null
post	Param_0.enabled == null
post	Param_0.fullName == null
post	Param_0.id == null
post	Param_0.locale == null
post	Param_0.password == null
post	Param_0.permissions == null
post	Param_0.roles == null
post	Param_0.screenName == null
post	Param_0.timeZone == null
post	Param_0.userName == null
post	init'ed(Param_0.dateCreated)
unanalyzed	call on java.util.Date:clone

method	PersistenceCapable pcNewInstance(StateManager, Object, bool)
pre	Param_2 != null
post	return_value == &new User(pcNewInstance#1)
post	new ArrayList(User#2) num objects == 1
post	new HashSet(User#1) num objects == 1
post	new User(pcNewInstance#1) num objects == 1
post	init'ed(return_value.activationCode)
post	init'ed(return_value.dateCreated)
post	init'ed(return_value.emailAddress)
post	return_value.enabled == One-of{java.lang.Boolean. TRUE, null}
post	init'ed(return_value.enabled)
post	init'ed(return_value.fullName)
post	init'ed(return_value.id)
post	init'ed(return_value.locale)
post	init'ed(return_value.password)
post	return_value.pcStateManager == Param_1
post	init'ed(return_value.pcStateManager)
post	return_value.permissions in Addr_Set{null,&new ArrayList(User#2)}
post	return_value.roles in Addr_Set{null,&new HashSet(User#1)}
post	init'ed(return_value.screenName)
post	init'ed(return_value.timeZone)
post	init'ed(return_value.userName)
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Date:clone
unanalyzed	call on org.apache.openjpa.util.StringId:getId
test_vector	Param_3: {0}, {1}

method	PersistenceCapable pcNewInstance(StateManager, bool)
post	return_value == &new User(pcNewInstance#1)
post	new ArrayList(User#2) num objects == 1
post	new HashSet(User#1) num objects == 1
post	new User(pcNewInstance#1) num objects == 1
post	init'ed(return_value.activationCode)
post	init'ed(return_value.dateCreated)
post	init'ed(return_value.emailAddress)
post	return_value.enabled == One-of{java.lang.Boolean. TRUE, null}
post	init'ed(return_value.enabled)
post	init'ed(return_value.fullName)
post	init'ed(return_value.id)
post	init'ed(return_value.locale)
post	init'ed(return_value.password)
post	return_value.pcStateManager == Param_1
post	init'ed(return_value.pcStateManager)
post	return_value.permissions in Addr_Set{null,&new ArrayList(User#2)}
post	return_value.roles in Addr_Set{null,&new HashSet(User#1)}
post	init'ed(return_value.screenName)
post	init'ed(return_value.timeZone)
post	init'ed(return_value.userName)
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Date:clone
test_vector	Param_2: {0}, {1}

method	int pcGetManagedFieldCount()
post	return_value == 13

method	void pcReplaceField(int)
pre	Param_0.pcStateManager != null
pre	Param_1 - pcInheritedFieldCount in 0..12
pre	init'ed(pcInheritedFieldCount)
post	possibly_updated(Param_0.activationCode)
post	possibly_updated(Param_0.dateCreated)
post	possibly_updated(Param_0.emailAddress)
post	possibly_updated(Param_0.enabled)
post	possibly_updated(Param_0.fullName)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.locale)
post	possibly_updated(Param_0.password)
post	possibly_updated(Param_0.permissions)
post	possibly_updated(Param_0.roles)
post	possibly_updated(Param_0.screenName)
post	possibly_updated(Param_0.timeZone)
post	possibly_updated(Param_0.userName)
unanalyzed	call on java.util.Date:clone
test_vector	Param_1 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {10}, {11}, {12}

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.activationCode)
post	possibly_updated(Param_0.dateCreated)
post	possibly_updated(Param_0.emailAddress)
post	possibly_updated(Param_0.enabled)
post	possibly_updated(Param_0.fullName)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.locale)
post	possibly_updated(Param_0.password)
post	possibly_updated(Param_0.permissions)
post	possibly_updated(Param_0.roles)
post	possibly_updated(Param_0.screenName)
post	possibly_updated(Param_0.timeZone)
post	possibly_updated(Param_0.userName)
unanalyzed	call on java.util.Date:clone
unanalyzed	call on org.apache.openjpa.enhance.StateManager:rep laceStringField
unanalyzed	call on org.apache.openjpa.enhance.StateManager:rep laceObjectField

method	void pcProvideField(int)
pre	Param_0.pcStateManager != null
pre	Param_1 - pcInheritedFieldCount in 0..12
pre	init'ed(pcInheritedFieldCount)
pre	(soft) init'ed(Param_0.activationCode)
pre	(soft) init'ed(Param_0.dateCreated)
pre	(soft) init'ed(Param_0.emailAddress)
pre	(soft) init'ed(Param_0.enabled)
pre	(soft) init'ed(Param_0.fullName)
pre	(soft) init'ed(Param_0.id)
pre	(soft) init'ed(Param_0.locale)
pre	(soft) init'ed(Param_0.password)
pre	(soft) init'ed(Param_0.permissions)
pre	(soft) init'ed(Param_0.roles)
pre	(soft) init'ed(Param_0.screenName)
pre	(soft) init'ed(Param_0.timeZone)
pre	(soft) init'ed(Param_0.userName)
unanalyzed	call on java.util.Date:clone
test_vector	Param_1 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {10}, {11}, {12}

method	void pcProvideFields(int[])
pre	Param_1 != null
pre	Param_1.length <= 2³²-1
pre	(soft) init'ed(Param_0.activationCode)
pre	(soft) init'ed(Param_0.dateCreated)
pre	(soft) init'ed(Param_0.emailAddress)
pre	(soft) init'ed(Param_0.enabled)
pre	(soft) init'ed(Param_0.fullName)
pre	(soft) init'ed(Param_0.id)
pre	(soft) init'ed(Param_0.locale)
pre	(soft) init'ed(Param_0.password)
pre	(soft) Param_0.pcStateManager != null
pre	(soft) init'ed(Param_0.permissions)
pre	(soft) init'ed(Param_0.roles)
pre	(soft) init'ed(Param_0.screenName)
pre	(soft) init'ed(Param_0.timeZone)
pre	(soft) init'ed(Param_0.userName)
pre	(soft) init'ed(Param_1[...])
pre	(soft) init'ed(pcInheritedFieldCount)
unanalyzed	call on java.util.Date:clone
unanalyzed	call on org.apache.openjpa.enhance.StateManager:pro videdStringField
unanalyzed	call on org.apache.openjpa.enhance.StateManager:pro videdObjectField

method	void pcCopyField(User, int)
pre	Param_1 != null
pre	Param_2 - pcInheritedFieldCount in 0..12
pre	init'ed(pcInheritedFieldCount)
pre	(soft) init'ed(Param_1.activationCode)
pre	(soft) init'ed(Param_1.dateCreated)
pre	(soft) init'ed(Param_1.emailAddress)
pre	(soft) init'ed(Param_1.enabled)
pre	(soft) init'ed(Param_1.fullName)
pre	(soft) init'ed(Param_1.id)
pre	(soft) init'ed(Param_1.locale)
pre	(soft) init'ed(Param_1.password)
pre	(soft) init'ed(Param_1.permissions)
pre	(soft) init'ed(Param_1.roles)
pre	(soft) init'ed(Param_1.screenName)
pre	(soft) init'ed(Param_1.timeZone)
pre	(soft) init'ed(Param_1.userName)
post	possibly_updated(Param_0.activationCode)
post	possibly_updated(Param_0.dateCreated)
post	possibly_updated(Param_0.emailAddress)
post	possibly_updated(Param_0.enabled)
post	possibly_updated(Param_0.fullName)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.locale)
post	possibly_updated(Param_0.password)
post	possibly_updated(Param_0.permissions)
post	possibly_updated(Param_0.roles)
post	possibly_updated(Param_0.screenName)
post	possibly_updated(Param_0.timeZone)
post	possibly_updated(Param_0.userName)
unanalyzed	call on java.util.Date:clone
test_vector	Param_2 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}, {8}, {9}, {10}, {11}, {12}

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.activationCode)
pre	(soft) init'ed(Param_1.dateCreated)
pre	(soft) init'ed(Param_1.emailAddress)
pre	(soft) init'ed(Param_1.enabled)
pre	(soft) init'ed(Param_1.fullName)
pre	(soft) init'ed(Param_1.id)
pre	(soft) init'ed(Param_1.locale)
pre	(soft) init'ed(Param_1.password)
pre	(soft) init'ed(Param_1.permissions)
pre	(soft) init'ed(Param_1.roles)
pre	(soft) init'ed(Param_1.screenName)
pre	(soft) init'ed(Param_1.timeZone)
pre	(soft) init'ed(Param_1.userName)
pre	(soft) init'ed(Param_2[...])
pre	(soft) init'ed(pcInheritedFieldCount)
post	possibly_updated(Param_0.activationCode)
post	possibly_updated(Param_0.dateCreated)
post	possibly_updated(Param_0.emailAddress)
post	possibly_updated(Param_0.enabled)
post	possibly_updated(Param_0.fullName)
post	possibly_updated(Param_0.id)
post	possibly_updated(Param_0.locale)
post	possibly_updated(Param_0.password)
post	possibly_updated(Param_0.permissions)
post	possibly_updated(Param_0.roles)
post	possibly_updated(Param_0.screenName)
post	possibly_updated(Param_0.timeZone)
post	possibly_updated(Param_0.userName)
unanalyzed	call on java.util.Date:clone

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

method	void pcCopyKeyFieldsFromObjectId(Object)
pre	Param_1 != null
post	init'ed(Param_0.id)

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)

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

method	void org.apache.roller.weblogger.pojos.User()
presumption	init'ed(java.lang.Boolean.TRUE)
post	this.enabled == java.lang.Boolean.TRUE
post	(soft) init'ed(this.enabled)
post	init'ed(this.id)
post	this.permissions == &new ArrayList(User#2)
post	this.roles == &new HashSet(User#1)
post	new ArrayList(User#2) num objects == 1
post	new HashSet(User#1) num objects == 1

method	void org.apache.roller.weblogger.pojos. User(String, String, String, String, String, String, String, Date, Boolean)
pre	dateCreated != null
presumption	init'ed(java.lang.Boolean.TRUE)
post	this.dateCreated != null
post	this.emailAddress == emailAddress
post	init'ed(this.emailAddress)
post	this.enabled == isEnabled
post	init'ed(this.enabled)
post	this.fullName == fullName
post	init'ed(this.fullName)
post	init'ed(this.id)
post	this.locale == locale
post	init'ed(this.locale)
post	this.password == password
post	init'ed(this.password)
post	this.permissions == &new ArrayList(User#2)
post	this.roles == &new HashSet(User#1)
post	this.timeZone == timeZone
post	init'ed(this.timeZone)
post	this.userName == userName
post	init'ed(this.userName)
post	new ArrayList(User#2) num objects == 1
post	new HashSet(User#1) num objects == 1

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 == Param_1
post	init'ed(this.id)

method	String pcgetUserName()
pre	init'ed(this.userName)
post	return_value == this.userName
post	init'ed(return_value)

method	void pcsetUserName(String)
post	this.userName == Param_1
post	init'ed(this.userName)

method	String pcgetPassword()
pre	init'ed(this.password)
post	return_value == this.password
post	init'ed(return_value)

method	void pcsetPassword(String)
post	this.password == Param_1
post	init'ed(this.password)

method	void resetPassword(String)
pre	init'ed(this.pcStateManager)
pre	(soft) init'ed(this.password)
pre	(soft) pcInheritedFieldCount <= 2³²-8
post	init'ed(this.password)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:set tingStringField
test_vector	java.lang.Boolean:booleanValue(...)@137: {0}, {1}

info method not available -- call on String org.apache.roller.weblogger. config.WebloggerConfig:getProperty(String)

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

method	String pcgetScreenName()
pre	init'ed(this.screenName)
post	return_value == this.screenName
post	init'ed(return_value)

method	void pcsetScreenName(String)
post	this.screenName == Param_1
post	init'ed(this.screenName)

method	String pcgetFullName()
pre	init'ed(this.fullName)
post	return_value == this.fullName
post	init'ed(return_value)

method	void pcsetFullName(String)
post	this.fullName == Param_1
post	init'ed(this.fullName)

method	String pcgetEmailAddress()
pre	init'ed(this.emailAddress)
post	return_value == this.emailAddress
post	init'ed(return_value)

method	void pcsetEmailAddress(String)
post	this.emailAddress == Param_1
post	init'ed(this.emailAddress)

method	Date pcgetDateCreated()
pre	init'ed(this.dateCreated)
post	init'ed(return_value)
test_vector	this.dateCreated: Inverse{null}, Addr_Set{null}

method	void pcsetDateCreated(Date)
post	init'ed(this.dateCreated)
test_vector	Param_1: Addr_Set{null}, Inverse{null}

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

method	void pcsetTimeZone(String)
post	this.timeZone == Param_1
post	init'ed(this.timeZone)

method	Boolean pcgetEnabled()
pre	init'ed(this.enabled)
post	return_value == this.enabled
post	init'ed(return_value)

method	void pcsetEnabled(Boolean)
post	this.enabled == Param_1
post	init'ed(this.enabled)

method	String pcgetActivationCode()
pre	init'ed(this.activationCode)
post	return_value == this.activationCode
post	init'ed(return_value)

method	void pcsetActivationCode(String)
post	this.activationCode == Param_1
post	init'ed(this.activationCode)

method	List pcgetPermissions()
pre	init'ed(this.permissions)
post	return_value == this.permissions
post	init'ed(return_value)

method	void pcsetPermissions(List)
post	this.permissions == Param_1
post	init'ed(this.permissions)

method	Set pcgetRoles()
pre	init'ed(this.roles)
post	return_value == this.roles
post	init'ed(return_value)

method	void pcsetRoles(Set)
post	this.roles == Param_1
post	init'ed(this.roles)

method	bool hasRole(String)
pre	init'ed(this.pcStateManager)
pre	this.roles != null
pre	(soft) org/apache/roller/weblogger/pojos/UserRole. pcInheritedFieldCount <= 2³²-2
pre	(soft) pcInheritedFieldCount <= 2³²-10
presumption	java.util.Iterator:next(...)@307 != null
presumption	role.role@307 != null
post	init'ed(return_value)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
test_vector	java.lang.String:equals(...)@308: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@306: {0}, {1}

method	void grantRole(String)
pre	(soft) org/apache/roller/weblogger/pojos/UserRole. pcInheritedFieldCount <= 2³²-3
pre	(soft) pcInheritedFieldCount <= 2³²-13
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) this.roles != null
pre	(soft) init'ed(this.userName)
unanalyzed	call on org.apache.openjpa.enhance.StateManager:acc essingField
unanalyzed	call on getUserName
unanalyzed	call on org.apache.roller.util.UUIDGenerator:genera teUUID
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	String toString()
pre	init'ed(this.dateCreated)
pre	init'ed(this.emailAddress)
pre	init'ed(this.enabled)
pre	init'ed(this.fullName)
pre	init'ed(this.id)
pre	init'ed(this.userName)
post	java.lang.StringBuffer:toString(...)._tainted == this.emailAddress._tainted \| this.fullName._ tainted \| this.id._tainted \| this.userName. _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.pcStateManager)
pre	(soft) init'ed(other.userName)
pre	(soft) pcInheritedFieldCount <= 2³²-13
pre	(soft) init'ed(this.pcStateManager)
pre	(soft) init'ed(this.userName)
presumption	org.apache.commons.lang.builder.EqualsBuilder:appen d(...)@347 != 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.pcStateManager)
pre	init'ed(this.userName)
pre	(soft) pcInheritedFieldCount <= 2³²-13
presumption	org.apache.commons.lang.builder.HashCodeBuilder:app end(...)@351 != 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()

Prev Msg Next Msg

+

click for all messages in this file low

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

+

low

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

+

click for all messages in this file low

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

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: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: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. PCRegistry:register(Class, String[], Class[], byte[], Class, String, PersistenceCapable)

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

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

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

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

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 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()