Theme.java

Theme.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void applyTheme()

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

void com.dmdirc.ui.themes.Theme(File)

Kind	Annotation Text
post	init'ed(this.file)
post	this.file == file

com.dmdirc.ui.themes.Theme__static_init

Kind	Annotation Text

int compareTo(Theme)

Kind	Annotation Text
pre	(soft) init'ed(o.metadata.automake)
pre	(soft) init'ed(this.metadata.automake)
pre	(soft) o.metadata.domains != null
pre	(soft) o.metadata.keydomains != null
pre	(soft) this.metadata.domains != null
pre	(soft) this.metadata.keydomains != null
pre	init'ed(o.metadata)
pre	init'ed(this.metadata)
pre	o != null
pre	o.file != null
pre	this.file != null
post	init'ed(return_value)
unanalyzed	call on getMetaData
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.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put

int compareTo(Object)

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

String getAuthor()

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

String getDescription()

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

String getFileName()

Kind	Annotation Text
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

String getFileName(bool)

Kind	Annotation Text
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}

String getMetaData(String, String)

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

String getName()

Kind	Annotation Text
pre	(soft) init'ed(this.metadata.automake)
pre	(soft) this.metadata.domains != null
pre	(soft) this.metadata.keydomains != null
pre	init'ed(this.metadata)
pre	this.file != null
post	init'ed(return_value)
post	java.lang.String:substring(...)._tainted == 0
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.HashMap
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put

String getVersion()

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

bool isEnabled()

Kind	Annotation Text
pre	init'ed(this.enabled)
post	init'ed(return_value)
post	return_value == this.enabled

bool isValidTheme()

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

void removeTheme()

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