//# 0 errors, 335 messages
//#
/*
    //#CompressionFilter.java:1:1: class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper
    //#CompressionFilter.java:1:1: method: org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init
    //#CompressionFilter.java:1:1: class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper
    //#CompressionFilter.java:1:1: method: org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init
    //#CompressionFilter.java:1:1: class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter
* Licensed to the Apache Software Foundation (ASF) under one or more
*  contributor license agreements.  The ASF licenses this file to You
* under the Apache License, Version 2.0 (the "License"); you may not
* use this file except in compliance with the License.
* You may obtain a copy of the License at
*
*     http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.  For additional information regarding
* copyright in this work, please see the NOTICE file in the top level
* directory of this distribution.
*/

package org.apache.roller.weblogger.ui.core.filters;

import java.io.ByteArrayOutputStream;
import java.io.IOException;
import java.io.OutputStream;
import java.io.OutputStreamWriter;
import java.io.PrintWriter;
import java.util.zip.GZIPOutputStream;
import javax.servlet.Filter;
import javax.servlet.FilterChain;
import javax.servlet.FilterConfig;
import javax.servlet.ServletException;
import javax.servlet.ServletOutputStream;
import javax.servlet.ServletRequest;
import javax.servlet.ServletResponse;
import javax.servlet.http.HttpServletRequest;
import javax.servlet.http.HttpServletResponse;
import javax.servlet.http.HttpServletResponseWrapper;
import org.apache.commons.logging.Log;
import org.apache.commons.logging.LogFactory;
import org.apache.roller.weblogger.config.WebloggerConfig;


/** 
 * Filter that compresses output with gzip (assuming that browser supports gzip).
 * <P>
 * Taken from More Servlets and JavaServer Pages from Prentice Hall and 
 * Sun Microsystems Press, http://www.moreservlets.com/.
 * &copy; 2002 Marty Hall; may be freely used or adapted.
 */
