| method | WeblogUpdatePinger$PingResult sendPing(PingTarget, Weblog) |
| pre | pingTarget != null |
| pre | website != null |
| presumption | org.apache.commons.logging.LogFactory:getLog(... )@52 != null |
| post | init'ed(java.lang.Object:toString(...)._tainted) |
| post | return_value == One-of{&new WeblogUpdatePinger$ PingResult(parseResult#1), &new WeblogUpdatePinger$PingResult(parseResult#2), &new WeblogUpdatePinger$PingResult(parseResult #4)} |
| post | return_value in Addr_Set{&new WeblogUpdatePinge r$PingResult(parseResult#1),&new WeblogUpdatePinger$PingResult(parseResult#2), &new WeblogUpdatePinger$PingResult(parseResult# 4)} |
| post | new WeblogUpdatePinger$PingResult(parseResult#1) num objects <= 1 |
| post | new WeblogUpdatePinger$PingResult(parseResult#1)._ tainted == 0 |
| post | new WeblogUpdatePinger$PingResult(parseResult#2)._ tainted == 0 |
| post | new WeblogUpdatePinger$PingResult(parseResult#4)._ tainted == 0 |
| post | init'ed(new WeblogUpdatePinger$PingResult(parseResu lt#1).error) |
| post | new WeblogUpdatePinger$PingResult(parseResult#1). message == &"" |
| post | new WeblogUpdatePinger$PingResult(parseResult#2) num objects <= 1 |
| post | init'ed(new WeblogUpdatePinger$PingResult(parseResu lt#2).error) |
| post | new WeblogUpdatePinger$PingResult(parseResult#2). message != null |
| post | new WeblogUpdatePinger$PingResult(parseResult#4) num objects <= 1 |
| post | init'ed(new WeblogUpdatePinger$PingResult(parseResu lt#4).error) |
| post | new WeblogUpdatePinger$PingResult(parseResult#4). message == &java.lang.Object:toString(...) |
| unanalyzed | call on java.lang.Boolean:booleanValue |
| unanalyzed | call on java.util.Map:get |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on org.apache.commons.logging.Log:isDebugEnabl ed |
| unanalyzed | call on java.lang.Object:getClass |
| unanalyzed | call on java.lang.Class:getName |
| unanalyzed | call on org.apache.commons.logging.Log:debug |
| unanalyzed | call on java.lang.Object:toString |
| test_vector | java.util.Set:contains(...)@107: {1}, {0} |
| test_vector | org.apache.commons.logging.Log:isDebugEnabled(... )@112: {0}, {1} |
| test_vector | org.apache.commons.logging.Log:isDebugEnabled(... )@123: {0}, {1} |
| method | WeblogUpdatePinger$PingResult parseResult(Object) |
| presumption | java.lang.Object:getClass(...)@137 != null |
| presumption | org.apache.commons.logging.LogFactory:getLog(... )@52 != null |
| post | init'ed(java.lang.Object:toString(...)._tainted) |
| post | return_value in Addr_Set{&new WeblogUpdatePinge r$PingResult(parseResult#2),&new WeblogUpdatePinger$PingResult(parseResult#4), &new WeblogUpdatePinger$PingResult(parseResult# 1)} |
| post | new WeblogUpdatePinger$PingResult(parseResult#1) num objects <= 1 |
| post | init'ed(new WeblogUpdatePinger$PingResult(parseResu lt#1).error) |
| post | new WeblogUpdatePinger$PingResult(parseResult#1). message == &"" |
| post | new WeblogUpdatePinger$PingResult(parseResult#2) num objects <= 1 |
| post | init'ed(new WeblogUpdatePinger$PingResult(parseResu lt#2).error) |
| post | new WeblogUpdatePinger$PingResult(parseResult#2). message != null |
| post | new WeblogUpdatePinger$PingResult(parseResult#4) num objects <= 1 |
| post | init'ed(new WeblogUpdatePinger$PingResult(parseResu lt#4).error) |
| post | new WeblogUpdatePinger$PingResult(parseResult#4). message == &java.lang.Object:toString(...) |
| unanalyzed | call on java.lang.Boolean:booleanValue |
| test_vector | obj: Inverse{null}, Addr_Set{null} |