| method | BlogEntry loadBlogEntry(Blog, String) |
| pre | blog != null |
| pre | (soft) log != null |
| post | return_value == One-of{&new BlogEntry(loadBlogE ntry#2*), null} |
| post | return_value in Addr_Set{null,&new BlogEntry(loadBlogEntry#2*)} |
| post | new ArrayList(BlogEntry#2) num objects <= 1 |
| post | new ArrayList(BlogEntry#3) num objects == new ArrayList(BlogEntry#2) num objects |
| post | new ArrayList(Content#1) num objects == new ArrayList(BlogEntry#2) num objects |
| post | new ArrayList(Content#3) num objects == new ArrayList(BlogEntry#2) num objects |
| post | new BlogEntry(loadBlogEntry#2*) num objects == new ArrayList(BlogEntry#2) num objects |
| post | new Date(PageBasedContent#2) num objects == new ArrayList(BlogEntry#2) num objects |
| post | new HashSet(BlogEntry#1) num objects == new ArrayList(BlogEntry#2) num objects |
| post | new LinkedList(PageBasedContent#1) num objects == new ArrayList(BlogEntry#2) num objects |
| post | new PropertyChangeSupport(Content#2) num objects == new ArrayList(BlogEntry#2) num objects |
| post | new BlogEntry(loadBlogEntry#2*).author == &"" |
| post | new BlogEntry(loadBlogEntry#2*).body == &"" |
| post | new BlogEntry(loadBlogEntry#2*).excerpt == &"" |
| post | new BlogEntry(loadBlogEntry#2*).subtitle == &"" |
| post | new BlogEntry(loadBlogEntry#2*).tags == &"" |
| post | new BlogEntry(loadBlogEntry#2*).tagsAsCommaSeparate d == &"" |
| post | new BlogEntry(loadBlogEntry#2*).title == &"" |
| post | new BlogEntry(loadBlogEntry#2*).blog == blog |
| post | new BlogEntry(loadBlogEntry#2*).blog != null |
| post | new BlogEntry(loadBlogEntry#2*).categories == &new HashSet(BlogEntry#1) |
| post | new BlogEntry(loadBlogEntry#2*).comments == &new ArrayList(BlogEntry#2) |
| post | new BlogEntry(loadBlogEntry#2*).commentsEnabled == 1 |
| post | new BlogEntry(loadBlogEntry#2*).trackBacksEnabled == 1 |
| post | init'ed(new BlogEntry(loadBlogEntry#2*).date) |
| post | new BlogEntry(loadBlogEntry#2*).events == &new ArrayList(Content#1) |
| post | init'ed(new BlogEntry(loadBlogEntry#2*). eventsEnabled) |
| post | possibly_updated(new BlogEntry(loadBlogEntry#2*). id) |
| post | init'ed(new BlogEntry(loadBlogEntry#2*).lockedBy) |
| post | init'ed(new BlogEntry(loadBlogEntry#2*).permalink) |
| post | init'ed(new BlogEntry(loadBlogEntry#2*). persistent) |
| post | new BlogEntry(loadBlogEntry#2*).propertyChangeEvent s == &new ArrayList(Content#3) |
| post | new BlogEntry(loadBlogEntry#2*).propertyChangeSuppo rt == &new PropertyChangeSupport(Content#2) |
| post | new BlogEntry(loadBlogEntry#2*).state == &net.sourceforge.pebble.domain.State__static_ init.new State(State__static_init#4) |
| post | new BlogEntry(loadBlogEntry#2*).tagsAsList == &new LinkedList(PageBasedContent#1) |
| post | new BlogEntry(loadBlogEntry#2*).trackBacks == &new ArrayList(BlogEntry#3) |
| unanalyzed | call on java.io.File:exists |
| unanalyzed | call on java.io.File:getAbsolutePath |
| unanalyzed | call on org.apache.commons.logging.Log:debug |
| unanalyzed | call on org.xml.sax.helpers.DefaultHandler |
| unanalyzed | call on java.text.SimpleDateFormat |
| unanalyzed | call on net.sourceforge.pebble.domain. Blog:getTimeZone |
| unanalyzed | call on java.text.SimpleDateFormat:setTimeZone |
| unanalyzed | call on net.sourceforge.pebble.domain. Blog:getLocale |
| unanalyzed | call on javax.xml.parsers.SAXParserFactory:newInsta nce |
| unanalyzed | call on javax.xml.parsers.SAXParserFactory:setValid ating |
| unanalyzed | call on javax.xml.parsers.SAXParserFactory:setNames paceAware |
| unanalyzed | call on javax.xml.parsers.SAXParserFactory:newSAXPa rser |
| unanalyzed | call on javax.xml.parsers.SAXParser:parse |
| unanalyzed | call on getBlog |
| unanalyzed | call on java.lang.Exception:getMessage |
| unanalyzed | call on java.lang.String:valueOf |
| unanalyzed | call on org.apache.commons.logging.Log:error |
| unanalyzed | call on java.lang.Exception:printStackTrace |
| unanalyzed | call on net.sourceforge.pebble.domain.Blog:getRoot |
| unanalyzed | call on java.text.DateFormat:setTimeZone |
| unanalyzed | call on java.lang.Long:parseLong |
| unanalyzed | call on java.util.Date |
| unanalyzed | call on java.text.DateFormat:format |
| unanalyzed | call on java.beans.PropertyChangeSupport:fireProper tyChange |
| unanalyzed | call on java.util.Date:getTime |
| unanalyzed | call on java.util.HashSet |
| unanalyzed | call on setState |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on java.beans.PropertyChangeSupport |
| unanalyzed | call on java.beans.PropertyChangeSupport:addPropert yChangeListener |
| unanalyzed | call on java.util.LinkedList |
| unanalyzed | call on setDate |
| unanalyzed | call on net.sourceforge.pebble.api.event. PebbleEvent |
| unanalyzed | call on java.util.List:add |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on java.util.EventObject |
| unanalyzed | call on java.lang.Exception |
| method | BlogEntry loadBlogEntry(Blog, File) |
| pre | source != null |
| pre | (soft) log != null |
| pre | (soft) blog != null |
| presumption | javax.xml.parsers.SAXParserFactory:newInstance(... )@71 != null |
| presumption | javax.xml.parsers.SAXParserFactory:newSAXParser(... )@74 != null |
| post | return_value in Addr_Set{null,&new BlogEntry(loadBlogEntry#2)} |
| post | new ArrayList(BlogEntry#2) num objects <= 1 |
| post | new ArrayList(BlogEntry#3) num objects <= 1 |
| post | new ArrayList(Content#1) num objects <= 1 |
| post | new ArrayList(Content#3) num objects <= 1 |
| post | new BlogEntry(loadBlogEntry#2) num objects <= 1 |
| post | new BlogEntry(loadBlogEntry#2).author == &"" |
| post | new BlogEntry(loadBlogEntry#2).blog == blog |
| post | new BlogEntry(loadBlogEntry#2).body == &"" |
| post | (soft) new BlogEntry(loadBlogEntry#2).blog != null |
| post | new BlogEntry(loadBlogEntry#2).categories == &new HashSet(BlogEntry#1) |
| post | new BlogEntry(loadBlogEntry#2).comments == &new ArrayList(BlogEntry#2) |
| post | new BlogEntry(loadBlogEntry#2).commentsEnabled == 1 |
| post | init'ed(new BlogEntry(loadBlogEntry#2).date) |
| post | new BlogEntry(loadBlogEntry#2).events == &new ArrayList(Content#1) |
| post | init'ed(new BlogEntry(loadBlogEntry#2). eventsEnabled) |
| post | new BlogEntry(loadBlogEntry#2).excerpt == &"" |
| post | possibly_updated(new BlogEntry(loadBlogEntry#2). id) |
| post | init'ed(new BlogEntry(loadBlogEntry#2).lockedBy) |
| post | init'ed(new BlogEntry(loadBlogEntry#2).permalink) |
| post | init'ed(new BlogEntry(loadBlogEntry#2).persistent) |
| post | new BlogEntry(loadBlogEntry#2).propertyChangeEvents == &new ArrayList(Content#3) |
| post | new BlogEntry(loadBlogEntry#2).propertyChangeSuppor t == &new PropertyChangeSupport(Content#2) |
| post | new BlogEntry(loadBlogEntry#2).state == &net.sourceforge.pebble.domain.State__static_ init.new State(State__static_init#4) |
| post | new BlogEntry(loadBlogEntry#2).subtitle == &"" |
| post | new BlogEntry(loadBlogEntry#2).tags == &"" |
| post | new BlogEntry(loadBlogEntry#2).tagsAsCommaSeparated == &"" |
| post | new BlogEntry(loadBlogEntry#2).tagsAsList == &new LinkedList(PageBasedContent#1) |
| post | new BlogEntry(loadBlogEntry#2).title == &"" |
| post | new BlogEntry(loadBlogEntry#2).trackBacks == &new ArrayList(BlogEntry#3) |
| post | new BlogEntry(loadBlogEntry#2).trackBacksEnabled == 1 |
| post | new Date(PageBasedContent#2) num objects <= 1 |
| post | new HashSet(BlogEntry#1) num objects <= 1 |
| post | new LinkedList(PageBasedContent#1) num objects <= 1 |
| post | new PropertyChangeSupport(Content#2) num objects <= 1 |
| unanalyzed | call on org.xml.sax.helpers.DefaultHandler |
| unanalyzed | call on java.text.SimpleDateFormat |
| unanalyzed | call on net.sourceforge.pebble.domain. Blog:getTimeZone |
| unanalyzed | call on java.text.SimpleDateFormat:setTimeZone |
| unanalyzed | call on net.sourceforge.pebble.domain. Blog:getLocale |
| unanalyzed | call on java.beans.PropertyChangeSupport:fireProper tyChange |
| unanalyzed | call on java.util.Date:getTime |
| unanalyzed | call on java.util.HashSet |
| unanalyzed | call on setState |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on java.beans.PropertyChangeSupport |
| unanalyzed | call on getBlog |
| unanalyzed | call on java.beans.PropertyChangeSupport:addPropert yChangeListener |
| unanalyzed | call on java.util.LinkedList |
| unanalyzed | call on java.util.Date |
| unanalyzed | call on setDate |
| unanalyzed | call on java.util.List:add |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on net.sourceforge.pebble.api.event. PebbleEvent |
| unanalyzed | call on java.util.EventObject |
| unanalyzed | call on java.lang.Exception |
| test_vector | java.io.File:exists(...)@65: {0}, {1} |
| method | Collection loadBlogEntries(Blog) |
| pre | blog != null |
| pre | (soft) log != null |
| presumption | Local_13[Local_11]@103 != null |
| presumption | Local_18[Local_16]@105 != null |
| presumption | Local_23[Local_21]@107 != null |
| presumption | Local_8[Local_6]@101 != null |
| presumption | blogEntryFiles.length@107 <= 232-1 |
| presumption | days.length@105 <= 232-1 |
| presumption | java.io.File:listFiles(...)@101 != null |
| presumption | java.io.File:listFiles(...)@103 != null |
| presumption | java.io.File:listFiles(...)@105 != null |
| presumption | java.io.File:listFiles(...)@107 != null |
| presumption | months.length@103 <= 232-1 |
| presumption | years.length@101 <= 232-1 |
| post | return_value == &new ArrayList(loadBlogEntries# 1) |
| post | new ArrayList(loadBlogEntries#1) num objects == 1 |
| unanalyzed | call on java.io.File:exists |
| unanalyzed | call on java.io.File:getAbsolutePath |
| unanalyzed | call on org.apache.commons.logging.Log:debug |
| unanalyzed | call on org.xml.sax.helpers.DefaultHandler |
| unanalyzed | call on java.text.SimpleDateFormat |
| unanalyzed | call on net.sourceforge.pebble.domain. Blog:getTimeZone |
| unanalyzed | call on java.text.SimpleDateFormat:setTimeZone |
| unanalyzed | call on net.sourceforge.pebble.domain. Blog:getLocale |
| unanalyzed | call on javax.xml.parsers.SAXParserFactory:newInsta nce |
| unanalyzed | call on javax.xml.parsers.SAXParserFactory:setValid ating |
| unanalyzed | call on javax.xml.parsers.SAXParserFactory:setNames paceAware |
| unanalyzed | call on javax.xml.parsers.SAXParserFactory:newSAXPa rser |
| unanalyzed | call on javax.xml.parsers.SAXParser:parse |
| unanalyzed | call on getBlog |
| unanalyzed | call on java.lang.Exception:getMessage |
| unanalyzed | call on java.lang.String:valueOf |
| unanalyzed | call on org.apache.commons.logging.Log:error |
| unanalyzed | call on java.lang.Exception:printStackTrace |
| unanalyzed | call on java.beans.PropertyChangeSupport:fireProper tyChange |
| unanalyzed | call on java.util.Date:getTime |
| unanalyzed | call on java.util.HashSet |
| unanalyzed | call on setState |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on java.beans.PropertyChangeSupport |
| unanalyzed | call on java.beans.PropertyChangeSupport:addPropert yChangeListener |
| unanalyzed | call on java.util.LinkedList |
| unanalyzed | call on java.util.Date |
| unanalyzed | call on setDate |
| unanalyzed | call on net.sourceforge.pebble.api.event. PebbleEvent |
| unanalyzed | call on java.util.List:add |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on java.util.EventObject |
| unanalyzed | call on java.lang.Exception |
| method | void storeBlogEntry(BlogEntry) |
| pre | blogEntry != null |
| pre | init'ed(blogEntry.attachment) |
| pre | init'ed(blogEntry.categories) |
| pre | blogEntry.comments != null |
| pre | init'ed(blogEntry.commentsEnabled) |
| pre | init'ed(blogEntry.excerpt) |
| pre | init'ed(blogEntry.timeZoneId) |
| pre | init'ed(blogEntry.trackBacks) |
| pre | init'ed(blogEntry.trackBacksEnabled) |
| pre | log != null |
| pre | (soft) init'ed(blogEntry.attachment.size) |
| pre | (soft) init'ed(blogEntry.attachment.type) |
| pre | (soft) init'ed(blogEntry.attachment.url) |
| unanalyzed | call on java.io.File:exists |
| unanalyzed | call on java.io.File:getAbsolutePath |
| pre | init'ed(blogEntry.author) |
| unanalyzed | call on org.apache.commons.logging.Log:debug |
| pre | blogEntry.blog != null |
| pre | init'ed(blogEntry.body) |
| unanalyzed | call on java.lang.Exception:getMessage |
| unanalyzed | call on java.lang.String:valueOf |
| unanalyzed | call on org.apache.commons.logging.Log:error |
| unanalyzed | call on java.lang.Exception:printStackTrace |
| pre | init'ed(blogEntry.date) |
| unanalyzed | call on net.sourceforge.pebble.domain.Blog:getRoot |
| pre | init'ed(blogEntry.id) |
| unanalyzed | call on org.w3c.dom.Document:createTextNode |
| unanalyzed | call on org.w3c.dom.Document:createCDATASection |
| pre | init'ed(blogEntry.originalPermalink) |
| pre | blogEntry.state != null |
| unanalyzed | call on java.text.SimpleDateFormat |
| unanalyzed | call on java.text.DateFormat:setTimeZone |
| unanalyzed | call on java.lang.Long:parseLong |
| pre | init'ed(blogEntry.state.name) |
| unanalyzed | call on java.util.Date |
| pre | init'ed(blogEntry.subtitle) |
| pre | init'ed(blogEntry.tags) |
| unanalyzed | call on java.text.DateFormat:format |
| pre | init'ed(blogEntry.title) |
| unanalyzed | call on java.io.File |
| unanalyzed | call on java.io.File:getParentFile |
| unanalyzed | call on java.io.File:getName |
| unanalyzed | call on javax.xml.parsers.DocumentBuilderFactory:ne wInstance |
| unanalyzed | call on javax.xml.parsers.DocumentBuilderFactory:se tValidating |
| unanalyzed | call on javax.xml.parsers.DocumentBuilderFactory:se tNamespaceAware |
| unanalyzed | call on javax.xml.parsers.DocumentBuilderFactory:se tIgnoringElementContentWhitespace |
| unanalyzed | call on javax.xml.parsers.DocumentBuilderFactory:se tIgnoringComments |
| unanalyzed | call on javax.xml.parsers.DocumentBuilderFactory:ne wDocumentBuilder |
| unanalyzed | call on javax.xml.parsers.DocumentBuilder:newDocume nt |
| unanalyzed | call on org.w3c.dom.Document:createElement |
| unanalyzed | call on org.w3c.dom.Document:appendChild |
| unanalyzed | call on org.w3c.dom.Element:appendChild |
| unanalyzed | call on java.util.Set:iterator |
| unanalyzed | call on java.text.SimpleDateFormat:setTimeZone |
| unanalyzed | call on java.text.SimpleDateFormat:format |
| unanalyzed | call on getComments |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on storeComment |
| unanalyzed | call on storeTrackBack |
| unanalyzed | call on java.io.StringWriter |
| unanalyzed | call on javax.xml.transform.dom.DOMSource |
| unanalyzed | call on javax.xml.transform.stream.StreamResult |
| unanalyzed | call on javax.xml.transform.TransformerFactory:newI nstance |
| unanalyzed | call on javax.xml.transform.TransformerFactory:newT ransformer |
| unanalyzed | call on javax.xml.transform.Transformer:setOutputPr operty |
| unanalyzed | call on javax.xml.transform.Transformer:transform |
| unanalyzed | call on java.io.File:length |
| unanalyzed | call on java.io.File:renameTo |
| unanalyzed | call on java.io.FileOutputStream |
| unanalyzed | call on java.io.OutputStreamWriter |
| unanalyzed | call on java.io.BufferedWriter |
| unanalyzed | call on java.io.StringWriter:getBuffer |
| unanalyzed | call on java.io.BufferedWriter:write |
| unanalyzed | call on java.io.BufferedWriter:flush |
| unanalyzed | call on java.io.BufferedWriter:close |
| unanalyzed | call on org.w3c.dom.Node:appendChild |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on java.util.HashSet |
| unanalyzed | call on net.sourceforge.pebble.domain. Blog:getTimeZoneId |
| unanalyzed | call on java.util.List:add |
| unanalyzed | call on java.util.List:addAll |
| unanalyzed | call on java.lang.String:length |
| unanalyzed | call on java.util.Date:getTime |
| unanalyzed | call on java.lang.Exception |
| test_vector | java.io.File:exists(...)@126: {1}, {0} |
| method | void storeBlogEntry(BlogEntry, File) |
| pre | blogEntry != null |
| pre | init'ed(blogEntry.attachment) |
| pre | init'ed(blogEntry.categories) |
| pre | blogEntry.comments != null |
| pre | init'ed(blogEntry.commentsEnabled) |
| pre | init'ed(blogEntry.excerpt) |
| pre | init'ed(blogEntry.timeZoneId) |
| pre | init'ed(blogEntry.trackBacks) |
| pre | init'ed(blogEntry.trackBacksEnabled) |
| pre | destination != null |
| pre | log != null |
| pre | (soft) init'ed(blogEntry.attachment.size) |
| pre | (soft) init'ed(blogEntry.attachment.type) |
| pre | (soft) init'ed(blogEntry.attachment.url) |
| pre | (soft) blogEntry.blog != null |
| presumption | comment.state@245 != null |
| presumption | java.io.StringWriter:getBuffer(...)@277 != null |
| pre | init'ed(blogEntry.author) |
| pre | init'ed(blogEntry.body) |
| presumption | java.util.Iterator:next(...)@205 != null |
| pre | init'ed(blogEntry.date) |
| presumption | java.util.Iterator:next(...)@245 != null |
| presumption | java.util.Iterator:next(...)@252 != null |
| presumption | init'ed(java.util.Locale.ENGLISH) |
| pre | init'ed(blogEntry.originalPermalink) |
| pre | blogEntry.state != null |
| presumption | javax.xml.parsers.DocumentBuilder:newDocument(... )@152 != null |
| presumption | javax.xml.parsers.DocumentBuilderFactory:newDocumen tBuilder(...)@151 != null |
| pre | init'ed(blogEntry.state.name) |
| presumption | javax.xml.parsers.DocumentBuilderFactory:newInstanc e(...)@145 != null |
| presumption | javax.xml.transform.TransformerFactory:newInstance( ...)@261 != null |
| pre | init'ed(blogEntry.subtitle) |
| presumption | javax.xml.transform.TransformerFactory:newTransform er(...)@261 != null |
| pre | init'ed(blogEntry.tags) |
| pre | init'ed(blogEntry.title) |
| presumption | org.w3c.dom.Document:createElement(...)@154 != null |
| presumption | org.w3c.dom.Document:createElement(...)@157 != null |
| presumption | org.w3c.dom.Document:createElement(...)@158 != null |
| presumption | org.w3c.dom.Document:createElement(...)@159 != null |
| presumption | org.w3c.dom.Document:createElement(...)@160 != null |
| presumption | org.w3c.dom.Document:createElement(...)@162 != null |
| presumption | org.w3c.dom.Document:createElement(...)@163 != null |
| presumption | org.w3c.dom.Document:createElement(...)@164 != null |
| presumption | org.w3c.dom.Document:createElement(...)@165 != null |
| presumption | org.w3c.dom.Document:createElement(...)@166 != null |
| presumption | org.w3c.dom.Document:createElement(...)@168 != null |
| presumption | org.w3c.dom.Document:createElement(...)@169 != null |
| presumption | org.w3c.dom.Document:createElement(...)@170 != null |
| presumption | org.w3c.dom.Document:createElement(...)@183 != null |
| presumption | org.w3c.dom.Document:createElement(...)@206 != null |
| presumption | org.w3c.dom.Document:createElement(...)@231 != null |
| presumption | org.w3c.dom.Document:createElement(...)@234 != null |
| presumption | org.w3c.dom.Document:createElement(...)@237 != null |
| presumption | trackBack.state@252 != null |
| unanalyzed | call on org.w3c.dom.Document:createTextNode |
| unanalyzed | call on org.w3c.dom.Document:createCDATASection |
| unanalyzed | call on org.w3c.dom.Document:createElement |
| unanalyzed | call on org.w3c.dom.Element:appendChild |
| unanalyzed | call on java.text.SimpleDateFormat |
| unanalyzed | call on java.text.SimpleDateFormat:setTimeZone |
| unanalyzed | call on java.text.SimpleDateFormat:format |
| unanalyzed | call on org.w3c.dom.Node:appendChild |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on java.util.HashSet |
| unanalyzed | call on net.sourceforge.pebble.domain. Blog:getTimeZoneId |
| unanalyzed | call on java.util.List:add |
| unanalyzed | call on getComments |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on java.util.List:addAll |
| unanalyzed | call on java.lang.String:length |
| unanalyzed | call on java.util.Date:getTime |
| unanalyzed | call on java.lang.Exception |
| test_vector | blogEntry.attachment: Addr_Set{null}, Inverse{null} |
| test_vector | blogEntry.excerpt: Addr_Set{null}, Inverse{null} |
| test_vector | java.io.File:exists(...)@270: {0}, {1} |
| test_vector | java.io.File:length(...)@270: {-9_223_372_036_854_7 75_808..0}, {1..264-1} |
| test_vector | java.util.Iterator:hasNext(...)@204: {1}, {0} |
| test_vector | java.util.Iterator:hasNext(...)@244: {1}, {0} |
| test_vector | java.util.Iterator:hasNext(...)@251: {1}, {0} |
| test_vector | blogEntry.author: Addr_Set{null}, Inverse{null} |
| test_vector | blogEntry.originalPermalink: Addr_Set{null}, Inverse{null} |
| test_vector | blogEntry.tags: Addr_Set{null}, Inverse{null} |
| method | void storeComment(Comment, Document, Node) |
| pre | comment != null |
| pre | init'ed(comment.authenticated) |
| pre | init'ed(comment.author) |
| pre | init'ed(comment.body) |
| pre | init'ed(comment.date) |
| pre | init'ed(comment.email) |
| pre | init'ed(comment.ipAddress) |
| pre | init'ed(comment.parent) |
| pre | comment.state != null |
| pre | init'ed(comment.state.name) |
| pre | init'ed(comment.title) |
| pre | init'ed(comment.website) |
| pre | doc != null |
| pre | root != null |
| pre | (soft) comment...date != null |
| presumption | init'ed(java.util.Locale.ENGLISH) |
| presumption | org.w3c.dom.Document:createElement(...)@296 != null |
| presumption | org.w3c.dom.Document:createElement(...)@299 != null |
| presumption | org.w3c.dom.Document:createElement(...)@300 != null |
| presumption | org.w3c.dom.Document:createElement(...)@301 != null |
| presumption | org.w3c.dom.Document:createElement(...)@302 != null |
| presumption | org.w3c.dom.Document:createElement(...)@303 != null |
| presumption | org.w3c.dom.Document:createElement(...)@304 != null |
| presumption | org.w3c.dom.Document:createElement(...)@305 != null |
| presumption | org.w3c.dom.Document:createElement(...)@306 != null |
| presumption | org.w3c.dom.Document:createElement(...)@307 != null |
| presumption | org.w3c.dom.Document:createElement(...)@308 != null |
| unanalyzed | call on org.w3c.dom.Document:createTextNode |
| unanalyzed | call on org.w3c.dom.Document:createCDATASection |
| unanalyzed | call on java.util.Date:getTime |
| test_vector | comment.parent: Addr_Set{null}, Inverse{null} |
| method | void storeTrackBack(TrackBack, Document, Node) |
| pre | doc != null |
| pre | root != null |
| pre | trackBack != null |
| pre | init'ed(trackBack.blogName) |
| pre | init'ed(trackBack.date) |
| pre | init'ed(trackBack.excerpt) |
| pre | init'ed(trackBack.ipAddress) |
| pre | trackBack.state != null |
| pre | init'ed(trackBack.state.name) |
| pre | init'ed(trackBack.title) |
| pre | (soft) init'ed(trackBack.url) |
| presumption | init'ed(java.util.Locale.ENGLISH) |
| presumption | org.w3c.dom.Document:createElement(...)@363 != null |
| presumption | org.w3c.dom.Document:createElement(...)@366 != null |
| presumption | org.w3c.dom.Document:createElement(...)@367 != null |
| presumption | org.w3c.dom.Document:createElement(...)@368 != null |
| presumption | org.w3c.dom.Document:createElement(...)@369 != null |
| presumption | org.w3c.dom.Document:createElement(...)@370 != null |
| presumption | org.w3c.dom.Document:createElement(...)@371 != null |
| presumption | org.w3c.dom.Document:createElement(...)@372 != null |
| unanalyzed | call on org.w3c.dom.Document:createTextNode |
| unanalyzed | call on org.w3c.dom.Document:createCDATASection |
| unanalyzed | call on java.lang.String:length |