Last Msg First Msg
























method String getId()
preinit'ed(Param_0.id)
preinit'ed(Param_0.pcStateManager)
pre(soft) init'ed(pcInheritedFieldCount)
postreturn_value == Param_0.id
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method void setId(String)
preinit'ed(Param_0.pcStateManager)
pre(soft) init'ed(Param_0.id)
pre(soft) init'ed(pcInheritedFieldCount)
postParam_0.id == One-of{old Param_0.id, Param_1}
post(soft) init'ed(Param_0.id)
unanalyzedcall on java.lang.String:trim
unanalyzedcall on java.lang.String:length
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method Weblog getWebsite()
preinit'ed(Param_0.pcStateManager)
preinit'ed(Param_0.website)
pre(soft) pcInheritedFieldCount <= 232-5
postreturn_value == Param_0.website
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method void setWebsite(Weblog)
preinit'ed(Param_0.pcStateManager)
pre(soft) init'ed(Param_0.website)
pre(soft) pcInheritedFieldCount <= 232-5
postParam_0.website == One-of{Param_1, old Param_0.website}
post(soft) init'ed(Param_0.website)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method User getUser()
preinit'ed(Param_0.pcStateManager)
preinit'ed(Param_0.user)
pre(soft) pcInheritedFieldCount <= 232-4
postreturn_value == Param_0.user
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method void setUser(User)
preinit'ed(Param_0.pcStateManager)
pre(soft) init'ed(Param_0.user)
pre(soft) pcInheritedFieldCount <= 232-4
postParam_0.user == One-of{Param_1, old Param_0.user}
post(soft) init'ed(Param_0.user)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method short getPermissionMask()
preinit'ed(Param_0.pcStateManager)
preinit'ed(Param_0.permissionMask)
pre(soft) pcInheritedFieldCount <= 232-3
postreturn_value == Param_0.permissionMask
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method void setPermissionMask(short)
preinit'ed(Param_0.pcStateManager)
pre(soft) init'ed(Param_0.permissionMask)
pre(soft) pcInheritedFieldCount <= 232-3
postParam_0.permissionMask == One-of{Param_1, old Param_0.permissionMask}
post(soft) init'ed(Param_0.permissionMask)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method bool isPending()
preinit'ed(Param_0.pcStateManager)
preinit'ed(Param_0.pending)
pre(soft) pcInheritedFieldCount <= 232-2
postreturn_value == Param_0.pending
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method void setPending(bool)
preinit'ed(Param_0.pcStateManager)
pre(soft) init'ed(Param_0.pending)
pre(soft) pcInheritedFieldCount <= 232-2
post(soft) init'ed(Param_0.pending)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method int pcGetEnhancementContractVersion()
postreturn_value == 2

method void pcClearFields()
postParam_0.id == null
postParam_0.user == null
postParam_0.website == null
postParam_0.pending == 0
postParam_0.permissionMask == 0
unanalyzedcall on java.lang.String:trim
unanalyzedcall on java.lang.String:length