public class CompressionFilter implements Filter {
    //#CompressionFilter.java:49: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter.org.apache.roller.weblogger.ui.core.filters.CompressionFilter()
    //#input(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter()): this
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter()): this.enabled
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter()): this.enabled == 1
    
    private static Log log = LogFactory.getLog(CompressionFilter.class);
    //#CompressionFilter.java:51: method: org.apache.roller.weblogger.ui.core.filters.CompressionFilter.org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init
    //#CompressionFilter.java:51: Warning: method not available
    //#    -- call on Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter
    //#    method: org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init
    //#    unanalyzed callee: Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): __Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter]
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): __Dispatch_Table.destroy()V
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): __Dispatch_Table.doFilter(Ljavax/servlet/ServletRequest;Ljavax/servlet/ServletResponse;Ljavax/servlet/FilterChain;)V
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): __Dispatch_Table.init(Ljavax/servlet/FilterConfig;)V
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): __Dispatch_Table.isGzipSupported(Ljavax/servlet/http/HttpServletRequest;)Z
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): log
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): __Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): __Dispatch_Table.destroy()V == &destroy
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): __Dispatch_Table.doFilter(Ljavax/servlet/ServletRequest;Ljavax/servlet/ServletResponse;Ljavax/servlet/FilterChain;)V == &doFilter
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): __Dispatch_Table.init(Ljavax/servlet/FilterConfig;)V == &init
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): __Dispatch_Table.isGzipSupported(Ljavax/servlet/http/HttpServletRequest;)Z == &isGzipSupported
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init): init'ed(log)
    //#CompressionFilter.java:51: end of method: org.apache.roller.weblogger.ui.core.filters.CompressionFilter.org.apache.roller.weblogger.ui.core.filters.CompressionFilter__static_init
    
    private boolean enabled = true;
    
    
    /** 
     * If browser does not support gzip, invoke resource normally. If browser 
     * does support gzip, set the Content-Encoding response header and invoke 
     * resource with a wrapped response that collects all the output. Extract 
     * the output and write it into a gzipped byte array. Finally, write that 
     * array to the client's output stream.
     */
    public void doFilter(ServletRequest request, ServletResponse response, FilterChain chain)
            throws ServletException, IOException {
        
        HttpServletRequest req = (HttpServletRequest) request;
    //#CompressionFilter.java:66: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter.doFilter(ServletRequest, ServletResponse, FilterChain)
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): "Content-Encoding"._tainted
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): "Gzip size:"._tainted
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): "Pre-zip size:"._tainted
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): "gzip"._tainted
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): chain
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): log
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper]
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Descendant_Table[others]
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Dispatch_Table.clear()V
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Dispatch_Table.close()V
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Dispatch_Table.getByteArrayStream()Ljava/io/ByteArrayOutputStream;
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Dispatch_Table.processStream()V
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Dispatch_Table.setFinallized()V
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayResponseWrapper.__Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayResponseWrapper]
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayResponseWrapper.__Dispatch_Table.getByteArrayOutputStream()Ljava/io/ByteArrayOutputStream;
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayResponseWrapper.__Dispatch_Table.getOutputStream()Ljavax/servlet/ServletOutputStream;
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): request
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): response
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): this
    //#input(void doFilter(ServletRequest, ServletResponse, FilterChain)): this.enabled
    //#pre[1] (void doFilter(ServletRequest, ServletResponse, FilterChain)): chain != null
    //#pre[6] (void doFilter(ServletRequest, ServletResponse, FilterChain)): init'ed(this.enabled)
    //#pre[2] (void doFilter(ServletRequest, ServletResponse, FilterChain)): (soft) log != null
    //#pre[3] (void doFilter(ServletRequest, ServletResponse, FilterChain)): (soft) request != null
    //#pre[4] (void doFilter(ServletRequest, ServletResponse, FilterChain)): (soft) response != null
    //#presumption(void doFilter(ServletRequest, ServletResponse, FilterChain)): javax.servlet.ServletResponse:getOutputStream(...)@150 != null
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:javax.servlet.http.HttpServletRequest:getHeader
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:javax.servlet.http.HttpServletResponseWrapper
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:javax.servlet.ServletResponse:getOutputStream
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:javax.servlet.ServletOutputStream
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:java.io.ByteArrayOutputStream
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:java.io.OutputStreamWriter
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:java.io.PrintWriter
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:java.io.ByteArrayOutputStream:toByteArray
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:java.io.OutputStream:write
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:java.io.OutputStream:flush
    //#unanalyzed(void doFilter(ServletRequest, ServletResponse, FilterChain)): Effects-of-calling:java.io.OutputStream:close
    //#test_vector(void doFilter(ServletRequest, ServletResponse, FilterChain)): this.enabled: {0}, {1}
        HttpServletResponse res = (HttpServletResponse) response;
        
        if (!this.enabled || !isGzipSupported(req)) {
            // Invoke resource normally.
            chain.doFilter(req, res);
        } else {
            // Tell browser we are sending it gzipped data.
            res.setHeader("Content-Encoding", "gzip");
            
            // Invoke resource, accumulating output in the wrapper.
            ByteArrayResponseWrapper responseWrapper =
                    new ByteArrayResponseWrapper(response);
            
            chain.doFilter(req, responseWrapper);
            
            ByteArrayOutputStream outputStream = responseWrapper.getByteArrayOutputStream();
            
            // Get character array representing output.
            log.debug("Pre-zip size:" + outputStream.size());
    //#CompressionFilter.java:85: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter
    //#    method: void doFilter(ServletRequest, ServletResponse, FilterChain)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
            
            // Make a writer that compresses data and puts
            // it into a byte array.
            ByteArrayOutputStream byteStream = new ByteArrayOutputStream();
            GZIPOutputStream zipOut = new GZIPOutputStream(byteStream);
            
            // Compress original output and put it into byte array.
            zipOut.write(responseWrapper.getByteArrayOutputStream().toByteArray());
            
            // Gzip streams must be explicitly closed.
            zipOut.close();
            
            log.debug("Gzip size:" + byteStream.size());
    //#CompressionFilter.java:98: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter
    //#    method: void doFilter(ServletRequest, ServletResponse, FilterChain)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
            
            // Update the Content-Length header.
            res.setContentLength(byteStream.size());
            
            ByteArrayOutputStreamWrapper newOut =
                    (ByteArrayOutputStreamWrapper) responseWrapper.getOutputStream();
            newOut.clear();
            newOut.setFinallized();
            
            /* now force close of OutputStream */
            newOut.write(byteStream.toByteArray());
    //#CompressionFilter.java:109: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper:write(byte[])
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter
    //#    method: void doFilter(ServletRequest, ServletResponse, FilterChain)
    //#    unanalyzed callee: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper:write(byte[])
            newOut.close();
        }
        
    }
    //#CompressionFilter.java:113: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter.doFilter(ServletRequest, ServletResponse, FilterChain)
    

    public void init(FilterConfig config) throws ServletException {
        
        // is compression enabled?
        if(WebloggerConfig.getBooleanProperty("compression.gzipResponse.enabled")) {
    //#CompressionFilter.java:119: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter.init(FilterConfig)
    //#CompressionFilter.java:119: Warning: method not available
    //#    -- call on bool org.apache.roller.weblogger.config.WebloggerConfig:getBooleanProperty(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter
    //#    method: void init(FilterConfig)
    //#    unanalyzed callee: bool org.apache.roller.weblogger.config.WebloggerConfig:getBooleanProperty(String)
    //#input(void init(FilterConfig)): log
    //#input(void init(FilterConfig)): this
    //#output(void init(FilterConfig)): this.enabled
    //#pre[1] (void init(FilterConfig)): log != null
    //#post(void init(FilterConfig)): init'ed(this.enabled)
    //#test_vector(void init(FilterConfig)): org.apache.roller.weblogger.config.WebloggerConfig:getBooleanProperty(...)@119: {0}, {1}
            this.enabled = true;
            log.info("Compressed Output ENABLED");
    //#CompressionFilter.java:121: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:info(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter
    //#    method: void init(FilterConfig)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:info(Object)
        } else {
            this.enabled = false;
            log.info("Compressed Output DISABLED");
    //#CompressionFilter.java:124: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:info(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter
    //#    method: void init(FilterConfig)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:info(Object)
        }
    }
    //#CompressionFilter.java:126: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter.init(FilterConfig)
    
    
    public void destroy() {}
    //#CompressionFilter.java:129: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter.destroy()
    //#CompressionFilter.java:129: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter.destroy()
    
    
    private boolean isGzipSupported(HttpServletRequest req) {
        String browserEncodings = req.getHeader("Accept-Encoding");
    //#CompressionFilter.java:133: method: bool org.apache.roller.weblogger.ui.core.filters.CompressionFilter.isGzipSupported(HttpServletRequest)
    //#input(bool isGzipSupported(HttpServletRequest)): req
    //#output(bool isGzipSupported(HttpServletRequest)): return_value
    //#pre[1] (bool isGzipSupported(HttpServletRequest)): req != null
    //#post(bool isGzipSupported(HttpServletRequest)): init'ed(return_value)
        return ((browserEncodings != null)
    //#CompressionFilter.java:134: end of method: bool org.apache.roller.weblogger.ui.core.filters.CompressionFilter.isGzipSupported(HttpServletRequest)
                    && (browserEncodings.indexOf("gzip") != -1));
    }
    
    
    /**
     * Implementation of HttpServletResponseWrapper that supports caching.
     */
    private class ByteArrayResponseWrapper extends HttpServletResponseWrapper {
        
        private PrintWriter tpWriter;
        private ByteArrayOutputStreamWrapper tpStream;
        
        
        public ByteArrayResponseWrapper(ServletResponse inResp) throws IOException {
    //#CompressionFilter.java:148: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)
    //#input(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): Param_1
    //#input(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): inResp
    //#input(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1) num objects
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): new CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter$ByteArrayResponseWrapper#1) num objects
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream.__Tag
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream.baStream
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream.finallized
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream.flushOnFinalizeOnly
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream.intStream
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream.this$0
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): new PrintWriter(CompressionFilter$ByteArrayResponseWrapper#2) num objects
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.this$0
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpWriter
    //#new obj(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1)
    //#new obj(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): new CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter$ByteArrayResponseWrapper#1)
    //#new obj(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): new PrintWriter(CompressionFilter$ByteArrayResponseWrapper#2)
    //#pre[2] (void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): inResp != null
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.this$0 == Param_1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): init'ed(this.this$0)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream.this$0 == this.this$0
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream == &new CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter$ByteArrayResponseWrapper#1)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpWriter == &new PrintWriter(CompressionFilter$ByteArrayResponseWrapper#2)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1) num objects == 1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): new CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter$ByteArrayResponseWrapper#1) num objects == 1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream.flushOnFinalizeOnly == 1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): new PrintWriter(CompressionFilter$ByteArrayResponseWrapper#2) num objects == 1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream.__Tag == org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): this.tpStream.baStream == &new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): init'ed(this.tpStream.finallized)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): init'ed(this.tpStream.intStream)
    //#unanalyzed(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): Effects-of-calling:javax.servlet.ServletOutputStream
    //#unanalyzed(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)): Effects-of-calling:java.io.ByteArrayOutputStream
            super((HttpServletResponse) inResp);
            tpStream = new ByteArrayOutputStreamWrapper(inResp.getOutputStream());
            tpWriter = new PrintWriter(new OutputStreamWriter(tpStream,"UTF-8"));
        }
    //#CompressionFilter.java:152: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper(CompressionFilter, ServletResponse)
        
        
        public ServletOutputStream getOutputStream() throws IOException {
            return tpStream;
    //#CompressionFilter.java:156: method: ServletOutputStream org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.getOutputStream()
    //#input(ServletOutputStream getOutputStream()): this
    //#input(ServletOutputStream getOutputStream()): this.tpStream
    //#output(ServletOutputStream getOutputStream()): return_value
    //#pre[2] (ServletOutputStream getOutputStream()): init'ed(this.tpStream)
    //#post(ServletOutputStream getOutputStream()): return_value == this.tpStream
    //#post(ServletOutputStream getOutputStream()): init'ed(return_value)
    //#CompressionFilter.java:156: end of method: ServletOutputStream org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.getOutputStream()
        }
        
        public PrintWriter getWriter() throws IOException {
            return tpWriter;
    //#CompressionFilter.java:160: method: PrintWriter org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.getWriter()
    //#input(PrintWriter getWriter()): this
    //#input(PrintWriter getWriter()): this.tpWriter
    //#output(PrintWriter getWriter()): return_value
    //#pre[2] (PrintWriter getWriter()): init'ed(this.tpWriter)
    //#post(PrintWriter getWriter()): return_value == this.tpWriter
    //#post(PrintWriter getWriter()): init'ed(return_value)
    //#CompressionFilter.java:160: end of method: PrintWriter org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.getWriter()
        }
        
        /**
         * Get a String representation of the entire buffer.
         */
        public String toString() {
            return tpStream.getByteArrayStream().toString();
    //#CompressionFilter.java:167: method: String org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.toString()
    //#input(String toString()): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper]
    //#input(String toString()): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Descendant_Table[others]
    //#input(String toString()): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Dispatch_Table.getByteArrayStream()Ljava/io/ByteArrayOutputStream;
    //#input(String toString()): this
    //#input(String toString()): this.tpStream
    //#input(String toString()): this.tpStream.__Tag
    //#input(String toString()): this.tpStream.baStream
    //#input(String toString()): this.tpStream.baStream._tainted
    //#output(String toString()): java.io.ByteArrayOutputStream:toString(...)._tainted
    //#output(String toString()): return_value
    //#new obj(String toString()): java.io.ByteArrayOutputStream:toString(...)
    //#pre[2] (String toString()): this.tpStream != null
    //#pre[3] (String toString()): this.tpStream.__Tag == org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper
    //#pre[4] (String toString()): this.tpStream.baStream != null
    //#post(String toString()): java.io.ByteArrayOutputStream:toString(...)._tainted == this.tpStream.baStream._tainted
    //#post(String toString()): init'ed(java.io.ByteArrayOutputStream:toString(...)._tainted)
    //#post(String toString()): return_value == &java.io.ByteArrayOutputStream:toString(...)
    //#CompressionFilter.java:167: end of method: String org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.toString()
        }
        
        public ByteArrayOutputStream getByteArrayOutputStream() throws IOException {
            return tpStream.getByteArrayStream();
    //#CompressionFilter.java:171: method: ByteArrayOutputStream org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.getByteArrayOutputStream()
    //#input(ByteArrayOutputStream getByteArrayOutputStream()): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper]
    //#input(ByteArrayOutputStream getByteArrayOutputStream()): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Descendant_Table[others]
    //#input(ByteArrayOutputStream getByteArrayOutputStream()): org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper.__Dispatch_Table.getByteArrayStream()Ljava/io/ByteArrayOutputStream;
    //#input(ByteArrayOutputStream getByteArrayOutputStream()): this
    //#input(ByteArrayOutputStream getByteArrayOutputStream()): this.tpStream
    //#input(ByteArrayOutputStream getByteArrayOutputStream()): this.tpStream.__Tag
    //#input(ByteArrayOutputStream getByteArrayOutputStream()): this.tpStream.baStream
    //#output(ByteArrayOutputStream getByteArrayOutputStream()): return_value
    //#pre[2] (ByteArrayOutputStream getByteArrayOutputStream()): this.tpStream != null
    //#pre[3] (ByteArrayOutputStream getByteArrayOutputStream()): this.tpStream.__Tag == org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper
    //#pre[4] (ByteArrayOutputStream getByteArrayOutputStream()): init'ed(this.tpStream.baStream)
    //#post(ByteArrayOutputStream getByteArrayOutputStream()): return_value == this.tpStream.baStream
    //#post(ByteArrayOutputStream getByteArrayOutputStream()): init'ed(return_value)
    //#CompressionFilter.java:171: end of method: ByteArrayOutputStream org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.getByteArrayOutputStream()
        }
        
    }
    
    
    /**
     * Implementation of ServletOutputStream that allows the filter to hold the
     * Response content for insertion into the cache.
     */
    private class ByteArrayOutputStreamWrapper extends ServletOutputStream {
    //#CompressionFilter.java:181: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter.org.apache.roller.weblogger.ui.core.filters.CompressionFilter()
        
        protected OutputStream intStream;
        protected ByteArrayOutputStream baStream;
        protected boolean finallized = false;
        protected boolean flushOnFinalizeOnly = true;
        
        
        public ByteArrayOutputStreamWrapper(OutputStream outStream) {
    //#CompressionFilter.java:189: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)
    //#input(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): Param_1
    //#input(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): outStream
    //#input(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1) num objects
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this.baStream
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this.finallized
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this.flushOnFinalizeOnly
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this.intStream
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this.this$0
    //#new obj(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this.baStream == &new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this.finallized == 0
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this.flushOnFinalizeOnly == 1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1) num objects == 1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this.intStream == outStream
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): init'ed(this.intStream)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): this.this$0 == Param_1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)): init'ed(this.this$0)
            intStream = outStream;
            baStream = new ByteArrayOutputStream();
        }
    //#CompressionFilter.java:192: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter, OutputStream)
        
        public ByteArrayOutputStreamWrapper() {
    //#CompressionFilter.java:194: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)
    //#input(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): Param_1
    //#input(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): java.lang.System.out
    //#input(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1) num objects
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this.baStream
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this.finallized
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this.flushOnFinalizeOnly
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this.intStream
    //#output(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this.this$0
    //#new obj(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1)
    //#presumption(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): init'ed(java.lang.System.out)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this.baStream == &new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this.finallized == 0
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this.flushOnFinalizeOnly == 1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): new ByteArrayOutputStream(CompressionFilter$ByteArrayOutputStreamWrapper#1) num objects == 1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this.intStream == java.lang.System.out
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): (soft) init'ed(this.intStream)
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): this.this$0 == Param_1
    //#post(void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)): init'ed(this.this$0)
            intStream = System.out;
            baStream = new ByteArrayOutputStream();
        }
    //#CompressionFilter.java:197: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper(CompressionFilter)
        
        
        public ByteArrayOutputStream getByteArrayStream() {
            return baStream;
    //#CompressionFilter.java:201: method: ByteArrayOutputStream org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.getByteArrayStream()
    //#input(ByteArrayOutputStream getByteArrayStream()): this
    //#input(ByteArrayOutputStream getByteArrayStream()): this.baStream
    //#output(ByteArrayOutputStream getByteArrayStream()): return_value
    //#pre[2] (ByteArrayOutputStream getByteArrayStream()): init'ed(this.baStream)
    //#post(ByteArrayOutputStream getByteArrayStream()): return_value == this.baStream
    //#post(ByteArrayOutputStream getByteArrayStream()): init'ed(return_value)
    //#CompressionFilter.java:201: end of method: ByteArrayOutputStream org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.getByteArrayStream()
        }
        
        public void setFinallized() {
            finallized = true;
    //#CompressionFilter.java:205: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.setFinallized()
    //#input(void setFinallized()): this
    //#output(void setFinallized()): this.finallized
    //#post(void setFinallized()): this.finallized == 1
        }
    //#CompressionFilter.java:206: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.setFinallized()
        
        public boolean isFinallized() {
            return finallized;
    //#CompressionFilter.java:209: method: bool org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.isFinallized()
    //#input(bool isFinallized()): this
    //#input(bool isFinallized()): this.finallized
    //#output(bool isFinallized()): return_value
    //#pre[2] (bool isFinallized()): init'ed(this.finallized)
    //#post(bool isFinallized()): return_value == this.finallized
    //#post(bool isFinallized()): init'ed(return_value)
    //#CompressionFilter.java:209: end of method: bool org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.isFinallized()
        }
        
        
        public void write(int i) throws java.io.IOException {
            baStream.write(i);
    //#CompressionFilter.java:214: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.write(int)
    //#input(void write(int)): i
    //#input(void write(int)): this
    //#input(void write(int)): this.baStream
    //#pre[3] (void write(int)): this.baStream != null
        }
    //#CompressionFilter.java:215: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.write(int)
        
        public void close() throws java.io.IOException {
            if (finallized) {
    //#CompressionFilter.java:218: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.close()
    //#input(void close()): __Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper]
    //#input(void close()): __Descendant_Table[others]
    //#input(void close()): __Dispatch_Table.processStream()V
    //#input(void close()): this
    //#input(void close()): this.__Tag
    //#input(void close()): this.baStream
    //#input(void close()): this.finallized
    //#input(void close()): this.intStream
    //#pre[4] (void close()): init'ed(this.finallized)
    //#pre[2] (void close()): (soft) this.__Tag == org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper
    //#pre[3] (void close()): (soft) this.baStream != null
    //#pre[5] (void close()): (soft) this.intStream != null
    //#unanalyzed(void close()): Effects-of-calling:java.io.ByteArrayOutputStream:toByteArray
    //#unanalyzed(void close()): Effects-of-calling:java.io.OutputStream:write
    //#unanalyzed(void close()): Effects-of-calling:java.io.OutputStream:flush
    //#test_vector(void close()): this.finallized: {0}, {1}
                processStream();
                intStream.close();
            }
        }
    //#CompressionFilter.java:222: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.close()
        
        public void flush() throws java.io.IOException {
            if (baStream.size() != 0) {
    //#CompressionFilter.java:225: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.flush()
    //#input(void flush()): __Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper]
    //#input(void flush()): __Descendant_Table[others]
    //#input(void flush()): __Dispatch_Table.processStream()V
    //#input(void flush()): this
    //#input(void flush()): this.__Tag
    //#input(void flush()): this.baStream
    //#input(void flush()): this.finallized
    //#input(void flush()): this.flushOnFinalizeOnly
    //#input(void flush()): this.intStream
    //#output(void flush()): new ByteArrayOutputStream(flush#1) num objects
    //#output(void flush()): this.baStream
    //#new obj(void flush()): new ByteArrayOutputStream(flush#1)
    //#pre[1] (void flush()): this.baStream != null
    //#pre[3] (void flush()): (soft) this.__Tag == org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper
    //#pre[4] (void flush()): (soft) init'ed(this.finallized)
    //#pre[5] (void flush()): (soft) init'ed(this.flushOnFinalizeOnly)
    //#pre[6] (void flush()): (soft) this.intStream != null
    //#post(void flush()): this.baStream == One-of{old this.baStream, &new ByteArrayOutputStream(flush#1)}
    //#post(void flush()): this.baStream != null
    //#post(void flush()): new ByteArrayOutputStream(flush#1) num objects <= 1
    //#unanalyzed(void flush()): Effects-of-calling:java.io.ByteArrayOutputStream:toByteArray
    //#unanalyzed(void flush()): Effects-of-calling:java.io.OutputStream:write
    //#unanalyzed(void flush()): Effects-of-calling:java.io.OutputStream:flush
    //#test_vector(void flush()): this.finallized: {0}, {1}
    //#test_vector(void flush()): java.io.ByteArrayOutputStream:size(...)@225: {0}, {-2_147_483_648..-1, 1..4_294_967_295}
                if (!flushOnFinalizeOnly || finallized) {
                    processStream();
                    baStream = new ByteArrayOutputStream();
                }
            }
        }
    //#CompressionFilter.java:231: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.flush()
        
        protected void processStream() throws java.io.IOException {
            intStream.write(baStream.toByteArray());
    //#CompressionFilter.java:234: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.processStream()
    //#input(void processStream()): this
    //#input(void processStream()): this.baStream
    //#input(void processStream()): this.intStream
    //#pre[2] (void processStream()): this.baStream != null
    //#pre[3] (void processStream()): this.intStream != null
            intStream.flush();
        }
    //#CompressionFilter.java:236: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.processStream()
        
        public void clear() {
            baStream = new ByteArrayOutputStream();
    //#CompressionFilter.java:239: method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.clear()
    //#input(void clear()): this
    //#output(void clear()): new ByteArrayOutputStream(clear#1) num objects
    //#output(void clear()): this.baStream
    //#new obj(void clear()): new ByteArrayOutputStream(clear#1)
    //#post(void clear()): this.baStream == &new ByteArrayOutputStream(clear#1)
    //#post(void clear()): new ByteArrayOutputStream(clear#1) num objects == 1
        }
    //#CompressionFilter.java:240: end of method: void org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.clear()
        
    }

}
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper]
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.clear()V
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.close()V
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.flush()V
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.getByteArrayStream()Ljava/io/ByteArrayOutputStream;
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.isFinallized()Z
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.processStream()V
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.setFinallized()V
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.write(I)V
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayOutputStreamWrapper] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.clear()V == &clear
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.close()V == &close
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.flush()V == &flush
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.getByteArrayStream()Ljava/io/ByteArrayOutputStream; == &getByteArrayStream
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.isFinallized()Z == &isFinallized
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.processStream()V == &processStream
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.setFinallized()V == &setFinallized
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init): __Dispatch_Table.write(I)V == &write
    //#CompressionFilter.java:: end of method: org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper.org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper__static_init
    //#CompressionFilter.java:: end of class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayOutputStreamWrapper
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init): __Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayResponseWrapper]
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init): __Dispatch_Table.getByteArrayOutputStream()Ljava/io/ByteArrayOutputStream;
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init): __Dispatch_Table.getOutputStream()Ljavax/servlet/ServletOutputStream;
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init): __Dispatch_Table.getWriter()Ljava/io/PrintWriter;
    //#output(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init): __Dispatch_Table.toString()Ljava/lang/String;
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init): __Descendant_Table[org/apache/roller/weblogger/ui/core/filters/CompressionFilter$ByteArrayResponseWrapper] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init): __Dispatch_Table.getByteArrayOutputStream()Ljava/io/ByteArrayOutputStream; == &getByteArrayOutputStream
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init): __Dispatch_Table.getOutputStream()Ljavax/servlet/ServletOutputStream; == &getOutputStream
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init): __Dispatch_Table.getWriter()Ljava/io/PrintWriter; == &getWriter
    //#post(org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init): __Dispatch_Table.toString()Ljava/lang/String; == &toString
    //#CompressionFilter.java:: end of method: org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper.org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper__static_init
    //#CompressionFilter.java:: end of class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter$ByteArrayResponseWrapper
    //#CompressionFilter.java:: end of class: org.apache.roller.weblogger.ui.core.filters.CompressionFilter
