Last Msg First Msg
























method String getId()
preinit'ed(Param_0.id)
preinit'ed(Param_0.pcStateManager)
pre(soft) pcInheritedFieldCount <= 232-3
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) pcInheritedFieldCount <= 232-3
postParam_0.id == One-of{Param_1, old Param_0.id}
post(soft) init'ed(Param_0.id)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

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

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

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

method void setPingTarget(PingTarget)
preinit'ed(Param_0.pcStateManager)
pre(soft) init'ed(Param_0.pingTarget)
pre(soft) pcInheritedFieldCount <= 232-4
postParam_0.pingTarget == One-of{Param_1, old Param_0.pingTarget}
post(soft) init'ed(Param_0.pingTarget)
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 int getAttempts()
preinit'ed(Param_0.attempts)
preinit'ed(Param_0.pcStateManager)
pre(soft) init'ed(pcInheritedFieldCount)
postreturn_value == Param_0.attempts
postinit'ed(return_value)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method void setAttempts(int)
preinit'ed(Param_0.pcStateManager)
pre(soft) init'ed(Param_0.attempts)
pre(soft) init'ed(pcInheritedFieldCount)
postParam_0.attempts == One-of{Param_1, old Param_0.attempts}
post(soft) init'ed(Param_0.attempts)
test_vectorParam_0.pcStateManager: Inverse{null}, Addr_Set{null}

method int pcGetEnhancementContractVersion()
postreturn_value == 2

