//# 0 errors, 221 messages
//#
/*
    //#ZipResourceManager.java:1:1: class: com.dmdirc.util.resourcemanager.ZipResourceManager
    //#ZipResourceManager.java:1:1: method: com.dmdirc.util.resourcemanager.ZipResourceManager.com.dmdirc.util.resourcemanager.ZipResourceManager__static_init
 * Copyright (c) 2006-2009 Chris Smith, Shane Mc Cormack, Gregory Holmes
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 * SOFTWARE.
 */

package com.dmdirc.util.resourcemanager;

import com.dmdirc.logger.ErrorLevel;
import com.dmdirc.logger.Logger;

import java.io.BufferedInputStream;
import java.io.IOException;
import java.io.InputStream;
import java.util.ArrayList;
import java.util.Enumeration;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.zip.ZipEntry;
import java.util.zip.ZipFile;

/**
 * Provides an easy way to access files inside a zip or jar.
 */
public final class ZipResourceManager extends ResourceManager {
    
    /** Zipfile instance. */
    private final ZipFile zipFile;
    
    /** Entries list. */
    private final List<String> entries;
    
    /**
     * Instantiates ZipResourceManager.
     *
     * @param filename Filename of the zip to load
     * @throws IOException Throw when the zip fails to load
     */
    protected ZipResourceManager(final String filename) throws IOException {
        super();
    //#ZipResourceManager.java:57: method: void com.dmdirc.util.resourcemanager.ZipResourceManager.com.dmdirc.util.resourcemanager.ZipResourceManager(String)
    //#input(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): filename
    //#input(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): this
    //#output(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): new ArrayList(ZipResourceManager#2) num objects
    //#output(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): new ZipFile(ZipResourceManager#1) num objects
    //#output(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): this.entries
    //#output(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): this.zipFile
    //#new obj(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): new ArrayList(ZipResourceManager#2)
    //#new obj(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): new ZipFile(ZipResourceManager#1)
    //#presumption(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): java.util.Enumeration:nextElement(...)@63 != null
    //#presumption(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): java.util.zip.ZipFile:entries(...)@61 != null
    //#post(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): this.entries == &new ArrayList(ZipResourceManager#2)
    //#post(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): this.zipFile == &new ZipFile(ZipResourceManager#1)
    //#post(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): new ArrayList(ZipResourceManager#2) num objects == 1
    //#post(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): new ZipFile(ZipResourceManager#1) num objects == 1
    //#test_vector(void com.dmdirc.util.resourcemanager.ZipResourceManager(String)): java.util.Enumeration:hasMoreElements(...)@62: {0}, {1}
        
        this.zipFile = new ZipFile(filename);
        entries = new ArrayList<String>();
        final Enumeration<? extends ZipEntry> zipEntries = zipFile.entries();
        while (zipEntries.hasMoreElements()) {
            entries.add(zipEntries.nextElement().getName());
        }
    }
    //#ZipResourceManager.java:65: end of method: void com.dmdirc.util.resourcemanager.ZipResourceManager.com.dmdirc.util.resourcemanager.ZipResourceManager(String)
    
