URLHandler.java

URLHandler.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.URLHandler()

Kind	Annotation Text
post	init'ed(this.config)
post	init'ed(this.desktop)
test_vector	java.awt.Desktop:isDesktopSupported(...)@55: {0}, {1}

com.dmdirc.util.URLHandler__static_init

Kind	Annotation Text
post	init'ed(me.config)
post	init'ed(me.desktop)
post	me == &new URLHandler(URLHandler__static_ init#1)
post	new URLHandler(URLHandler__static_init#1) num objects == 1
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on java.awt.Desktop:getDesktop
unanalyzed	call on java.awt.Desktop:isDesktopSupported

void execApp(String)

Kind	Annotation Text
pre	(soft) command != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	java.lang.Runtime:getRuntime(...)@233 != null
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:toArray

void execBrowser(URI)

Kind	Annotation Text
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	init'ed(java.awt.Desktop$Action.BROWSE)
test_vector	java.awt.Desktop:isSupported(...)@287: {0}, {1}
test_vector	this.desktop: Addr_Set{null}, Inverse{null}

void execMail(URI)

Kind	Annotation Text
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	init'ed(java.awt.Desktop$Action.MAIL)
test_vector	java.awt.Desktop:isSupported(...)@310: {0}, {1}
test_vector	this.desktop: Addr_Set{null}, Inverse{null}

URLHandler getURLHander()

Kind	Annotation Text
post	return_value == &new URLHandler(URLHandler__ static_init#1)

void launchApp(String)

Kind	Annotation Text
pre	(soft) init'ed(lastLaunch)
pre	(soft) this.config != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
post	init'ed(lastLaunch)
post	lastLaunch == One-of{old lastLaunch, &new Date(launchApp#1*)}
post	new Date(launchApp#1*) num objects <= 1
unanalyzed	call on com.dmdirc.Main:getUI
unanalyzed	call on com.dmdirc.Server
unanalyzed	call on com.dmdirc.Server:join
unanalyzed	call on com.dmdirc.ServerManager:getServerManager
unanalyzed	call on com.dmdirc.ServerManager:getServersByAddres s
unanalyzed	call on com.dmdirc.config.ConfigManager:getOption
unanalyzed	call on com.dmdirc.config.ConfigManager:getOptionBo ol
unanalyzed	call on com.dmdirc.config.ConfigManager:getOptionIn t
unanalyzed	call on com.dmdirc.config.ConfigManager:hasOptionSt ring
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.config.IdentityManager:getProfil es
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.util.InvalidAddressException:get Message
unanalyzed	call on getStatusBar
unanalyzed	call on java.awt.Desktop:browse
unanalyzed	call on java.awt.Desktop:isSupported
unanalyzed	call on java.awt.Desktop:mail
unanalyzed	call on java.io.IOException:getMessage
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.Long:longValue
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.Runtime:exec
unanalyzed	call on java.lang.Runtime:getRuntime
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:equalsIgnoreCase
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:replaceAll
unanalyzed	call on java.lang.String:replaceFirst
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.net.URI
unanalyzed	call on java.net.URI:getFragment
unanalyzed	call on java.net.URI:getHost
unanalyzed	call on java.net.URI:getPath
unanalyzed	call on java.net.URI:getPort
unanalyzed	call on java.net.URI:getQuery
unanalyzed	call on java.net.URI:getScheme
unanalyzed	call on java.net.URI:getUserInfo
unanalyzed	call on java.net.URI:toString
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on java.util.Date
unanalyzed	call on java.util.Date:getTime
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:toArray
unanalyzed	call on setMessage
unanalyzed	call on showURLDialog
test_vector	java.net.URI:getScheme(...)@82: Inverse{null}, Addr_Set{null}

void launchApp(URI)

Kind	Annotation Text
pre	(soft) this.config != null
pre	(soft) uri != null
pre	init'ed(lastLaunch)
presumption	com.dmdirc.Main:getUI(...)@133 != null
presumption	com.dmdirc.Main:getUI(...)@141 != null
presumption	com.dmdirc.Main:getUI(...)@149 != null
presumption	com.dmdirc.Main:getUI(...)@154 != null
presumption	com.dmdirc.config.ConfigManager:getOption(...)@137 != null
presumption	com.dmdirc.config.IdentityManager:getGlobalConfig(. ..)@122 != null
presumption	com.dmdirc.config.IdentityManager:getGlobalConfig(. ..)@126 != null
presumption	getStatusBar(...)@141 != null
presumption	getStatusBar(...)@149 != null
presumption	getStatusBar(...)@154 != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	java.lang.Long:valueOf(...)@124 != null
presumption	java.util.Date:getTime(...)@124 - java.util. Date:getTime(...)@124 in {-18_446_744_073_709_551_6 15..2⁶³}
post	lastLaunch == &new Date(launchApp#1)
post	new Date(launchApp#1) num objects == 1
unanalyzed	call on com.dmdirc.Server
unanalyzed	call on com.dmdirc.Server:join
unanalyzed	call on com.dmdirc.ServerManager:getServerManager
unanalyzed	call on com.dmdirc.ServerManager:getServersByAddres s
unanalyzed	call on com.dmdirc.config.IdentityManager:getProfil es
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on java.awt.Desktop:browse
unanalyzed	call on java.awt.Desktop:isSupported
unanalyzed	call on java.awt.Desktop:mail
unanalyzed	call on java.io.IOException:getMessage
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.Runtime:exec
unanalyzed	call on java.lang.Runtime:getRuntime
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:equalsIgnoreCase
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:replaceAll
unanalyzed	call on java.lang.String:replaceFirst
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.net.URI
unanalyzed	call on java.net.URI:getFragment
unanalyzed	call on java.net.URI:getHost
unanalyzed	call on java.net.URI:getPath
unanalyzed	call on java.net.URI:getPort
unanalyzed	call on java.net.URI:getQuery
unanalyzed	call on java.net.URI:getScheme
unanalyzed	call on java.net.URI:getUserInfo
unanalyzed	call on java.net.URI:toString
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:toArray
test_vector	com.dmdirc.config.ConfigManager:getOptionBool(... )@122: {0}, {1}
test_vector	com.dmdirc.config.ConfigManager:hasOptionString(... )@132: {1}, {0}
test_vector	java.lang.String:equals(...)@139: {0}, {1}
test_vector	java.lang.String:equals(...)@148: {0}, {1}
test_vector	java.lang.String:equals(...)@151: {0}, {1}
test_vector	lastLaunch: Addr_Set{null}, Inverse{null}

void launchApp(URL)

Kind	Annotation Text
pre	(soft) init'ed(lastLaunch)
pre	(soft) this.config != null
pre	(soft) url != null
presumption	init'ed(com.dmdirc.logger.ErrorLevel.LOW)
presumption	java.net.URL:toURI(...)@101 != null
post	init'ed(lastLaunch)
post	lastLaunch == One-of{old lastLaunch, &new Date(launchApp#1*)}
post	new Date(launchApp#1*) num objects <= 1
unanalyzed	call on com.dmdirc.Main:getUI
unanalyzed	call on com.dmdirc.Server
unanalyzed	call on com.dmdirc.Server:join
unanalyzed	call on com.dmdirc.ServerManager:getServerManager
unanalyzed	call on com.dmdirc.ServerManager:getServersByAddres s
unanalyzed	call on com.dmdirc.config.ConfigManager:getOption
unanalyzed	call on com.dmdirc.config.ConfigManager:getOptionBo ol
unanalyzed	call on com.dmdirc.config.ConfigManager:getOptionIn t
unanalyzed	call on com.dmdirc.config.ConfigManager:hasOptionSt ring
unanalyzed	call on com.dmdirc.config.IdentityManager:getGlobal Config
unanalyzed	call on com.dmdirc.config.IdentityManager:getProfil es
unanalyzed	call on com.dmdirc.logger.Logger:userError
unanalyzed	call on com.dmdirc.util.InvalidAddressException:get Message
unanalyzed	call on getStatusBar
unanalyzed	call on java.awt.Desktop:browse
unanalyzed	call on java.awt.Desktop:isSupported
unanalyzed	call on java.awt.Desktop:mail
unanalyzed	call on java.io.IOException:getMessage
unanalyzed	call on java.lang.Exception
unanalyzed	call on java.lang.Long:longValue
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.Runtime:exec
unanalyzed	call on java.lang.Runtime:getRuntime
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:equalsIgnoreCase
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:replaceAll
unanalyzed	call on java.lang.String:replaceFirst
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.net.URI
unanalyzed	call on java.net.URI:getFragment
unanalyzed	call on java.net.URI:getHost
unanalyzed	call on java.net.URI:getPath
unanalyzed	call on java.net.URI:getPort
unanalyzed	call on java.net.URI:getQuery
unanalyzed	call on java.net.URI:getScheme
unanalyzed	call on java.net.URI:getUserInfo
unanalyzed	call on java.net.URI:toString
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:iterator
unanalyzed	call on java.util.Date
unanalyzed	call on java.util.Date:getTime
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:toArray
unanalyzed	call on setMessage
unanalyzed	call on showURLDialog
test_vector	java.net.URI:getScheme(...)@102: Inverse{null}, Addr_Set{null}

String[] parseArguments(String)

Kind	Annotation Text
pre	command != null
presumption	java.util.List:size(...)@278 >= 0
post	init'ed(return_value)

String substituteParams(URI, String)

Kind	Annotation Text
pre	command != null
pre	url != null
presumption	java.lang.String:indexOf(...)@207 <= 2³²-2
post	return_value != null
test_vector	java.lang.String:indexOf(...)@204: {-2³¹. .-2, 0..2³²-1}, {-1}
test_vector	java.lang.String:isEmpty(...)@203: {1}, {0}
test_vector	java.net.URI:getFragment(...)@179: Addr_Set{null}, Inverse{null}
test_vector	java.net.URI:getHost(...)@183: Addr_Set{null}, Inverse{null}
test_vector	java.net.URI:getPath(...)@187: Addr_Set{null}, Inverse{null}
test_vector	java.net.URI:getPort(...)@199: {-2³¹..0}, {1..2³²-1}
test_vector	java.net.URI:getQuery(...)@195: Addr_Set{null}, Inverse{null}
test_vector	java.net.URI:getScheme(...)@191: Addr_Set{null}, Inverse{null}
test_vector	java.net.URI:getUserInfo(...)@168: Addr_Set{null}, Inverse{null}