//# 0 errors, 178 messages
//#
/*
    //#gzipresponsewrapper.java:1:1: class: net.sourceforge.pebble.web.filter.GZIPResponseWrapper
    //#gzipresponsewrapper.java:1:1: method: net.sourceforge.pebble.web.filter.GZIPResponseWrapper.net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init
 * Copyright (c) 2003-2006, Simon Brown
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   - Redistributions of source code must retain the above copyright
 *     notice, this list of conditions and the following disclaimer.
 *
 *   - Redistributions in binary form must reproduce the above copyright
 *     notice, this list of conditions and the following disclaimer in
 *     the documentation and/or other materials provided with the
 *     distribution.
 *
 *   - Neither the name of Pebble nor the names of its contributors may
 *     be used to endorse or promote products derived from this software
 *     without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 */
package net.sourceforge.pebble.web.filter;

import javax.servlet.ServletOutputStream;
import javax.servlet.http.HttpServletResponse;
import javax.servlet.http.HttpServletResponseWrapper;
import java.io.IOException;
import java.io.OutputStreamWriter;
import java.io.PrintWriter;

public class GZIPResponseWrapper extends HttpServletResponseWrapper {

  protected HttpServletResponse wrappedResponse = null;
  protected ServletOutputStream stream = null;
  protected PrintWriter writer = null;

  public GZIPResponseWrapper(HttpServletResponse response) {
    super(response);
    //#gzipresponsewrapper.java:48: method: void net.sourceforge.pebble.web.filter.GZIPResponseWrapper.net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)
    //#input(void net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)): response
    //#input(void net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)): this
    //#output(void net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)): this.stream
    //#output(void net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)): this.wrappedResponse
    //#output(void net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)): this.writer
    //#post(void net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)): this.stream == null
    //#post(void net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)): this.writer == null
    //#post(void net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)): this.wrappedResponse == response
    //#post(void net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)): init'ed(this.wrappedResponse)
    wrappedResponse = response;
  }
    //#gzipresponsewrapper.java:50: end of method: void net.sourceforge.pebble.web.filter.GZIPResponseWrapper.net.sourceforge.pebble.web.filter.GZIPResponseWrapper(HttpServletResponse)

  public ServletOutputStream createOutputStream() throws IOException {
    return (new GZIPResponseStream(wrappedResponse));
    //#gzipresponsewrapper.java:53: method: ServletOutputStream net.sourceforge.pebble.web.filter.GZIPResponseWrapper.createOutputStream()
    //#input(ServletOutputStream createOutputStream()): this
    //#input(ServletOutputStream createOutputStream()): this.wrappedResponse
    //#output(ServletOutputStream createOutputStream()): new ByteArrayOutputStream(GZIPResponseStream#1) num objects
    //#output(ServletOutputStream createOutputStream()): new GZIPOutputStream(GZIPResponseStream#2) num objects
    //#output(ServletOutputStream createOutputStream()): new GZIPResponseStream(createOutputStream#1) num objects
    //#output(ServletOutputStream createOutputStream()): return_value.__Tag
    //#output(ServletOutputStream createOutputStream()): return_value.baos
    //#output(ServletOutputStream createOutputStream()): return_value.closed
    //#output(ServletOutputStream createOutputStream()): return_value.gzipstream
    //#output(ServletOutputStream createOutputStream()): return_value.output
    //#output(ServletOutputStream createOutputStream()): return_value.response
    //#output(ServletOutputStream createOutputStream()): return_value
    //#new obj(ServletOutputStream createOutputStream()): new ByteArrayOutputStream(GZIPResponseStream#1)
    //#new obj(ServletOutputStream createOutputStream()): new GZIPOutputStream(GZIPResponseStream#2)
    //#new obj(ServletOutputStream createOutputStream()): new GZIPResponseStream(createOutputStream#1)
    //#pre[2] (ServletOutputStream createOutputStream()): this.wrappedResponse != null
    //#post(ServletOutputStream createOutputStream()): return_value == &new GZIPResponseStream(createOutputStream#1)
    //#post(ServletOutputStream createOutputStream()): new ByteArrayOutputStream(GZIPResponseStream#1) num objects == 1
    //#post(ServletOutputStream createOutputStream()): new GZIPOutputStream(GZIPResponseStream#2) num objects == 1
    //#post(ServletOutputStream createOutputStream()): new GZIPResponseStream(createOutputStream#1) num objects == 1
    //#post(ServletOutputStream createOutputStream()): return_value.__Tag == net/sourceforge/pebble/web/filter/GZIPResponseStream
    //#post(ServletOutputStream createOutputStream()): return_value.baos == &new ByteArrayOutputStream(GZIPResponseStream#1)
    //#post(ServletOutputStream createOutputStream()): return_value.closed == 0
    //#post(ServletOutputStream createOutputStream()): return_value.gzipstream == &new GZIPOutputStream(GZIPResponseStream#2)
    //#post(ServletOutputStream createOutputStream()): init'ed(return_value.output)
    //#post(ServletOutputStream createOutputStream()): return_value.response == this.wrappedResponse
    //#post(ServletOutputStream createOutputStream()): return_value.response != null
    //#unanalyzed(ServletOutputStream createOutputStream()): Effects-of-calling:javax.servlet.ServletOutputStream
    //#unanalyzed(ServletOutputStream createOutputStream()): Effects-of-calling:javax.servlet.http.HttpServletResponse:getOutputStream
    //#unanalyzed(ServletOutputStream createOutputStream()): Effects-of-calling:java.io.ByteArrayOutputStream
    //#unanalyzed(ServletOutputStream createOutputStream()): Effects-of-calling:java.util.zip.GZIPOutputStream
    //#gzipresponsewrapper.java:53: end of method: ServletOutputStream net.sourceforge.pebble.web.filter.GZIPResponseWrapper.createOutputStream()
  }