    /**
     * Returns an instance of a ZipResourceManager for the specified file.
     *
     * @param filename Filename of the zip to load
     * 
     * @return ZipResourceManager instance
     * 
     * @throws IOException Throw when the zip fails to load
     */
    public static synchronized ZipResourceManager getInstance(final String filename) throws
            IOException {
        return new ZipResourceManager(filename);
    //#ZipResourceManager.java:78: method: ZipResourceManager com.dmdirc.util.resourcemanager.ZipResourceManager.getInstance(String)
    //#input(ZipResourceManager getInstance(String)): __Class_Obj.__Lock
    //#input(ZipResourceManager getInstance(String)): filename
    //#output(ZipResourceManager getInstance(String)): new ArrayList(ZipResourceManager#2) num objects
    //#output(ZipResourceManager getInstance(String)): new ZipFile(ZipResourceManager#1) num objects
    //#output(ZipResourceManager getInstance(String)): new ZipResourceManager(getInstance#1) num objects
    //#output(ZipResourceManager getInstance(String)): return_value.__Tag
    //#output(ZipResourceManager getInstance(String)): return_value.entries
    //#output(ZipResourceManager getInstance(String)): return_value.zipFile
    //#output(ZipResourceManager getInstance(String)): return_value
    //#new obj(ZipResourceManager getInstance(String)): new ArrayList(ZipResourceManager#2)
    //#new obj(ZipResourceManager getInstance(String)): new ZipFile(ZipResourceManager#1)
    //#new obj(ZipResourceManager getInstance(String)): new ZipResourceManager(getInstance#1)
    //#post(ZipResourceManager getInstance(String)): return_value == &new ZipResourceManager(getInstance#1)
    //#post(ZipResourceManager getInstance(String)): new ArrayList(ZipResourceManager#2) num objects == 1
    //#post(ZipResourceManager getInstance(String)): new ZipFile(ZipResourceManager#1) num objects == 1
    //#post(ZipResourceManager getInstance(String)): new ZipResourceManager(getInstance#1) num objects == 1
    //#post(ZipResourceManager getInstance(String)): return_value.__Tag == com/dmdirc/util/resourcemanager/ZipResourceManager
    //#post(ZipResourceManager getInstance(String)): return_value.entries == &new ArrayList(ZipResourceManager#2)
    //#post(ZipResourceManager getInstance(String)): return_value.zipFile == &new ZipFile(ZipResourceManager#1)
    //#unanalyzed(ZipResourceManager getInstance(String)): Effects-of-calling:java.util.zip.ZipFile
    //#unanalyzed(ZipResourceManager getInstance(String)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(ZipResourceManager getInstance(String)): Effects-of-calling:java.util.zip.ZipFile:entries
    //#unanalyzed(ZipResourceManager getInstance(String)): Effects-of-calling:java.util.Enumeration:hasMoreElements
    //#unanalyzed(ZipResourceManager getInstance(String)): Effects-of-calling:java.util.Enumeration:nextElement
    //#unanalyzed(ZipResourceManager getInstance(String)): Effects-of-calling:java.util.zip.ZipEntry:getName
    //#unanalyzed(ZipResourceManager getInstance(String)): Effects-of-calling:java.util.List:add
    //#ZipResourceManager.java:78: end of method: ZipResourceManager com.dmdirc.util.resourcemanager.ZipResourceManager.getInstance(String)
    }
    
    /** {@inheritDoc} */
    @Override
    public boolean resourceExists(final String resource) {
        final ZipEntry zipEntry = zipFile.getEntry(resource);        
    //#ZipResourceManager.java:84: method: bool com.dmdirc.util.resourcemanager.ZipResourceManager.resourceExists(String)
    //#input(bool resourceExists(String)): resource
    //#input(bool resourceExists(String)): this
    //#input(bool resourceExists(String)): this.zipFile
    //#output(bool resourceExists(String)): return_value
    //#pre[3] (bool resourceExists(String)): this.zipFile != null
    //#post(bool resourceExists(String)): init'ed(return_value)
        
        return zipEntry != null && !zipEntry.isDirectory();
    //#ZipResourceManager.java:86: end of method: bool com.dmdirc.util.resourcemanager.ZipResourceManager.resourceExists(String)
    }
    
