infer_clone/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl

// TODO: Checking any one of {InterleavedResponse, ForwardUncommited} is relatively fast. But,
// checking both is very slow.

// According to the Servlet API, one should use
//  - a writer for a textual response
//  - a stream for a binary response, or for a mixed binary+textual response
// but never both a writer and a stream.
property InterleavedResponse
  message "A ServletResponse was asked for both a writer and a stream."
  prefix "ServletResponse"
  nondet (start)
  start -> start: *
  start -> gotWriter: getWriter(R, IgnoreRet) => r := R
  start -> gotStream: getOutputStream(R, IgnoreRet) => r := R
  gotWriter -> error: getOutputStream(R, IgnoreRet) when R == r
  gotStream -> error: getWriter(R, IgnoreRet) when R == r

property ForwardUncommitted
  message "A ServletResponse was forwarded before being committed."
  nondet (start)
  start -> start: *
  start -> gotChannel: "ServletResponse.\\(getWriter\\|getOutputStream\\)"(R, C) => r := R; c := C
  gotChannel -> ok: "\\(PrintWriter\\|ServletOutputStream\\).flush.*"(C, IgnoreRet) when C == c
  gotChannel -> error: "RequestDispatcher.forward"(IgnoreDispatcher, IgnoreRequest, Response, IgnoreRet) when Response == r