| method | int doStartTag() |
| pre | this.pageContext != null |
| pre | (soft) init'ed(this.query) |
| presumption | java.io.Writer:append(...)@57 != null |
| presumption | java.io.Writer:append(...)@60 != null |
| presumption | javax.servlet.jsp.JspWriter:append(...)@57 != null |
| presumption | javax.servlet.jsp.JspWriter:append(...)@59 != null |
| presumption | javax.servlet.jsp.JspWriter:append(...)@60 != null |
| presumption | javax.servlet.jsp.PageContext:getOut(...)@52 != null |
| presumption | javax.servlet.jsp.PageContext:getRequest(...)@53 != null |
| post | return_value == 0 |
| test_vector | this.query: {0}, {1} |
| test_vector | javax.servlet.ServletRequest:getAttribute(...)@53: Addr_Set{null}, Inverse{null} |