    /** {@inheritDoc} */
    @Override
    public byte[] getResourceBytes(final String resource) {
        final ZipEntry zipEntry = zipFile.getEntry(resource);
    //#ZipResourceManager.java:92: method: byte[] com.dmdirc.util.resourcemanager.ZipResourceManager.getResourceBytes(String)
    //#input(byte[] getResourceBytes(String)): com.dmdirc.logger.ErrorLevel.LOW
    //#input(byte[] getResourceBytes(String)): resource
    //#input(byte[] getResourceBytes(String)): this
    //#input(byte[] getResourceBytes(String)): this.zipFile
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#1) num objects
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#1).length
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#2) num objects
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#2).length
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#3) num objects
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#3).length
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#5) num objects
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#5).length
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#6) num objects
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#6).length
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#7) num objects
    //#output(byte[] getResourceBytes(String)): new byte[](getResourceBytes#7).length
    //#output(byte[] getResourceBytes(String)): return_value
    //#new obj(byte[] getResourceBytes(String)): new byte[](getResourceBytes#1)
    //#new obj(byte[] getResourceBytes(String)): new byte[](getResourceBytes#2)
    //#new obj(byte[] getResourceBytes(String)): new byte[](getResourceBytes#3)
    //#new obj(byte[] getResourceBytes(String)): new byte[](getResourceBytes#5)
    //#new obj(byte[] getResourceBytes(String)): new byte[](getResourceBytes#6)
    //#new obj(byte[] getResourceBytes(String)): new byte[](getResourceBytes#7)
    //#pre[3] (byte[] getResourceBytes(String)): this.zipFile != null
    //#presumption(byte[] getResourceBytes(String)): init'ed(com.dmdirc.logger.ErrorLevel.LOW)
    //#presumption(byte[] getResourceBytes(String)): java.util.zip.ZipEntry:getSize(...)@104 >= 0
    //#post(byte[] getResourceBytes(String)): return_value in Addr_Set{&new byte[](getResourceBytes#3),&new byte[](getResourceBytes#6),&new byte[](getResourceBytes#7),&new byte[](getResourceBytes#5),&new byte[](getResourceBytes#2),&new byte[](getResourceBytes#1)}
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#1) num objects <= 1
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#1).length == 0
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#2) num objects <= 1
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#2).length == 0
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#3) num objects <= 1
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#3).length <= 18_446_744_073_709_551_615
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#5) num objects <= 1
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#5).length == 0
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#6) num objects <= 1
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#6).length == 0
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#7) num objects <= 1
    //#post(byte[] getResourceBytes(String)): new byte[](getResourceBytes#7).length == 0
    //#test_vector(byte[] getResourceBytes(String)): java.util.zip.ZipEntry:isDirectory(...)@100: {0}, {1}
    //#test_vector(byte[] getResourceBytes(String)): java.util.zip.ZipFile:getEntry(...)@92: Inverse{null}, Addr_Set{null}
        BufferedInputStream inputStream;
        
        
        if (zipEntry == null) {
            return new byte[0];
        }
        
        if (zipEntry.isDirectory()) {
            return new byte[0];
        }
        
        final byte[] bytes = new byte[(int) zipEntry.getSize()];
        
        try {
            inputStream =
                    new BufferedInputStream(zipFile.getInputStream(zipEntry));
        } catch (IOException ex) {
            return new byte[0];
        }
        
        try {
            if (inputStream.read(bytes) != bytes.length) {
                inputStream.close();
                return new byte[0];
            }
        } catch (IOException ex) {
            return new byte[0];
        }
        
        try {
            inputStream.close();
        } catch (IOException ex) {
            Logger.userError(ErrorLevel.LOW, "Unable to close stream");
    //#ZipResourceManager.java:125: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.logger.Logger:userError(ErrorLevel, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.util.resourcemanager.ZipResourceManager
    //#    method: byte[] getResourceBytes(String)
    //#    unanalyzed callee: void com.dmdirc.logger.Logger:userError(ErrorLevel, String)
        }
        
        return bytes;
    //#ZipResourceManager.java:128: end of method: byte[] com.dmdirc.util.resourcemanager.ZipResourceManager.getResourceBytes(String)
    }
    
