| method | String render(WeblogEntry, String) |
| pre | str != null |
| presumption | java.lang.String:length(...)@73 <= 4_294_967_167 |
| presumption | java.util.regex.Matcher:group(...)@77 != null |
| presumption | java.util.regex.Pattern:compile(...)@43 != null |
| presumption | java.util.regex.Pattern:matcher(...)@72 != null |
| post | java.lang.StringBuffer:toString(...)._tainted == 0 |
| post | return_value == &java.lang.StringBuffer:toStrin g(...) |
| unanalyzed | call on java.net.URLEncoder:encode |
| unanalyzed | call on java.lang.Throwable:__curr_excep_obj |
| unanalyzed | call on java.lang.RuntimeException |
| test_vector | java.lang.String:equals(...)@78: {0}, {1} |
| test_vector | java.lang.String:length(...)@81: {1.. 232-1}, {0} |
| test_vector | java.util.regex.Matcher:find(...)@75: {0}, {1} |
| test_vector | java.util.regex.Matcher:group(...)@80: Addr_Set{null}, Inverse{null} |