Messages

method

com.dmdirc.util.resourcemanager.ZipResourceManager __static_init

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

method	ZipResourceManager getInstance(String)
post	return_value == &new ZipResourceManager(getInst ance#1)
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.entries == &new ArrayList(ZipResou rceManager#2)
post	return_value.zipFile == &new ZipFile(ZipResourc eManager#1)
unanalyzed	call on java.util.zip.ZipFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.zip.ZipFile:entries
unanalyzed	call on java.util.Enumeration:hasMoreElements
unanalyzed	call on java.util.Enumeration:nextElement
unanalyzed	call on java.util.zip.ZipEntry:getName
unanalyzed	call on java.util.List:add

method	bool resourceExists(String)
pre	this.zipFile != null
post	init'ed(return_value)

method	byte[] getResourceBytes(String)
pre	this.zipFile != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	java.util.zip.ZipEntry:getSize(...)@104 >= 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)}
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
test_vector	java.util.zip.ZipEntry:isDirectory(...)@100: {0}, {1}
test_vector	java.util.zip.ZipFile:getEntry(...)@92: Inverse{null}, Addr_Set{null}

method not available - call not analyzed Info call on void com.dmdirc.logger.Logger:userError(Err orLevel, String)

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

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

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

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

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