    /** {@inheritDoc} */
    @Override
    public InputStream getResourceInputStream(final String resource) {
        final ZipEntry zipEntry = zipFile.getEntry(resource);
    //#ZipResourceManager.java:134: method: InputStream com.dmdirc.util.resourcemanager.ZipResourceManager.getResourceInputStream(String)
    //#input(InputStream getResourceInputStream(String)): resource
    //#input(InputStream getResourceInputStream(String)): this
    //#input(InputStream getResourceInputStream(String)): this.zipFile
    //#output(InputStream getResourceInputStream(String)): return_value
    //#pre[3] (InputStream getResourceInputStream(String)): this.zipFile != null
    //#post(InputStream getResourceInputStream(String)): init'ed(return_value)
    //#test_vector(InputStream getResourceInputStream(String)): java.util.zip.ZipFile:getEntry(...)@134: Inverse{null}, Addr_Set{null}
        
        if (zipEntry == null) {
            return null;
        }
        
        try {
            return zipFile.getInputStream(zipEntry);
        } catch (IOException ex) {
            return null;
    //#ZipResourceManager.java:143: end of method: InputStream com.dmdirc.util.resourcemanager.ZipResourceManager.getResourceInputStream(String)
        }
        
    }
    
    /** {@inheritDoc} */
    @Override
    public Map<String, byte[]> getResourcesEndingWithAsBytes(
            final String resourcesSuffix) {
        final Map<String, byte[]> resources = new HashMap<String, byte[]>();
    //#ZipResourceManager.java:152: method: Map com.dmdirc.util.resourcemanager.ZipResourceManager.getResourcesEndingWithAsBytes(String)
    //#input(Map getResourcesEndingWithAsBytes(String)): com.dmdirc.logger.ErrorLevel.LOW
    //#input(Map getResourcesEndingWithAsBytes(String)): resourcesSuffix
    //#input(Map getResourcesEndingWithAsBytes(String)): this
    //#input(Map getResourcesEndingWithAsBytes(String)): this.entries
    //#input(Map getResourcesEndingWithAsBytes(String)): this.zipFile
    //#output(Map getResourcesEndingWithAsBytes(String)): new HashMap(getResourcesEndingWithAsBytes#1) num objects
    //#output(Map getResourcesEndingWithAsBytes(String)): return_value
    //#new obj(Map getResourcesEndingWithAsBytes(String)): new HashMap(getResourcesEndingWithAsBytes#1)
    //#pre[3] (Map getResourcesEndingWithAsBytes(String)): this.entries != null
    //#pre[4] (Map getResourcesEndingWithAsBytes(String)): (soft) this.zipFile != null
    //#presumption(Map getResourcesEndingWithAsBytes(String)): java.util.Iterator:next(...)@154 != null
    //#post(Map getResourcesEndingWithAsBytes(String)): return_value == &new HashMap(getResourcesEndingWithAsBytes#1)
    //#post(Map getResourcesEndingWithAsBytes(String)): new HashMap(getResourcesEndingWithAsBytes#1) num objects == 1
    //#unanalyzed(Map getResourcesEndingWithAsBytes(String)): Effects-of-calling:java.util.zip.ZipFile:getEntry
    //#unanalyzed(Map getResourcesEndingWithAsBytes(String)): Effects-of-calling:java.util.zip.ZipEntry:isDirectory
    //#unanalyzed(Map getResourcesEndingWithAsBytes(String)): Effects-of-calling:java.util.zip.ZipEntry:getSize
    //#unanalyzed(Map getResourcesEndingWithAsBytes(String)): Effects-of-calling:java.util.zip.ZipFile:getInputStream
    //#unanalyzed(Map getResourcesEndingWithAsBytes(String)): Effects-of-calling:java.io.BufferedInputStream
    //#unanalyzed(Map getResourcesEndingWithAsBytes(String)): Effects-of-calling:java.io.BufferedInputStream:read
    //#unanalyzed(Map getResourcesEndingWithAsBytes(String)): Effects-of-calling:java.io.BufferedInputStream:close
    //#unanalyzed(Map getResourcesEndingWithAsBytes(String)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(Map getResourcesEndingWithAsBytes(String)): Effects-of-calling:com.dmdirc.logger.Logger:userError
    //#test_vector(Map getResourcesEndingWithAsBytes(String)): java.lang.String:endsWith(...)@155: {0}, {1}
    //#test_vector(Map getResourcesEndingWithAsBytes(String)): java.util.Iterator:hasNext(...)@154: {0}, {1}
        
        for (String entry : entries) {
            if (entry.endsWith(resourcesSuffix)) {
                resources.put(entry, getResourceBytes(entry));
            }
        }
        
        return resources;
    //#ZipResourceManager.java:160: end of method: Map com.dmdirc.util.resourcemanager.ZipResourceManager.getResourcesEndingWithAsBytes(String)
    }
    