method PersistenceCapable pcNewInstance(StateManager, Object, bool)
preinit'ed(LIMITED)
preParam_2 != null
postreturn_value == &new WeblogPermission(pcNewInst ance#1)
postnew WeblogPermission(pcNewInstance#1) num objects == 1
postinit'ed(return_value.id)
postreturn_value.pcStateManager == Param_1
postinit'ed(return_value.pcStateManager)
postinit'ed(return_value.pending)
postreturn_value.permissionMask == One-of{LIMITED, 0}
postinit'ed(return_value.permissionMask)
postreturn_value.user == null
postreturn_value.website == null
unanalyzedcall on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzedcall on java.lang.String:trim
unanalyzedcall on java.lang.String:length
unanalyzedcall on org.apache.openjpa.util.StringId:getId
test_vectorParam_3: {0}, {1}

method PersistenceCapable pcNewInstance(StateManager, bool)
preinit'ed(LIMITED)
postreturn_value == &new WeblogPermission(pcNewInst ance#1)
postnew WeblogPermission(pcNewInstance#1) num objects == 1
postinit'ed(return_value.id)
postreturn_value.pcStateManager == Param_1
postinit'ed(return_value.pcStateManager)
postinit'ed(return_value.pending)
postreturn_value.permissionMask == One-of{LIMITED, 0}
postinit'ed(return_value.permissionMask)
postreturn_value.user == null
postreturn_value.website == null
unanalyzedcall on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzedcall on java.lang.String:trim
unanalyzedcall on java.lang.String:length
test_vectorParam_2: {0}, {1}

method int pcGetManagedFieldCount()
postreturn_value == 5

method void pcReplaceField(int)
preParam_0.pcStateManager != null
preParam_1 - pcInheritedFieldCount in 0..4
preinit'ed(pcInheritedFieldCount)
postpossibly_updated(Param_0.id)
postpossibly_updated(Param_0.pending)
postpossibly_updated(Param_0.permissionMask)
postpossibly_updated(Param_0.user)
postpossibly_updated(Param_0.website)
unanalyzedcall on java.lang.String:trim
unanalyzedcall on java.lang.String:length
test_vectorParam_1 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}

method void pcReplaceFields(int[])
preParam_1 != null
preParam_1.length <= 232-1
pre(soft) Param_0.pcStateManager != null
pre(soft) init'ed(Param_1[...])
pre(soft) init'ed(pcInheritedFieldCount)
postpossibly_updated(Param_0.id)
postpossibly_updated(Param_0.pending)
postpossibly_updated(Param_0.permissionMask)
postpossibly_updated(Param_0.user)
postpossibly_updated(Param_0.website)
unanalyzedcall on java.lang.String:trim
unanalyzedcall on java.lang.String:length
unanalyzedcall on org.apache.openjpa.enhance.StateManager:rep laceStringField
unanalyzedcall on org.apache.openjpa.enhance.StateManager:rep laceBooleanField
unanalyzedcall on org.apache.openjpa.enhance.StateManager:rep laceShortField
unanalyzedcall on org.apache.openjpa.enhance.StateManager:rep laceObjectField

method void pcProvideField(int)
preParam_0.pcStateManager != null
preParam_1 - pcInheritedFieldCount in 0..4
preinit'ed(pcInheritedFieldCount)
pre(soft) init'ed(Param_0.id)
pre(soft) init'ed(Param_0.pending)
pre(soft) init'ed(Param_0.permissionMask)
pre(soft) init'ed(Param_0.user)
pre(soft) init'ed(Param_0.website)
test_vectorParam_1 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}

method void pcProvideFields(int[])
preParam_1 != null
preParam_1.length <= 232-1
pre(soft) init'ed(Param_0.id)
pre(soft) Param_0.pcStateManager != null
pre(soft) init'ed(Param_0.pending)
pre(soft) init'ed(Param_0.permissionMask)
pre(soft) init'ed(Param_0.user)
pre(soft) init'ed(Param_0.website)
pre(soft) init'ed(Param_1[...])
pre(soft) init'ed(pcInheritedFieldCount)
unanalyzedcall on org.apache.openjpa.enhance.StateManager:pro videdStringField
unanalyzedcall on org.apache.openjpa.enhance.StateManager:pro videdBooleanField
unanalyzedcall on org.apache.openjpa.enhance.StateManager:pro videdShortField
unanalyzedcall on org.apache.openjpa.enhance.StateManager:pro videdObjectField

method void pcCopyField(WeblogPermission, int)
preParam_1 != null
preParam_2 - pcInheritedFieldCount in 0..4
preinit'ed(pcInheritedFieldCount)
pre(soft) init'ed(Param_1.id)
pre(soft) init'ed(Param_1.pending)
pre(soft) init'ed(Param_1.permissionMask)
pre(soft) init'ed(Param_1.user)
pre(soft) init'ed(Param_1.website)
postParam_0.id == One-of{old Param_0.id, Param_1.id}
postpossibly_updated(Param_0.pending)
postParam_0.permissionMask == One-of{old Param_0.permissionMask, Param_1.permissionMask}
postParam_0.user == One-of{old Param_0.user, Param_1.user}
postParam_0.website == One-of{old Param_0.website, Param_1.website}
unanalyzedcall on java.lang.String:trim
unanalyzedcall on java.lang.String:length
test_vectorParam_2 - pcInheritedFieldCount: {0}, {1}, {2}, {3}, {4}

method void pcCopyFields(Object, int[])
preParam_0.pcStateManager != null
preParam_0.pcStateManager == Param_1.pcStateManager
preParam_1 != null
preParam_1.pcStateManager != null
preParam_2 != null
preParam_2.length <= 232-1
pre(soft) init'ed(Param_1.id)
pre(soft) init'ed(Param_1.pending)
pre(soft) init'ed(Param_1.permissionMask)
pre(soft) init'ed(Param_1.user)
pre(soft) init'ed(Param_1.website)
pre(soft) init'ed(Param_2[...])
pre(soft) init'ed(pcInheritedFieldCount)
postpossibly_updated(Param_0.id)
postpossibly_updated(Param_0.pending)
postpossibly_updated(Param_0.permissionMask)
postpossibly_updated(Param_0.user)
postpossibly_updated(Param_0.website)
unanalyzedcall on java.lang.String:trim
unanalyzedcall on java.lang.String:length

method Object pcGetGenericContext()
preinit'ed(Param_0.pcStateManager)
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method Object pcFetchObjectId()
preinit'ed(Param_0.pcStateManager)
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method bool pcIsDeleted()
preinit'ed(Param_0.pcStateManager)
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method bool pcIsDirty()
preinit'ed(Param_0.pcStateManager)
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method bool pcIsNew()
preinit'ed(Param_0.pcStateManager)
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method bool pcIsPersistent()
preinit'ed(Param_0.pcStateManager)
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method bool pcIsTransactional()
preinit'ed(Param_0.pcStateManager)
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method bool pcSerializing()
preinit'ed(Param_0.pcStateManager)
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method void pcDirty(String)
preinit'ed(Param_0.pcStateManager)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method StateManager pcGetStateManager()
preinit'ed(Param_0.pcStateManager)
postreturn_value == Param_0.pcStateManager
postinit'ed(return_value)

method Object pcGetVersion()
preinit'ed(Param_0.pcStateManager)
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method void pcReplaceStateManager(StateManager)
preinit'ed(Param_0.pcStateManager)
postinit'ed(Param_0.pcStateManager)
test_vectorParam_0.pcStateManager: Addr_Set{null}, Inverse{null}

method void pcCopyKeyFieldsToObjectId(FieldSupplier, Object)

method void pcCopyKeyFieldsToObjectId(Object)

method void pcCopyKeyFieldsFromObjectId(FieldConsumer, Object)
preParam_1 != null
preParam_2 != null
preinit'ed(pcInheritedFieldCount)

method void pcCopyKeyFieldsFromObjectId(Object)
preParam_1 != null
postpossibly_updated(Param_0.id)
unanalyzedcall on java.lang.String:trim
unanalyzedcall on java.lang.String:length

method Object pcNewObjectIdInstance(Object)
postreturn_value == &new StringId(pcNewObjectIdInst ance#1)
postnew StringId(pcNewObjectIdInstance#1) num objects == 1
unanalyzedcall on java.lang.Class:forName
unanalyzedcall on java.lang.Throwable:__curr_excep_obj
unanalyzedcall on java.lang.Throwable:getMessage
unanalyzedcall on java.lang.NoClassDefFoundError

method Object pcNewObjectIdInstance()
preinit'ed(Param_0.id)
postreturn_value == &new StringId(pcNewObjectIdInst ance#1)
postnew StringId(pcNewObjectIdInstance#1) num objects == 1
unanalyzedcall on java.lang.Class:forName
unanalyzedcall on java.lang.Throwable:__curr_excep_obj
unanalyzedcall on java.lang.Throwable:getMessage
unanalyzedcall on java.lang.NoClassDefFoundError

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

method Object pcGetDetachedState()
preinit'ed(Param_0.pcDetachedState)
postreturn_value == Param_0.pcDetachedState
postinit'ed(return_value)

method void pcSetDetachedState(Object)
postParam_0.pcDetachedState == Param_1
postinit'ed(Param_0.pcDetachedState)









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











method org.apache.roller.weblogger.pojos.WeblogPermission __static_init
presumptioninit'ed(java.lang.Boolean.TYPE)
presumptioninit'ed(java.lang.Short.TYPE)
postADMIN == 3
postAUTHOR == 1
postnew Class[](WeblogPermission__static_init#2) num objects == 1
postnew String[](WeblogPermission__static_init#1) num objects == 1
postnew byte[](WeblogPermission__static_init#3) num objects == 1
postLIMITED == 0
postpcFieldFlags == &new byte[](WeblogPermission__ static_init#3)
postpcFieldNames == &new String[](WeblogPermission_ _static_init#1)
postpcFieldTypes == &new Class[](WeblogPermission__ static_init#2)
postpcFieldTypes.length == 5
postpcFieldNames.length == 5
postpcFieldFlags.length == 5
postpcFieldTypes[1] == java.lang.Boolean.TYPE
post(soft) init'ed(pcFieldTypes[1])
postpcFieldTypes[2] == java.lang.Short.TYPE
post(soft) init'ed(pcFieldTypes[2])
postpcFieldNames[0] == &"id"
postpcFieldNames[1] == &"pending"
postpcFieldNames[2] == &"permissionMask"
postpcFieldNames[3] == &"user"
postpcFieldNames[4] == &"website"
postpcFieldFlags[0] == 26
postpcFieldFlags[1] == 26
postpcFieldFlags[2] == 26
postpcFieldFlags[3] == 26
postpcFieldFlags[4] == 26
unanalyzedcall on java.lang.Class:forName
unanalyzedcall on java.lang.Throwable:__curr_excep_obj
unanalyzedcall on java.lang.Throwable:getMessage
unanalyzedcall on java.lang.NoClassDefFoundError
unanalyzedcall on org.apache.roller.util.UUIDGenerator:genera teUUID









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











method void org.apache.roller.weblogger.pojos. WeblogPermission()
preinit'ed(LIMITED)
postinit'ed(this.id)
postthis.pending == 1
postthis.permissionMask == LIMITED
postinit'ed(this.permissionMask)
postthis.user == null
postthis.website == null










method bool has(short)
preinit'ed(this.pcStateManager)
preinit'ed(this.permissionMask)
pre(soft) pcInheritedFieldCount <= 232-3
postinit'ed(return_value)
unanalyzedcall on org.apache.openjpa.enhance.StateManager:acc essingField










method String pcgetId()
preinit'ed(this.id)
postreturn_value == this.id
postinit'ed(return_value)










method void pcsetId(String)
postthis.id == One-of{old this.id, Param_1}
test_vectorParam_1: Addr_Set{null}, Inverse{null}
test_vectorjava.lang.String:length(...)@69: {1.. 232-1}, {0}










method Weblog pcgetWebsite()
preinit'ed(this.website)
postreturn_value == this.website
postinit'ed(return_value)










method void pcsetWebsite(Weblog)
postthis.website == Param_1
postinit'ed(this.website)










method User pcgetUser()
preinit'ed(this.user)
postreturn_value == this.user
postinit'ed(return_value)










method void pcsetUser(User)
postthis.user == Param_1
postinit'ed(this.user)










method short pcgetPermissionMask()
preinit'ed(this.permissionMask)
postreturn_value == this.permissionMask
postinit'ed(return_value)










method void pcsetPermissionMask(short)
postthis.permissionMask == Param_1
postinit'ed(this.permissionMask)










method bool pcisPending()
preinit'ed(this.pending)
postreturn_value == this.pending
postinit'ed(return_value)










method void pcsetPending(bool)
postthis.pending == Param_1
postinit'ed(this.pending)










method String toString()
preinit'ed(this.id)
preinit'ed(this.pending)
preinit'ed(this.permissionMask)
postjava.lang.StringBuffer:toString(...)._tainted == this.id._tainted
postinit'ed(java.lang.StringBuffer:toString(...)._ tainted)
postreturn_value == &java.lang.StringBuffer:toStrin g(...)










method bool equals(Object)
pre(soft) init'ed(other.user)
pre(soft) init'ed(other.website)
pre(soft) init'ed(this.user)
pre(soft) init'ed(this.website)
presumptionorg.apache.commons.lang.builder.EqualsBuilder:appen d(...)@140 != null
postinit'ed(return_value)
test_vectorother == this: {0}, {1}









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











method int hashCode()
preinit'ed(this.user)
preinit'ed(this.website)
presumptionorg.apache.commons.lang.builder.HashCodeBuilder:app end(...)@147 != null
postinit'ed(return_value)









  infomethod not available-- call on void org.apache.commons.lang.builder. HashCodeBuilder()
  infomethod not available-- call on HashCodeBuilder org.apache.commons.lang. builder.HashCodeBuilder:append(Object)
  infomethod not available-- call on int org.apache.commons.lang.builder. HashCodeBuilder:toHashCode()










Prev Msg Next Msg
+
low
precondition failureorg/apache/roller/weblogger/pojos/WeblogPermission. pcReplaceField: Param_1 - pcInheritedFieldCount in 0..4
+
low
precondition failureorg/apache/roller/weblogger/pojos/WeblogPermission. pcProvideField: Param_1 - pcInheritedFieldCount in 0..4
+
low
precondition failureorg/apache/roller/weblogger/pojos/WeblogPermission. pcCopyField: Param_2 - pcInheritedFieldCount in 0..4
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:settingStringField(PersistenceCapable, int, String, String, int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:settingObjectField(PersistenceCapable, int, Object, Object, int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:settingShortField(PersistenceCapable, int, short, short, int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:accessingField(int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:settingBooleanField(PersistenceCapable , int, bool, bool, int)
  infomethod not available-- call on String org.apache.openjpa.enhance. StateManager:replaceStringField(PersistenceCapable, int)
  infomethod not available-- call on bool org.apache.openjpa.enhance. StateManager:replaceBooleanField(PersistenceCapable , int)
  infomethod not available-- call on short org.apache.openjpa.enhance. StateManager:replaceShortField(PersistenceCapable, int)
  infomethod not available-- call on Object org.apache.openjpa.enhance. StateManager:replaceObjectField(PersistenceCapable, int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:providedStringField(PersistenceCapable , int, String)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:providedBooleanField(PersistenceCapabl e, int, bool)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:providedShortField(PersistenceCapable, int, short)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:providedObjectField(PersistenceCapable , int, Object)
  infomethod not available-- call on Object org.apache.openjpa.enhance. StateManager:getGenericContext()
  infomethod not available-- call on Object org.apache.openjpa.enhance. StateManager:fetchObjectId()
  infomethod not available-- call on bool org.apache.openjpa.enhance. StateManager:isDeleted()
  infomethod not available-- call on bool org.apache.openjpa.enhance. StateManager:isDirty()
  infomethod not available-- call on bool org.apache.openjpa.enhance. StateManager:isNew()
  infomethod not available-- call on bool org.apache.openjpa.enhance. StateManager:isPersistent()
  infomethod not available-- call on bool org.apache.openjpa.enhance. StateManager:isTransactional()
  infomethod not available-- call on bool org.apache.openjpa.enhance. StateManager:serializing()
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:dirty(String)
  infomethod not available-- call on Object org.apache.openjpa.enhance. StateManager:getVersion()
  infomethod not available-- call on StateManager org.apache.openjpa.enhance. StateManager:replaceStateManager(StateManager)
  infomethod not available-- call on String org.apache.openjpa.util. StringId:getId()
  infomethod not available-- call on void org.apache.openjpa.enhance. FieldConsumer:storeStringField(int, String)
  infomethod not available-- call on String org.apache.openjpa.util. StringId:getId()
  infomethod not available-- call on void org.apache.openjpa.util. StringId(Class, String)
  infomethod not available-- call on bool org.apache.openjpa.enhance. StateManager:isDetached()
Prev Msg Next Msg