  public void finishResponse() {
    try {
      if (writer != null) {
    //#gzipresponsewrapper.java:58: method: void net.sourceforge.pebble.web.filter.GZIPResponseWrapper.finishResponse()
    //#input(void finishResponse()): this
    //#input(void finishResponse()): this.stream
    //#input(void finishResponse()): this.writer
    //#pre[5] (void finishResponse()): (soft) init'ed(this.stream)
    //#pre[6] (void finishResponse()): (soft) init'ed(this.writer)
    //#test_vector(void finishResponse()): this.stream: Addr_Set{null}, Inverse{null}
    //#test_vector(void finishResponse()): this.writer: Addr_Set{null}, Inverse{null}
        writer.close();
      } else {
        if (stream != null) {
          stream.close();
        }
      }
    } catch (IOException e) {
    }
  }
    //#gzipresponsewrapper.java:67: end of method: void net.sourceforge.pebble.web.filter.GZIPResponseWrapper.finishResponse()

  public void flushBuffer() throws IOException {
	if (stream != null) {
    //#gzipresponsewrapper.java:70: method: void net.sourceforge.pebble.web.filter.GZIPResponseWrapper.flushBuffer()
    //#input(void flushBuffer()): this
    //#input(void flushBuffer()): this.stream
    //#pre[2] (void flushBuffer()): init'ed(this.stream)
    //#test_vector(void flushBuffer()): this.stream: Addr_Set{null}, Inverse{null}
	  stream.flush();
	}
  }
    //#gzipresponsewrapper.java:73: end of method: void net.sourceforge.pebble.web.filter.GZIPResponseWrapper.flushBuffer()