    /** {@inheritDoc} */
    @Override
    public Map<String, byte[]> getResourcesStartingWithAsBytes(
            final String resourcesPrefix) {
        final Map<String, byte[]> resources = new HashMap<String, byte[]>();
    //#ZipResourceManager.java:167: method: Map com.dmdirc.util.resourcemanager.ZipResourceManager.getResourcesStartingWithAsBytes(String)
    //#input(Map getResourcesStartingWithAsBytes(String)): com.dmdirc.logger.ErrorLevel.LOW
    //#input(Map getResourcesStartingWithAsBytes(String)): resourcesPrefix
    //#input(Map getResourcesStartingWithAsBytes(String)): this
    //#input(Map getResourcesStartingWithAsBytes(String)): this.entries
    //#input(Map getResourcesStartingWithAsBytes(String)): this.zipFile
    //#output(Map getResourcesStartingWithAsBytes(String)): new HashMap(getResourcesStartingWithAsBytes#1) num objects
    //#output(Map getResourcesStartingWithAsBytes(String)): return_value
    //#new obj(Map getResourcesStartingWithAsBytes(String)): new HashMap(getResourcesStartingWithAsBytes#1)
    //#pre[3] (Map getResourcesStartingWithAsBytes(String)): this.entries != null
    //#pre[4] (Map getResourcesStartingWithAsBytes(String)): (soft) this.zipFile != null
    //#presumption(Map getResourcesStartingWithAsBytes(String)): java.util.Iterator:next(...)@169 != null
    //#post(Map getResourcesStartingWithAsBytes(String)): return_value == &new HashMap(getResourcesStartingWithAsBytes#1)
    //#post(Map getResourcesStartingWithAsBytes(String)): new HashMap(getResourcesStartingWithAsBytes#1) num objects == 1
    //#unanalyzed(Map getResourcesStartingWithAsBytes(String)): Effects-of-calling:java.util.zip.ZipFile:getEntry
    //#unanalyzed(Map getResourcesStartingWithAsBytes(String)): Effects-of-calling:java.util.zip.ZipEntry:isDirectory
    //#unanalyzed(Map getResourcesStartingWithAsBytes(String)): Effects-of-calling:java.util.zip.ZipEntry:getSize
    //#unanalyzed(Map getResourcesStartingWithAsBytes(String)): Effects-of-calling:java.util.zip.ZipFile:getInputStream
    //#unanalyzed(Map getResourcesStartingWithAsBytes(String)): Effects-of-calling:java.io.BufferedInputStream
    //#unanalyzed(Map getResourcesStartingWithAsBytes(String)): Effects-of-calling:java.io.BufferedInputStream:read
    //#unanalyzed(Map getResourcesStartingWithAsBytes(String)): Effects-of-calling:java.io.BufferedInputStream:close
    //#unanalyzed(Map getResourcesStartingWithAsBytes(String)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(Map getResourcesStartingWithAsBytes(String)): Effects-of-calling:com.dmdirc.logger.Logger:userError
    //#test_vector(Map getResourcesStartingWithAsBytes(String)): java.lang.String:startsWith(...)@170: {0}, {1}
    //#test_vector(Map getResourcesStartingWithAsBytes(String)): java.util.Iterator:hasNext(...)@169: {0}, {1}
        
        for (String entry : entries) {
            if (entry.startsWith(resourcesPrefix)) {
                resources.put(entry, getResourceBytes(entry));
            }
        }
        
        return resources;
    //#ZipResourceManager.java:175: end of method: Map com.dmdirc.util.resourcemanager.ZipResourceManager.getResourcesStartingWithAsBytes(String)
    }
    
