| method | void doGet(HttpServletRequest, HttpServletResponse ) |
| pre | response != null |
| pre | this.authenticator != null |
| presumption | javax.servlet.http.HttpServletResponse:getWriter(.. .)@67 != null |
| unanalyzed | call on javax.servlet.http.HttpServletRequest:getSe ssion |
| unanalyzed | call on javax.servlet.http.HttpSession:getAttribute |
| unanalyzed | call on java.lang.Math:random |
| unanalyzed | call on java.lang.Integer |
| unanalyzed | call on javax.servlet.http.HttpSession:setAttribute |
| unanalyzed | call on javax.servlet.http.HttpServletRequest:getPa rameter |
| unanalyzed | call on java.util.ResourceBundle:getString |