  public ServletOutputStream getOutputStream() throws IOException {
    if (writer != null) {
    //#gzipresponsewrapper.java:76: method: ServletOutputStream net.sourceforge.pebble.web.filter.GZIPResponseWrapper.getOutputStream()
    //#input(ServletOutputStream getOutputStream()): __Descendant_Table[net/sourceforge/pebble/web/filter/GZIPResponseWrapper]
    //#input(ServletOutputStream getOutputStream()): __Descendant_Table[others]
    //#input(ServletOutputStream getOutputStream()): __Dispatch_Table.createOutputStream()Ljavax/servlet/ServletOutputStream;
    //#input(ServletOutputStream getOutputStream()): this
    //#input(ServletOutputStream getOutputStream()): this.__Tag
    //#input(ServletOutputStream getOutputStream()): this.stream
    //#input(ServletOutputStream getOutputStream()): this.wrappedResponse
    //#input(ServletOutputStream getOutputStream()): this.writer
    //#output(ServletOutputStream getOutputStream()): new ByteArrayOutputStream(GZIPResponseStream#1) num objects
    //#output(ServletOutputStream getOutputStream()): new GZIPOutputStream(GZIPResponseStream#2) num objects
    //#output(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1) num objects
    //#output(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).__Tag
    //#output(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).baos
    //#output(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).closed
    //#output(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).gzipstream
    //#output(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).output
    //#output(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).response
    //#output(ServletOutputStream getOutputStream()): return_value
    //#output(ServletOutputStream getOutputStream()): this.stream
    //#new obj(ServletOutputStream getOutputStream()): new ByteArrayOutputStream(GZIPResponseStream#1)
    //#new obj(ServletOutputStream getOutputStream()): new GZIPOutputStream(GZIPResponseStream#2)
    //#new obj(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1)
    //#pre[1] (ServletOutputStream getOutputStream()): init'ed(this.stream)
    //#pre[5] (ServletOutputStream getOutputStream()): this.writer == null
    //#pre[3] (ServletOutputStream getOutputStream()): (soft) this.__Tag == net/sourceforge/pebble/web/filter/GZIPResponseWrapper
    //#pre[4] (ServletOutputStream getOutputStream()): (soft) this.wrappedResponse != null
    //#post(ServletOutputStream getOutputStream()): return_value == One-of{old this.stream, &new GZIPResponseStream(createOutputStream#1)}
    //#post(ServletOutputStream getOutputStream()): return_value != null
    //#post(ServletOutputStream getOutputStream()): this.stream == return_value
    //#post(ServletOutputStream getOutputStream()): new ByteArrayOutputStream(GZIPResponseStream#1) num objects <= 1
    //#post(ServletOutputStream getOutputStream()): new GZIPOutputStream(GZIPResponseStream#2) num objects <= 1
    //#post(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1) num objects <= 1
    //#post(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).__Tag == net/sourceforge/pebble/web/filter/GZIPResponseStream
    //#post(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).baos == &new ByteArrayOutputStream(GZIPResponseStream#1)
    //#post(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).closed == 0
    //#post(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).gzipstream == &new GZIPOutputStream(GZIPResponseStream#2)
    //#post(ServletOutputStream getOutputStream()): init'ed(new GZIPResponseStream(createOutputStream#1).output)
    //#post(ServletOutputStream getOutputStream()): new GZIPResponseStream(createOutputStream#1).response == this.wrappedResponse
    //#post(ServletOutputStream getOutputStream()): (soft) new GZIPResponseStream(createOutputStream#1).response != null
    //#unanalyzed(ServletOutputStream getOutputStream()): Effects-of-calling:javax.servlet.ServletOutputStream
    //#unanalyzed(ServletOutputStream getOutputStream()): Effects-of-calling:javax.servlet.http.HttpServletResponse:getOutputStream
    //#unanalyzed(ServletOutputStream getOutputStream()): Effects-of-calling:java.io.ByteArrayOutputStream
    //#unanalyzed(ServletOutputStream getOutputStream()): Effects-of-calling:java.util.zip.GZIPOutputStream
    //#test_vector(ServletOutputStream getOutputStream()): this.stream: Inverse{null}, Addr_Set{null}
      throw new IllegalStateException("getWriter() has already been called!");
    }

    if (stream == null)
      stream = createOutputStream();
    return (stream);
    //#gzipresponsewrapper.java:82: end of method: ServletOutputStream net.sourceforge.pebble.web.filter.GZIPResponseWrapper.getOutputStream()
  }