    /** {@inheritDoc} */
    @Override
    public Map<String, InputStream> getResourcesStartingWithAsInputStreams(
            final String resourcesPrefix) {
        final Map<String, InputStream> resources =
    //#ZipResourceManager.java:182: method: Map com.dmdirc.util.resourcemanager.ZipResourceManager.getResourcesStartingWithAsInputStreams(String)
    //#input(Map getResourcesStartingWithAsInputStreams(String)): resourcesPrefix
    //#input(Map getResourcesStartingWithAsInputStreams(String)): this
    //#input(Map getResourcesStartingWithAsInputStreams(String)): this.entries
    //#input(Map getResourcesStartingWithAsInputStreams(String)): this.zipFile
    //#output(Map getResourcesStartingWithAsInputStreams(String)): new HashMap(getResourcesStartingWithAsInputStreams#1) num objects
    //#output(Map getResourcesStartingWithAsInputStreams(String)): return_value
    //#new obj(Map getResourcesStartingWithAsInputStreams(String)): new HashMap(getResourcesStartingWithAsInputStreams#1)
    //#pre[3] (Map getResourcesStartingWithAsInputStreams(String)): this.entries != null
    //#pre[4] (Map getResourcesStartingWithAsInputStreams(String)): (soft) this.zipFile != null
    //#presumption(Map getResourcesStartingWithAsInputStreams(String)): java.util.Iterator:next(...)@185 != null
    //#post(Map getResourcesStartingWithAsInputStreams(String)): return_value == &new HashMap(getResourcesStartingWithAsInputStreams#1)
    //#post(Map getResourcesStartingWithAsInputStreams(String)): new HashMap(getResourcesStartingWithAsInputStreams#1) num objects == 1
    //#unanalyzed(Map getResourcesStartingWithAsInputStreams(String)): Effects-of-calling:java.util.zip.ZipFile:getEntry
    //#unanalyzed(Map getResourcesStartingWithAsInputStreams(String)): Effects-of-calling:java.util.zip.ZipFile:getInputStream
    //#unanalyzed(Map getResourcesStartingWithAsInputStreams(String)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#test_vector(Map getResourcesStartingWithAsInputStreams(String)): java.lang.String:startsWith(...)@186: {0}, {1}
    //#test_vector(Map getResourcesStartingWithAsInputStreams(String)): java.util.Iterator:hasNext(...)@185: {0}, {1}
                new HashMap<String, InputStream>();
        
        for (String entry : entries) {
            if (entry.startsWith(resourcesPrefix)) {
                resources.put(entry, getResourceInputStream(entry));
            }
        }
        
        return resources;
    //#ZipResourceManager.java:191: end of method: Map com.dmdirc.util.resourcemanager.ZipResourceManager.getResourcesStartingWithAsInputStreams(String)
    }
    
