Messages

Last Msg First Msg

method

com.dmdirc.ui.themes.Theme__static_init

method	int compareTo(Object)
pre	this.file != null
pre	init'ed(this.metadata)
pre	x0 != null
pre	x0.file != null
pre	init'ed(x0.metadata)
pre	(soft) init'ed(this.metadata.automake)
pre	(soft) this.metadata.domains != null
pre	(soft) this.metadata.keydomains != null
pre	(soft) init'ed(x0.metadata.automake)
pre	(soft) x0.metadata.domains != null
pre	(soft) x0.metadata.keydomains != null
post	init'ed(return_value)
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on getName
unanalyzed	call on java.lang.String:compareTo
unanalyzed	call on getMetaData
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:get

method	void com.dmdirc.ui.themes.Theme(File)
post	this.file == file
post	init'ed(this.file)

method	bool isValidTheme()
pre	init'ed(this.rm)
pre	(soft) this.file != null
pre	(soft) this.rm.zipFile != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.MEDIUM)
post	init'ed(return_value)
post	this.metadata == One-of{old this.metadata, &new ConfigFile(isValidTheme#2), null}
post	possibly_updated(this.metadata.lines)
post	this.rm == One-of{old this.rm, &new ZipResourceManager(getInstance#1)}
post	init'ed(this.rm)
post	new ArrayList(ConfigFile#1) num objects <= 1
post	new ArrayList(ZipResourceManager#2) num objects <= 1
post	new ArrayList(readLines#4) num objects == 0
post	new ConfigFile(isValidTheme#2) num objects <= 1
post	init'ed(new ConfigFile(isValidTheme#2).charset)
post	new ConfigFile(isValidTheme#2).domains == &new ArrayList(ConfigFile#1)
post	init'ed(new ConfigFile(isValidTheme#2).file)
post	new ConfigFile(isValidTheme#2).flatdomains == &new MapList(ConfigFile#2)
post	init'ed(new ConfigFile(isValidTheme#2).is)
post	new ConfigFile(isValidTheme#2).keydomains == &new HashMap(ConfigFile#3)
post	init'ed(new ConfigFile(isValidTheme#2).lines)
post	new HashMap(ConfigFile#3) num objects <= 1
post	new HashMap(MapList#1) num objects <= 1
post	new MapList(ConfigFile#2) num objects <= 1
post	new MapList(ConfigFile#2).map == &new HashMap(MapList#1)
post	new ZipFile(ZipResourceManager#1) num objects <= 1
post	new ZipResourceManager(getInstance#1) num objects <= 1
post	new ZipResourceManager(getInstance#1).entries == &new ArrayList(ZipResourceManager#2)
post	new ZipResourceManager(getInstance#1).zipFile == &new ZipFile(ZipResourceManager#1)
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:get
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
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.zip.ZipEntry:isDirectory
unanalyzed	call on java.nio.charset.Charset:forName
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.Map:clear
unanalyzed	call on java.util.List:clear
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on java.io.BufferedReader:readLine
unanalyzed	call on java.io.BufferedReader:close
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.lang.Exception
test_vector	this.rm: Inverse{null}, Addr_Set{null}

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

Prev Msg Next Msg

test always goes same way

click for all messages in this file Low Prob.

Test predetermined because this.rm != null

Prev Msg Next Msg

method	void applyTheme()
pre	(soft) init'ed(this.enabled)
pre	(soft) init'ed(this.rm)
pre	(soft) this.file != null
pre	(soft) this.rm.zipFile != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.MEDIUM)
presumption	this.rm.zipFile@105 != null
post	init'ed(this.enabled)
post	this.identity == One-of{old this.identity, &new ThemeIdentity(applyTheme#1)}
post	this.metadata == One-of{old this.metadata, &new ConfigFile(isValidTheme#2), null}
post	init'ed(this.metadata.lines)
post	this.rm == One-of{old this.rm, &new ZipResourceManager(getInstance#1)}
post	init'ed(this.rm)
post	new ArrayList(ConfigFile#1) num objects <= 1
post	new ConfigFile(isValidTheme#2) num objects == new ArrayList(ConfigFile#1) num objects
post	new HashMap(ConfigFile#3) num objects == new ArrayList(ConfigFile#1) num objects
post	new HashMap(MapList#1) num objects == new ArrayList(ConfigFile#1) num objects
post	new MapList(ConfigFile#2) num objects == new ArrayList(ConfigFile#1) num objects
post	new ArrayList(ZipResourceManager#2) num objects <= 1
post	new ZipFile(ZipResourceManager#1) num objects == new ArrayList(ZipResourceManager#2) num objects
post	new ZipResourceManager(getInstance#1) num objects == new ArrayList(ZipResourceManager#2) num objects
post	new ArrayList(readLines#4) num objects == 0
post	init'ed(new ConfigFile(isValidTheme#2).charset)
post	new ConfigFile(isValidTheme#2).domains == &new ArrayList(ConfigFile#1)
post	init'ed(new ConfigFile(isValidTheme#2).file)
post	new ConfigFile(isValidTheme#2).flatdomains == &new MapList(ConfigFile#2)
post	init'ed(new ConfigFile(isValidTheme#2).is)
post	new ConfigFile(isValidTheme#2).keydomains == &new HashMap(ConfigFile#3)
post	init'ed(new ConfigFile(isValidTheme#2).lines)
post	new MapList(ConfigFile#2).map == &new HashMap(MapList#1)
post	new ThemeIdentity(applyTheme#1) num objects <= 1
post	init'ed(new ThemeIdentity(applyTheme#1).myTarget)
post	init'ed(new ThemeIdentity(applyTheme#1).theme)
post	new ZipResourceManager(getInstance#1).entries == &new ArrayList(ZipResourceManager#2)
post	new ZipResourceManager(getInstance#1).zipFile == &new ZipFile(ZipResourceManager#1)
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:get
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
unanalyzed	call on com.dmdirc.config.Identity
unanalyzed	call on com.dmdirc.config.ConfigTarget:setTheme
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on java.io.IOException:getMessage
unanalyzed	call on java.io.File:getCanonicalPath
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.zip.ZipEntry:isDirectory
unanalyzed	call on java.nio.charset.Charset:forName
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.Map:clear
unanalyzed	call on java.util.List:clear
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on java.io.BufferedReader:readLine
unanalyzed	call on java.io.BufferedReader:close
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.io.File:getAbsolutePath
test_vector	this.enabled: {0}, {1}

method not available - call not analyzed Info call on void com.dmdirc.config.IdentityManager:addI dentity(Identity)

method not available - call not analyzed Info call on String com.dmdirc.config.InvalidIdentityFil eException:getMessage()

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

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

method	void removeTheme()
pre	init'ed(this.rm)
pre	(soft) init'ed(this.enabled)
pre	(soft) this.file != null
pre	(soft) init'ed(this.identity)
pre	(soft) this.rm.zipFile != null
post	init'ed(this.enabled)
post	this.metadata == One-of{old this.metadata, &new ConfigFile(isValidTheme#2), null}
post	init'ed(this.metadata.lines)
post	this.rm == One-of{old this.rm, &new ZipResourceManager(getInstance#1)}
post	init'ed(this.rm)
post	new ArrayList(ConfigFile#1) num objects <= 1
post	new ConfigFile(isValidTheme#2) num objects == new ArrayList(ConfigFile#1) num objects
post	new HashMap(ConfigFile#3) num objects == new ArrayList(ConfigFile#1) num objects
post	new HashMap(MapList#1) num objects == new ArrayList(ConfigFile#1) num objects
post	new MapList(ConfigFile#2) num objects == new ArrayList(ConfigFile#1) num objects
post	new ArrayList(ZipResourceManager#2) num objects <= 1
post	new ZipFile(ZipResourceManager#1) num objects == new ArrayList(ZipResourceManager#2) num objects
post	new ZipResourceManager(getInstance#1) num objects == new ArrayList(ZipResourceManager#2) num objects
post	new ArrayList(readLines#4) num objects == 0
post	init'ed(new ConfigFile(isValidTheme#2).charset)
post	new ConfigFile(isValidTheme#2).domains == &new ArrayList(ConfigFile#1)
post	init'ed(new ConfigFile(isValidTheme#2).file)
post	new ConfigFile(isValidTheme#2).flatdomains == &new MapList(ConfigFile#2)
post	init'ed(new ConfigFile(isValidTheme#2).is)
post	new ConfigFile(isValidTheme#2).keydomains == &new HashMap(ConfigFile#3)
post	init'ed(new ConfigFile(isValidTheme#2).lines)
post	new MapList(ConfigFile#2).map == &new HashMap(MapList#1)
post	new ZipResourceManager(getInstance#1).entries == &new ArrayList(ZipResourceManager#2)
post	new ZipResourceManager(getInstance#1).zipFile == &new ZipFile(ZipResourceManager#1)
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:get
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
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on java.io.IOException:getMessage
unanalyzed	call on java.io.File:getCanonicalPath
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.zip.ZipEntry:isDirectory
unanalyzed	call on java.nio.charset.Charset:forName
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.Map:clear
unanalyzed	call on java.util.List:clear
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on java.io.BufferedReader:readLine
unanalyzed	call on java.io.BufferedReader:close
unanalyzed	call on java.lang.String:isEmpty
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.io.File:getAbsolutePath
test_vector	this.enabled: {0}, {1}
test_vector	this.identity: Inverse{null}, Addr_Set{null}

method not available - call not analyzed Info call on void com.dmdirc.config.IdentityManager:remo veIdentity(Identity)

method	bool isEnabled()
pre	init'ed(this.enabled)
post	return_value == this.enabled
post	init'ed(return_value)

method	String getFileName(bool)
pre	this.file != null
presumption	java.io.File:getName(...)@156 != null
post	java.lang.String:substring(...)._tainted == 0
post	return_value != null
test_vector	includeExtension: {1}, {0}

method	String getFileName()
pre	this.file != null
post	java.lang.String:substring(...)._tainted == 0
post	return_value != null
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring

method	String getName()
pre	this.file != null
pre	init'ed(this.metadata)
pre	(soft) init'ed(this.metadata.automake)
pre	(soft) this.metadata.domains != null
pre	(soft) this.metadata.keydomains != null
post	java.lang.String:substring(...)._tainted == 0
post	init'ed(return_value)
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:get

method	String getVersion()
pre	init'ed(this.metadata)
pre	(soft) init'ed(this.metadata.automake)
pre	(soft) this.metadata.domains != null
pre	(soft) this.metadata.keydomains != null
post	init'ed(return_value)
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:get

method	String getAuthor()
pre	init'ed(this.metadata)
pre	(soft) init'ed(this.metadata.automake)
pre	(soft) this.metadata.domains != null
pre	(soft) this.metadata.keydomains != null
post	init'ed(return_value)
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:get

method	String getDescription()
pre	init'ed(this.metadata)
pre	(soft) init'ed(this.metadata.automake)
pre	(soft) this.metadata.domains != null
pre	(soft) this.metadata.keydomains != null
post	init'ed(return_value)
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:get

method	int compareTo(Theme)
pre	o != null
pre	o.file != null
pre	init'ed(o.metadata)
pre	this.file != null
pre	init'ed(this.metadata)
pre	(soft) init'ed(o.metadata.automake)
pre	(soft) o.metadata.domains != null
pre	(soft) o.metadata.keydomains != null
pre	(soft) init'ed(this.metadata.automake)
pre	(soft) this.metadata.domains != null
pre	(soft) this.metadata.keydomains != null
post	init'ed(return_value)
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
unanalyzed	call on getMetaData
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:get

Prev Msg Next Msg

null dereference

click for all messages in this file Medium Prob.

check that getName(...) != null

unused assignment in callee

Low Prob.

Unused assignment to (java.lang.String:substring(.. .)._tainted) in getName

Prev Msg Next Msg

method	String getMetaData(String, String)
pre	init'ed(this.metadata)
pre	(soft) init'ed(this.metadata.automake)
pre	(soft) this.metadata.domains != null
pre	(soft) this.metadata.keydomains != null
presumption	java.util.Map:get(...)@236 != null
post	init'ed(return_value)
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:get
test_vector	this.metadata: Addr_Set{null}, Inverse{null}
test_vector	java.util.Map:containsKey(...)@226: {1}, {0}
test_vector	java.util.Map:containsKey(...)@267: {0}, {1}

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