ZipResourceManager.java

ZipResourceManager.java

current inspection = 2009-09-03 21:56:13 (id #1)

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void com.dmdirc.util.resourcemanager.ZipResourceManager(String)

Kind	Annotation Text
presumption	java.util.Enumeration:nextElement(...)@63 != null
presumption	java.util.zip.ZipFile:entries(...)@61 != null
post	new ArrayList(ZipResourceManager#2) num objects == 1
post	new ZipFile(ZipResourceManager#1) num objects == 1
post	this.entries == &new ArrayList(ZipResourceManag er#2)
post	this.zipFile == &new ZipFile(ZipResourceManager #1)
test_vector	java.util.Enumeration:hasMoreElements(...)@62: {0}, {1}

com.dmdirc.util.resourcemanager.ZipResourceManager__static_init

Kind	Annotation Text

ZipResourceManager getInstance(String)

Kind	Annotation Text
post	new ArrayList(ZipResourceManager#2) num objects == 1
post	new ZipFile(ZipResourceManager#1) num objects == 1
post	new ZipResourceManager(getInstance#1) num objects == 1
post	return_value == &new ZipResourceManager(getInst ance#1)
post	return_value.entries == &new ArrayList(ZipResou rceManager#2)
post	return_value.zipFile == &new ZipFile(ZipResourc eManager#1)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Enumeration:hasMoreElements
unanalyzed	call on java.util.Enumeration:nextElement
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.zip.ZipEntry:getName
unanalyzed	call on java.util.zip.ZipFile
unanalyzed	call on java.util.zip.ZipFile:entries

byte[] getResourceBytes(String)

Kind	Annotation Text
pre	this.zipFile != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	java.util.zip.ZipEntry:getSize(...)@104 >= 0
post	new byte[](getResourceBytes#1) num objects <= 1
post	new byte[](getResourceBytes#1).length == 0
post	new byte[](getResourceBytes#2) num objects <= 1
post	new byte[](getResourceBytes#2).length == 0
post	new byte[](getResourceBytes#3) num objects <= 1
post	new byte[](getResourceBytes#3).length <= 2⁶⁴-1
post	new byte[](getResourceBytes#5) num objects <= 1
post	new byte[](getResourceBytes#5).length == 0
post	new byte[](getResourceBytes#6) num objects <= 1
post	new byte[](getResourceBytes#6).length == 0
post	new byte[](getResourceBytes#7) num objects <= 1
post	new byte[](getResourceBytes#7).length == 0
post	return_value in Addr_Set{&new byte[](getResourc eBytes#3),&new byte[](getResourceBytes#6), &new byte[](getResourceBytes#7),&new byte[](getResourceBytes#5),&new byte[](getResourceBytes#2),&new byte[](getResourceBytes#1)}
test_vector	java.util.zip.ZipEntry:isDirectory(...)@100: {0}, {1}
test_vector	java.util.zip.ZipFile:getEntry(...)@92: Inverse{null}, Addr_Set{null}

InputStream getResourceInputStream(String)

Kind	Annotation Text
pre	this.zipFile != null
post	init'ed(return_value)
test_vector	java.util.zip.ZipFile:getEntry(...)@134: Inverse{null}, Addr_Set{null}

Map getResourcesEndingWithAsBytes(String)

Kind	Annotation Text
pre	(soft) this.zipFile != null
pre	this.entries != null
presumption	java.util.Iterator:next(...)@154 != null
post	new HashMap(getResourcesEndingWithAsBytes#1) num objects == 1
post	return_value == &new HashMap(getResourcesEnding WithAsBytes#1)
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on java.io.BufferedInputStream
unanalyzed	call on java.io.BufferedInputStream:close
unanalyzed	call on java.io.BufferedInputStream:read
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.zip.ZipEntry:getSize
unanalyzed	call on java.util.zip.ZipEntry:isDirectory
unanalyzed	call on java.util.zip.ZipFile:getEntry
unanalyzed	call on java.util.zip.ZipFile:getInputStream
test_vector	java.lang.String:endsWith(...)@155: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@154: {0}, {1}

List getResourcesStartingWith(String)

Kind	Annotation Text
pre	this.entries != null
presumption	java.util.Iterator:next(...)@199 != null
post	new ArrayList(getResourcesStartingWith#1) num objects == 1
post	return_value == &new ArrayList(getResourcesStar tingWith#1)
test_vector	java.lang.String:startsWith(...)@200: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@199: {0}, {1}

Map getResourcesStartingWithAsBytes(String)

Kind	Annotation Text
pre	(soft) this.zipFile != null
pre	this.entries != null
presumption	java.util.Iterator:next(...)@169 != null
post	new HashMap(getResourcesStartingWithAsBytes#1) num objects == 1
post	return_value == &new HashMap(getResourcesStarti ngWithAsBytes#1)
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on java.io.BufferedInputStream
unanalyzed	call on java.io.BufferedInputStream:close
unanalyzed	call on java.io.BufferedInputStream:read
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.zip.ZipEntry:getSize
unanalyzed	call on java.util.zip.ZipEntry:isDirectory
unanalyzed	call on java.util.zip.ZipFile:getEntry
unanalyzed	call on java.util.zip.ZipFile:getInputStream
test_vector	java.lang.String:startsWith(...)@170: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@169: {0}, {1}

Map getResourcesStartingWithAsInputStreams(String)

Kind	Annotation Text
pre	(soft) this.zipFile != null
pre	this.entries != null
presumption	java.util.Iterator:next(...)@185 != null
post	new HashMap(getResourcesStartingWithAsInputStreams# 1) num objects == 1
post	return_value == &new HashMap(getResourcesStarti ngWithAsInputStreams#1)
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.zip.ZipFile:getEntry
unanalyzed	call on java.util.zip.ZipFile:getInputStream
test_vector	java.lang.String:startsWith(...)@186: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@185: {0}, {1}

bool resourceExists(String)

Kind	Annotation Text
pre	this.zipFile != null
post	init'ed(return_value)