method org.apache.roller.weblogger.pojos.PingQueueEntry__ static_init
presumptioninit'ed(java.lang.Integer.TYPE)
postpcFieldFlags == &new byte[](PingQueueEntry__ static_init#3)
postpcFieldNames == &new String[](PingQueueEntry__ static_init#1)
postpcFieldTypes == &new Class[](PingQueueEntry__ static_init#2)
postnew Class[](PingQueueEntry__static_init#2) num objects == 1
postnew String[](PingQueueEntry__static_init#1) num objects == 1
postnew byte[](PingQueueEntry__static_init#3) num objects == 1
postpcFieldTypes.length == 5
postpcFieldNames.length == 5
postpcFieldFlags.length == 5
postpcFieldTypes[0] == java.lang.Integer.TYPE
post(soft) init'ed(pcFieldTypes[0])
postpcFieldNames[0] == &"attempts"
postpcFieldNames[1] == &"entryTime"
postpcFieldNames[2] == &"id"
postpcFieldNames[3] == &"pingTarget"
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

method void pcClearFields()
postParam_0.attempts == 0
postParam_0.entryTime == null
postParam_0.id == null
postParam_0.pingTarget == null
postParam_0.website == null

method PersistenceCapable pcNewInstance(StateManager, Object, bool)
preParam_2 != null
postreturn_value == &new PingQueueEntry(pcNewInstan ce#1)
postnew PingQueueEntry(pcNewInstance#1) num objects == 1
postreturn_value.attempts == 0
postreturn_value.entryTime == null
postinit'ed(return_value.id)
postreturn_value.pcStateManager == Param_1
postinit'ed(return_value.pcStateManager)
postreturn_value.pingTarget == null
postreturn_value.website == null
unanalyzedcall on org.apache.roller.util.UUIDGenerator:genera teUUID
unanalyzedcall on org.apache.openjpa.util.StringId:getId
test_vectorParam_3: {0}, {1}

method PersistenceCapable pcNewInstance(StateManager, bool)
postreturn_value == &new PingQueueEntry(pcNewInstan ce#1)
postnew PingQueueEntry(pcNewInstance#1) num objects == 1
postreturn_value.attempts == 0
postreturn_value.entryTime == null
postinit'ed(return_value.id)
postreturn_value.pcStateManager == Param_1
postinit'ed(return_value.pcStateManager)
postreturn_value.pingTarget == null
postreturn_value.website == null
unanalyzedcall on org.apache.roller.util.UUIDGenerator:genera teUUID
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.attempts)
postpossibly_updated(Param_0.entryTime)
postpossibly_updated(Param_0.id)
postpossibly_updated(Param_0.pingTarget)
postpossibly_updated(Param_0.website)
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.attempts)
postpossibly_updated(Param_0.entryTime)
postpossibly_updated(Param_0.id)
postpossibly_updated(Param_0.pingTarget)
postpossibly_updated(Param_0.website)
unanalyzedcall on org.apache.openjpa.enhance.StateManager:rep laceIntField
unanalyzedcall on org.apache.openjpa.enhance.StateManager:rep laceObjectField
unanalyzedcall on org.apache.openjpa.enhance.StateManager:rep laceStringField

method void pcProvideField(int)
preParam_0.pcStateManager != null
preParam_1 - pcInheritedFieldCount in 0..4
preinit'ed(pcInheritedFieldCount)
pre(soft) init'ed(Param_0.attempts)
pre(soft) init'ed(Param_0.entryTime)
pre(soft) init'ed(Param_0.id)
pre(soft) init'ed(Param_0.pingTarget)
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.attempts)
pre(soft) init'ed(Param_0.entryTime)
pre(soft) init'ed(Param_0.id)
pre(soft) Param_0.pcStateManager != null
pre(soft) init'ed(Param_0.pingTarget)
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 videdIntField
unanalyzedcall on org.apache.openjpa.enhance.StateManager:pro videdObjectField
unanalyzedcall on org.apache.openjpa.enhance.StateManager:pro videdStringField

method void pcCopyField(PingQueueEntry, int)
preParam_1 != null
preParam_2 - pcInheritedFieldCount in 0..4
preinit'ed(pcInheritedFieldCount)
pre(soft) init'ed(Param_1.attempts)
pre(soft) init'ed(Param_1.entryTime)
pre(soft) init'ed(Param_1.id)
pre(soft) init'ed(Param_1.pingTarget)
pre(soft) init'ed(Param_1.website)
postParam_0.attempts == One-of{Param_1.attempts, old Param_0.attempts}
postParam_0.entryTime == One-of{old Param_0.entryTime, Param_1.entryTime}
postParam_0.id == One-of{old Param_0.id, Param_1.id}
postParam_0.pingTarget == One-of{old Param_0. pingTarget, Param_1.pingTarget}
postParam_0.website == One-of{old Param_0.website, Param_1.website}
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.attempts)
pre(soft) init'ed(Param_1.entryTime)
pre(soft) init'ed(Param_1.id)
pre(soft) init'ed(Param_1.pingTarget)
pre(soft) init'ed(Param_1.website)
pre(soft) init'ed(Param_2[...])
pre(soft) init'ed(pcInheritedFieldCount)
postpossibly_updated(Param_0.attempts)
postpossibly_updated(Param_0.entryTime)
postpossibly_updated(Param_0.id)
postpossibly_updated(Param_0.pingTarget)
postpossibly_updated(Param_0.website)

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
prepcInheritedFieldCount <= 232-3

method void pcCopyKeyFieldsFromObjectId(Object)
preParam_1 != null
postinit'ed(Param_0.id)

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, null}
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)

method void writeObject(ObjectOutputStream)
preinit'ed(Param_0.pcStateManager)
preParam_1 != null
postParam_0.pcDetachedState == One-of{old Param_0.pcDetachedState, null}
unanalyzedcall on org.apache.openjpa.enhance.StateManager:ser ializing

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









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











method void org.apache.roller.weblogger.pojos. PingQueueEntry()
postthis.attempts == 0
postthis.entryTime == null
postthis.pingTarget == null
postthis.website == null
postinit'ed(this.id)










method void org.apache.roller.weblogger.pojos. PingQueueEntry(String, Timestamp, PingTarget, Weblog, int)
postthis.attempts == attempts
postinit'ed(this.attempts)
postthis.entryTime == entryTime
postinit'ed(this.entryTime)
postinit'ed(this.id)
postthis.pingTarget == pingTarget
postinit'ed(this.pingTarget)
postthis.website == website
postinit'ed(this.website)










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










method void pcsetId(String)
postthis.id == Param_1
postinit'ed(this.id)










method Timestamp pcgetEntryTime()
preinit'ed(this.entryTime)
postreturn_value == this.entryTime
postinit'ed(return_value)










method void pcsetEntryTime(Timestamp)
postthis.entryTime == Param_1
postinit'ed(this.entryTime)










method PingTarget pcgetPingTarget()
preinit'ed(this.pingTarget)
postreturn_value == this.pingTarget
postinit'ed(return_value)










method void pcsetPingTarget(PingTarget)
postthis.pingTarget == Param_1
postinit'ed(this.pingTarget)










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 int pcgetAttempts()
preinit'ed(this.attempts)
postreturn_value == this.attempts
postinit'ed(return_value)










method void pcsetAttempts(int)
postthis.attempts == Param_1
postinit'ed(this.attempts)










method int incrementAttempts()
prethis.attempts <= 232-2
postreturn_value == old this.attempts + 1
postreturn_value >= -231+1
postthis.attempts == return_value










method String toString()
preinit'ed(this.attempts)
preinit'ed(this.entryTime)
preinit'ed(this.id)
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.entryTime)
pre(soft) init'ed(other.pcStateManager)
pre(soft) init'ed(other.website)
pre(soft) pcInheritedFieldCount <= 232-5
pre(soft) init'ed(this.entryTime)
pre(soft) init'ed(this.pcStateManager)
pre(soft) init'ed(this.website)
presumptionorg.apache.commons.lang.builder.EqualsBuilder:appen d(...)@184 != null
postinit'ed(return_value)
unanalyzedcall on org.apache.openjpa.enhance.StateManager:acc essingField
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.entryTime)
preinit'ed(this.pcStateManager)
preinit'ed(this.website)
pre(soft) pcInheritedFieldCount <= 232-5
presumptionorg.apache.commons.lang.builder.HashCodeBuilder:app end(...)@191 != null
postinit'ed(return_value)
unanalyzedcall on org.apache.openjpa.enhance.StateManager:acc essingField









  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/PingQueueEntry. pcReplaceField: Param_1 - pcInheritedFieldCount in 0..4
+
low
precondition failureorg/apache/roller/weblogger/pojos/PingQueueEntry. pcProvideField: Param_1 - pcInheritedFieldCount in 0..4
+
low
precondition failureorg/apache/roller/weblogger/pojos/PingQueueEntry. 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: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:settingIntField(PersistenceCapable, int, int, int, int)
  infomethod not available-- call on void org.apache.openjpa.enhance. PCRegistry:register(Class, String[], Class[], byte[], Class, String, PersistenceCapable)
  infomethod not available-- call on int org.apache.openjpa.enhance. StateManager:replaceIntField(PersistenceCapable, int)
  infomethod not available-- call on Object org.apache.openjpa.enhance. StateManager:replaceObjectField(PersistenceCapable, int)
  infomethod not available-- call on String org.apache.openjpa.enhance. StateManager:replaceStringField(PersistenceCapable, int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:providedIntField(PersistenceCapable, int, int)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:providedObjectField(PersistenceCapable , int, Object)
  infomethod not available-- call on void org.apache.openjpa.enhance. StateManager:providedStringField(PersistenceCapable , int, String)
  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