| method | RuntimeConfigDefs unmarshall(InputStream) |
| pre | instream != null |
| presumption | java.util.Iterator:next(...)@67 != null |
| presumption | org.jdom.Document:getRootElement(...)@63 != null |
| presumption | org.jdom.Element:getChildren(...)@64 != null |
| presumption | org.jdom.input.SAXBuilder:build(...)@61 != null |
| post | return_value == &new RuntimeConfigDefs(unmarsha ll#1) |
| post | new ArrayList(RuntimeConfigDefs#1) num objects == 1 |
| post | new RuntimeConfigDefs(unmarshall#1) num objects == 1 |
| post | return_value.configDefs == &new ArrayList(RuntimeConfigDefs#1) |
| unanalyzed | call on org.jdom.Element:getAttributeValue |
| unanalyzed | call on org.jdom.Element:getChildText |
| unanalyzed | call on org.jdom.Element:getChild |
| unanalyzed | call on java.lang.Integer:parseInt |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on org.jdom.Element:getChildren |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on java.util.List:add |
| test_vector | java.util.Iterator:hasNext(...)@66: {0}, {1} |
| method | ConfigDef elementToConfigDef(Element) |
| pre | element != null |
| presumption | java.util.Iterator:next(...)@85 != null |
| presumption | org.jdom.Element:getChildren(...)@81 != null |
| post | return_value == &new ConfigDef(elementToConfigD ef#1) |
| post | new ArrayList(ConfigDef#1) num objects == 1 |
| post | new ConfigDef(elementToConfigDef#1) num objects == 1 |
| post | return_value.displayGroups == &new ArrayList(ConfigDef#1) |
| post | init'ed(return_value.name) |
| unanalyzed | call on org.jdom.Element:getAttributeValue |
| unanalyzed | call on org.jdom.Element:getChildText |
| unanalyzed | call on org.jdom.Element:getChild |
| unanalyzed | call on java.lang.Integer:parseInt |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on org.jdom.Element:getChildren |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on java.util.List:add |
| test_vector | java.util.Iterator:hasNext(...)@83: {0}, {1} |
| method | DisplayGroup elementToDisplayGroup(Element) |
| pre | element != null |
| presumption | java.util.Iterator:next(...)@104 != null |
| presumption | org.jdom.Element:getChildren(...)@100 != null |
| post | return_value == &new DisplayGroup(elementToDisp layGroup#1) |
| post | new ArrayList(DisplayGroup#1) num objects == 1 |
| post | new DisplayGroup(elementToDisplayGroup#1) num objects == 1 |
| post | init'ed(return_value.key) |
| post | init'ed(return_value.name) |
| post | return_value.propertyDefs == &new ArrayList(DisplayGroup#1) |
| unanalyzed | call on org.jdom.Element:getAttributeValue |
| unanalyzed | call on org.jdom.Element:getChildText |
| unanalyzed | call on org.jdom.Element:getChild |
| unanalyzed | call on java.lang.Integer:parseInt |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on java.util.List:add |
| test_vector | java.util.Iterator:hasNext(...)@102: {0}, {1} |
| method | PropertyDef elementToPropertyDef(Element) |
| pre | element != null |
| post | return_value == &new PropertyDef(elementToPrope rtyDef#1) |
| post | new PropertyDef(elementToPropertyDef#1) num objects == 1 |
| post | init'ed(return_value.cols) |
| post | init'ed(return_value.defaultValue) |
| post | init'ed(return_value.key) |
| post | init'ed(return_value.name) |
| post | init'ed(return_value.rows) |
| post | init'ed(return_value.type) |
| unanalyzed | call on java.lang.Integer:parseInt |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| test_vector | org.jdom.Element:getChild(...)@122: Addr_Set{null}, Inverse{null} |
| test_vector | org.jdom.Element:getChild(...)@125: Addr_Set{null}, Inverse{null} |