| method | PersistenceCapable pcNewInstance(StateManager, Object, bool) |
| pre | init'ed(LIMITED) |
| pre | Param_2 != null |
| post | return_value == &new WeblogPermission(pcNewInst ance#1) |
| post | new WeblogPermission(pcNewInstance#1) num objects == 1 |
| post | init'ed(return_value.id) |
| post | return_value.pcStateManager == Param_1 |
| post | init'ed(return_value.pcStateManager) |
| post | init'ed(return_value.pending) |
| post | return_value.permissionMask == One-of{LIMITED, 0} |
| post | init'ed(return_value.permissionMask) |
| post | return_value.user == null |
| post | return_value.website == null |
| unanalyzed | call on org.apache.roller.util.UUIDGenerator:genera teUUID |
| 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) |
| pre | init'ed(LIMITED) |
| post | return_value == &new WeblogPermission(pcNewInst ance#1) |
| post | new WeblogPermission(pcNewInstance#1) num objects == 1 |
| post | init'ed(return_value.id) |
| post | return_value.pcStateManager == Param_1 |
| post | init'ed(return_value.pcStateManager) |
| post | init'ed(return_value.pending) |
| post | return_value.permissionMask == One-of{LIMITED, 0} |
| post | init'ed(return_value.permissionMask) |
| post | return_value.user == null |
| post | return_value.website == null |
| unanalyzed | call on org.apache.roller.util.UUIDGenerator:genera teUUID |
| unanalyzed | call on java.lang.String:trim |
| unanalyzed | call on java.lang.String:length |
| test_vector | Param_2: {0}, {1} |
| method | void pcReplaceField(int) |
| pre | Param_0.pcStateManager != null |
| pre | Param_1 - pcInheritedFieldCount in 0..4 |
| pre | init'ed(pcInheritedFieldCount) |
| post | possibly_updated(Param_0.id) |
| post | possibly_updated(Param_0.pending) |
| post | possibly_updated(Param_0.permissionMask) |
| post | possibly_updated(Param_0.user) |
| 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} |
| method | void pcReplaceFields(int[]) |
| pre | Param_1 != null |
| pre | Param_1.length <= 232-1 |
| pre | (soft) Param_0.pcStateManager != null |
| pre | (soft) init'ed(Param_1[...]) |
| pre | (soft) init'ed(pcInheritedFieldCount) |
| post | possibly_updated(Param_0.id) |
| post | possibly_updated(Param_0.pending) |
| post | possibly_updated(Param_0.permissionMask) |
| post | possibly_updated(Param_0.user) |
| 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 laceStringField |
| unanalyzed | call on org.apache.openjpa.enhance.StateManager:rep laceBooleanField |
| unanalyzed | call on org.apache.openjpa.enhance.StateManager:rep laceShortField |
| unanalyzed | call on org.apache.openjpa.enhance.StateManager:rep laceObjectField |
| method | void pcProvideFields(int[]) |
| pre | Param_1 != null |
| pre | Param_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) |
| unanalyzed | call on org.apache.openjpa.enhance.StateManager:pro videdStringField |
| unanalyzed | call on org.apache.openjpa.enhance.StateManager:pro videdBooleanField |
| unanalyzed | call on org.apache.openjpa.enhance.StateManager:pro videdShortField |
| unanalyzed | call on org.apache.openjpa.enhance.StateManager:pro videdObjectField |
| method | void pcCopyField(WeblogPermission, int) |
| pre | Param_1 != null |
| pre | Param_2 - pcInheritedFieldCount in 0..4 |
| pre | init'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) |
| post | Param_0.id == One-of{old Param_0.id, Param_1.id} |
| post | possibly_updated(Param_0.pending) |
| post | Param_0.permissionMask == One-of{old Param_0.permissionMask, Param_1.permissionMask} |
| post | Param_0.user == One-of{old Param_0.user, Param_1.user} |
| post | Param_0.website == One-of{old Param_0.website, Param_1.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} |
| 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 <= 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) |
| post | possibly_updated(Param_0.id) |
| post | possibly_updated(Param_0.pending) |
| post | possibly_updated(Param_0.permissionMask) |
| post | possibly_updated(Param_0.user) |
| post | possibly_updated(Param_0.website) |
| unanalyzed | call on java.lang.String:trim |
| unanalyzed | call on java.lang.String:length |
| 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} |
| 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 | org.apache.roller.weblogger.pojos.WeblogPermission __static_init |
| presumption | init'ed(java.lang.Boolean.TYPE) |
| presumption | init'ed(java.lang.Short.TYPE) |
| post | ADMIN == 3 |
| post | AUTHOR == 1 |
| post | new Class[](WeblogPermission__static_init#2) num objects == 1 |
| post | new String[](WeblogPermission__static_init#1) num objects == 1 |
| post | new byte[](WeblogPermission__static_init#3) num objects == 1 |
| post | LIMITED == 0 |
| post | pcFieldFlags == &new byte[](WeblogPermission__ static_init#3) |
| post | pcFieldNames == &new String[](WeblogPermission_ _static_init#1) |
| post | pcFieldTypes == &new Class[](WeblogPermission__ static_init#2) |
| post | pcFieldTypes.length == 5 |
| post | pcFieldNames.length == 5 |
| post | pcFieldFlags.length == 5 |
| post | pcFieldTypes[1] == java.lang.Boolean.TYPE |
| post | (soft) init'ed(pcFieldTypes[1]) |
| post | pcFieldTypes[2] == java.lang.Short.TYPE |
| post | (soft) init'ed(pcFieldTypes[2]) |
| post | pcFieldNames[0] == &"id" |
| post | pcFieldNames[1] == &"pending" |
| post | pcFieldNames[2] == &"permissionMask" |
| post | pcFieldNames[3] == &"user" |
| post | pcFieldNames[4] == &"website" |
| post | pcFieldFlags[0] == 26 |
| post | pcFieldFlags[1] == 26 |
| post | pcFieldFlags[2] == 26 |
| post | pcFieldFlags[3] == 26 |
| post | pcFieldFlags[4] == 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 |
| + |
|
low |
|
precondition failure | org/apache/roller/weblogger/pojos/WeblogPermission. pcReplaceField: Param_1 - pcInheritedFieldCount in 0..4 |
| + |
|
low |
|
precondition failure | org/apache/roller/weblogger/pojos/WeblogPermission. pcProvideField: Param_1 - pcInheritedFieldCount in 0..4 |
| + |
|
low |
|
precondition failure | org/apache/roller/weblogger/pojos/WeblogPermission. pcCopyField: Param_2 - pcInheritedFieldCount in 0..4 |
|   |
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:settingShortField(PersistenceCapable, int, short, short, 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:settingBooleanField(PersistenceCapable , int, bool, bool, int) |
|   |
info | method not available | -- call on String org.apache.openjpa.enhance. StateManager:replaceStringField(PersistenceCapable, int) |
|   |
info | method not available | -- call on bool org.apache.openjpa.enhance. StateManager:replaceBooleanField(PersistenceCapable , int) |
|   |
info | method not available | -- call on short org.apache.openjpa.enhance. StateManager:replaceShortField(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:providedBooleanField(PersistenceCapabl e, int, bool) |
|   |
info | method not available | -- call on void org.apache.openjpa.enhance. StateManager:providedShortField(PersistenceCapable, int, short) |
|   |
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() |