  public PrintWriter getWriter() throws IOException {
    if (writer != null) {
    //#gzipresponsewrapper.java:86: method: PrintWriter net.sourceforge.pebble.web.filter.GZIPResponseWrapper.getWriter()
    //#input(PrintWriter getWriter()): __Descendant_Table[net/sourceforge/pebble/web/filter/GZIPResponseWrapper]
    //#input(PrintWriter getWriter()): __Descendant_Table[others]
    //#input(PrintWriter getWriter()): __Dispatch_Table.createOutputStream()Ljavax/servlet/ServletOutputStream;
    //#input(PrintWriter getWriter()): this
    //#input(PrintWriter getWriter()): this.__Tag
    //#input(PrintWriter getWriter()): this.stream
    //#input(PrintWriter getWriter()): this.wrappedResponse
    //#input(PrintWriter getWriter()): this.writer
    //#output(PrintWriter getWriter()): new ByteArrayOutputStream(GZIPResponseStream#1) num objects
    //#output(PrintWriter getWriter()): new GZIPOutputStream(GZIPResponseStream#2) num objects
    //#output(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1) num objects
    //#output(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1).__Tag
    //#output(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1).baos
    //#output(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1).closed
    //#output(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1).gzipstream
    //#output(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1).output
    //#output(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1).response
    //#output(PrintWriter getWriter()): new PrintWriter(getWriter#1) num objects
    //#output(PrintWriter getWriter()): return_value
    //#output(PrintWriter getWriter()): this.stream
    //#output(PrintWriter getWriter()): this.writer
    //#new obj(PrintWriter getWriter()): new ByteArrayOutputStream(GZIPResponseStream#1)
    //#new obj(PrintWriter getWriter()): new GZIPOutputStream(GZIPResponseStream#2)
    //#new obj(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1)
    //#new obj(PrintWriter getWriter()): new PrintWriter(getWriter#1)
    //#pre[2] (PrintWriter getWriter()): init'ed(this.writer)
    //#pre[1] (PrintWriter getWriter()): (soft) this.stream == null
    //#pre[4] (PrintWriter getWriter()): (soft) this.__Tag == net/sourceforge/pebble/web/filter/GZIPResponseWrapper
    //#pre[5] (PrintWriter getWriter()): (soft) this.wrappedResponse != null
    //#post(PrintWriter getWriter()): return_value == One-of{old this.writer, &new PrintWriter(getWriter#1)}
    //#post(PrintWriter getWriter()): return_value != null
    //#post(PrintWriter getWriter()): this.stream == One-of{old this.stream, &new GZIPResponseStream(createOutputStream#1)}
    //#post(PrintWriter getWriter()): (soft) this.stream in Addr_Set{null,&new GZIPResponseStream(createOutputStream#1)}
    //#post(PrintWriter getWriter()): this.writer == One-of{old this.writer, &new PrintWriter(getWriter#1)}
    //#post(PrintWriter getWriter()): this.writer != null
    //#post(PrintWriter getWriter()): new ByteArrayOutputStream(GZIPResponseStream#1) num objects <= 1
    //#post(PrintWriter getWriter()): new GZIPOutputStream(GZIPResponseStream#2) num objects <= 1
    //#post(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1) num objects <= 1
    //#post(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1).__Tag == net/sourceforge/pebble/web/filter/GZIPResponseStream
    //#post(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1).baos == &new ByteArrayOutputStream(GZIPResponseStream#1)
    //#post(PrintWriter getWriter()): init'ed(new GZIPResponseStream(createOutputStream#1).closed)
    //#post(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1).gzipstream == &new GZIPOutputStream(GZIPResponseStream#2)
    //#post(PrintWriter getWriter()): init'ed(new GZIPResponseStream(createOutputStream#1).output)
    //#post(PrintWriter getWriter()): new GZIPResponseStream(createOutputStream#1).response == this.wrappedResponse
    //#post(PrintWriter getWriter()): (soft) new GZIPResponseStream(createOutputStream#1).response != null
    //#post(PrintWriter getWriter()): new PrintWriter(getWriter#1) num objects <= 1
    //#unanalyzed(PrintWriter getWriter()): Effects-of-calling:javax.servlet.ServletOutputStream
    //#unanalyzed(PrintWriter getWriter()): Effects-of-calling:javax.servlet.http.HttpServletResponse:getOutputStream
    //#unanalyzed(PrintWriter getWriter()): Effects-of-calling:java.io.ByteArrayOutputStream
    //#unanalyzed(PrintWriter getWriter()): Effects-of-calling:java.util.zip.GZIPOutputStream
    //#test_vector(PrintWriter getWriter()): this.writer: Addr_Set{null}, Inverse{null}
      return (writer);
    }

    if (stream != null) {
      throw new IllegalStateException("getOutputStream() has already been called!");
    }

    stream = createOutputStream();
    writer = new PrintWriter(new OutputStreamWriter(stream, "UTF-8"));
    return (writer);
    //#gzipresponsewrapper.java:96: end of method: PrintWriter net.sourceforge.pebble.web.filter.GZIPResponseWrapper.getWriter()
  }

  public void setContentLength(int length) {
  }
    //#gzipresponsewrapper.java:100: method: void net.sourceforge.pebble.web.filter.GZIPResponseWrapper.setContentLength(int)
    //#gzipresponsewrapper.java:100: end of method: void net.sourceforge.pebble.web.filter.GZIPResponseWrapper.setContentLength(int)

}
    //#output(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Descendant_Table[net/sourceforge/pebble/web/filter/GZIPResponseWrapper]
    //#output(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.createOutputStream()Ljavax/servlet/ServletOutputStream;
    //#output(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.finishResponse()V
    //#output(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.flushBuffer()V
    //#output(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.getOutputStream()Ljavax/servlet/ServletOutputStream;
    //#output(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.getWriter()Ljava/io/PrintWriter;
    //#output(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.setContentLength(I)V
    //#post(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Descendant_Table[net/sourceforge/pebble/web/filter/GZIPResponseWrapper] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.createOutputStream()Ljavax/servlet/ServletOutputStream; == &createOutputStream
    //#post(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.finishResponse()V == &finishResponse
    //#post(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.flushBuffer()V == &flushBuffer
    //#post(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.getOutputStream()Ljavax/servlet/ServletOutputStream; == &getOutputStream
    //#post(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.getWriter()Ljava/io/PrintWriter; == &getWriter
    //#post(net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init): __Dispatch_Table.setContentLength(I)V == &setContentLength
    //#gzipresponsewrapper.java:: end of method: net.sourceforge.pebble.web.filter.GZIPResponseWrapper.net.sourceforge.pebble.web.filter.GZIPResponseWrapper__static_init
    //#gzipresponsewrapper.java:: end of class: net.sourceforge.pebble.web.filter.GZIPResponseWrapper
