| method | Module parse(Element) |
| pre | elem != null |
| post | return_value == &new AppModuleImpl(parse#1) |
| post | new AppModuleImpl(parse#1) num objects == 1 |
| post | init'ed(return_value.draft) |
| post | init'ed(return_value.edited) |
| unanalyzed | call on org.jdom.Namespace:getNamespace |
| unanalyzed | call on com.sun.syndication.feed.module.ModuleImpl |
| test_vector | java.lang.String:equals(...)@44: {0}, {1} |
| test_vector | java.lang.String:equals(...)@45: {0}, {1} |
| test_vector | org.jdom.Element:getChild(...)@40: Addr_Set{null}, Inverse{null} |
| test_vector | org.jdom.Element:getChild(...)@42: Addr_Set{null}, Inverse{null} |
| test_vector | org.jdom.Element:getChild(...)@48: Addr_Set{null}, Inverse{null} |