    /** {@inheritDoc} */
    @Override
    public List<String> getResourcesStartingWith(final String resourcesPrefix) {
        final List<String> resources = new ArrayList<String>();
    //#ZipResourceManager.java:197: method: List com.dmdirc.util.resourcemanager.ZipResourceManager.getResourcesStartingWith(String)
    //#input(List getResourcesStartingWith(String)): resourcesPrefix
    //#input(List getResourcesStartingWith(String)): this
    //#input(List getResourcesStartingWith(String)): this.entries
    //#output(List getResourcesStartingWith(String)): new ArrayList(getResourcesStartingWith#1) num objects
    //#output(List getResourcesStartingWith(String)): return_value
    //#new obj(List getResourcesStartingWith(String)): new ArrayList(getResourcesStartingWith#1)
    //#pre[3] (List getResourcesStartingWith(String)): this.entries != null
    //#presumption(List getResourcesStartingWith(String)): java.util.Iterator:next(...)@199 != null
    //#post(List getResourcesStartingWith(String)): return_value == &new ArrayList(getResourcesStartingWith#1)
    //#post(List getResourcesStartingWith(String)): new ArrayList(getResourcesStartingWith#1) num objects == 1
    //#test_vector(List getResourcesStartingWith(String)): java.lang.String:startsWith(...)@200: {0}, {1}
    //#test_vector(List getResourcesStartingWith(String)): java.util.Iterator:hasNext(...)@199: {0}, {1}
        
        for (String entry : entries) {
            if (entry.startsWith(resourcesPrefix)) {
                resources.add(entry);
            }
        }
        
        return resources;
    //#ZipResourceManager.java:205: end of method: List com.dmdirc.util.resourcemanager.ZipResourceManager.getResourcesStartingWith(String)
    }
}

    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Descendant_Table[com/dmdirc/util/resourcemanager/ZipResourceManager]
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.extractResource(Ljava/lang/String;Ljava/lang/String;Z)Z
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.extractResources(Ljava/lang/String;Ljava/lang/String;)V
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.extractResources(Ljava/lang/String;Ljava/lang/String;Z)V
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourceBytes(Ljava/lang/String;)[B
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourceInputStream(Ljava/lang/String;)Ljava/io/InputStream;
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourcesEndingWithAsBytes(Ljava/lang/String;)Ljava/util/Map;
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourcesStartingWith(Ljava/lang/String;)Ljava/util/List;
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourcesStartingWithAsBytes(Ljava/lang/String;)Ljava/util/Map;
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourcesStartingWithAsInputStreams(Ljava/lang/String;)Ljava/util/Map;
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.resourceExists(Ljava/lang/String;)Z
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.resourceToFile([BLjava/io/File;)V
    //#output(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): com/dmdirc/util/resourcemanager/ResourceManager.__Descendant_Table[com/dmdirc/util/resourcemanager/ZipResourceManager]
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Descendant_Table[com/dmdirc/util/resourcemanager/ZipResourceManager] == &__Dispatch_Table
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): com/dmdirc/util/resourcemanager/ResourceManager.__Descendant_Table[com/dmdirc/util/resourcemanager/ZipResourceManager] == &__Dispatch_Table
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.extractResource(Ljava/lang/String;Ljava/lang/String;Z)Z == &com/dmdirc/util/resourcemanager/ResourceManager.extractResource
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.extractResources(Ljava/lang/String;Ljava/lang/String;)V == &com/dmdirc/util/resourcemanager/ResourceManager.extractResources
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.extractResources(Ljava/lang/String;Ljava/lang/String;Z)V == &com/dmdirc/util/resourcemanager/ResourceManager.extractResources
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourceBytes(Ljava/lang/String;)[B == &getResourceBytes
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourceInputStream(Ljava/lang/String;)Ljava/io/InputStream; == &getResourceInputStream
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourcesEndingWithAsBytes(Ljava/lang/String;)Ljava/util/Map; == &getResourcesEndingWithAsBytes
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourcesStartingWith(Ljava/lang/String;)Ljava/util/List; == &getResourcesStartingWith
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourcesStartingWithAsBytes(Ljava/lang/String;)Ljava/util/Map; == &getResourcesStartingWithAsBytes
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.getResourcesStartingWithAsInputStreams(Ljava/lang/String;)Ljava/util/Map; == &getResourcesStartingWithAsInputStreams
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.resourceExists(Ljava/lang/String;)Z == &resourceExists
    //#post(com.dmdirc.util.resourcemanager.ZipResourceManager__static_init): __Dispatch_Table.resourceToFile([BLjava/io/File;)V == &com/dmdirc/util/resourcemanager/ResourceManager.resourceToFile
    //#ZipResourceManager.java:: end of method: com.dmdirc.util.resourcemanager.ZipResourceManager.com.dmdirc.util.resourcemanager.ZipResourceManager__static_init
    //#ZipResourceManager.java:: end of class: com.dmdirc.util.resourcemanager.ZipResourceManager
