Messages

method

com.dmdirc.addons.addonbrowser.AddonInfo__static_ init

method	AddonInfo$AddonType[] values()
pre	(soft) init'ed($VALUES[...])
post	return_value == &new AddonInfo$AddonType[](valu es#1)
post	new AddonInfo$AddonType[](values#1) num objects == 1
post	return_value.length == 3
post	return_value[...] == One-of{$VALUES[...], undefined}

method	AddonInfo$AddonType valueOf(String)
post	init'ed(return_value)

method

void com.dmdirc.addons.addonbrowser. AddonInfo$AddonType(String, int)

method	com.dmdirc.addons.addonbrowser.AddonInfo$AddonType __static_init
post	$VALUES == &new AddonInfo$AddonType[](AddonInfo $AddonType__static_init#4)
post	TYPE_ACTION_PACK == &new AddonInfo$AddonType(Ad donInfo$AddonType__static_init#3)
post	$VALUES[2] == &new AddonInfo$AddonType(AddonInf o$AddonType__static_init#3)
post	TYPE_PLUGIN == &new AddonInfo$AddonType(AddonIn fo$AddonType__static_init#1)
post	$VALUES[0] == &new AddonInfo$AddonType(AddonInf o$AddonType__static_init#1)
post	TYPE_THEME == &new AddonInfo$AddonType(AddonInf o$AddonType__static_init#2)
post	$VALUES[1] == &new AddonInfo$AddonType(AddonInf o$AddonType__static_init#2)
post	new AddonInfo$AddonType(AddonInfo$AddonType__ static_init#1) num objects == 1
post	new AddonInfo$AddonType(AddonInfo$AddonType__ static_init#2) num objects == 1
post	new AddonInfo$AddonType(AddonInfo$AddonType__ static_init#3) num objects == 1
post	new AddonInfo$AddonType[](AddonInfo$AddonType__ static_init#4) num objects == 1
post	$VALUES.length == 3
unanalyzed	call on java.lang.Enum

method	String toString()
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuilder:toStri ng(...)

method	void com.dmdirc.addons.addonbrowser. AddonInfo(Map)
pre	entry != null
presumption	java.util.Map:get(...)@79 != null
presumption	java.util.Map:get(...)@85 != null
presumption	java.util.Map:get(...)@87 != null
presumption	javax.swing.ImageIcon:getImage(...)@90 != null
post	init'ed(this.author)
post	init'ed(this.date)
post	init'ed(this.description)
post	init'ed(this.id)
post	init'ed(this.rating)
post	this.screenshot in Addr_Set{&new ImageIcon(AddonInfo#3),&new ImageIcon(AddonInf o#1)}
post	init'ed(this.stableDownload)
post	init'ed(this.title)
post	this.type == One-of{&com.dmdirc.addons. addonbrowser.AddonInfo$AddonType__static_init.new AddonInfo$AddonType(AddonInfo$AddonType__static_ init#1), &com.dmdirc.addons.addonbrowser. AddonInfo$AddonType__static_init.new AddonInfo$AddonType(Addo...
post	this.type in Addr_Set{&com.dmdirc.addons. addonbrowser.AddonInfo$AddonType__static_init.new AddonInfo$AddonType(AddonInfo$AddonType__static_ init#3),&com.dmdirc.addons.addonbrowser. AddonInfo$AddonType__static_init.new AddonInfo$AddonType(Add...
post	init'ed(this.unstableDownload)
post	init'ed(this.verified)
post	new ImageIcon(AddonInfo#1) num objects <= 1
post	new ImageIcon(AddonInfo#3) num objects <= 1
test_vector	java.lang.String:equals(...)@87: {0}, {1}

method not available - call not analyzed Info call on URL com.dmdirc.util.URLBuilder:buildURL(Str ing)

method	String getDescription()
post	return_value == this.description
post	init'ed(return_value)

method	String getStableDownload()
post	return_value == this.stableDownload
post	init'ed(return_value)

method	AddonInfo$AddonType getType()
post	return_value == this.type
post	init'ed(return_value)

method	String getUnstableDownload()
post	return_value == this.unstableDownload
post	init'ed(return_value)

method	ImageIcon getScreenshot()
post	return_value == this.screenshot
post	init'ed(return_value)

method	bool isInstalled()
presumption	com.dmdirc.updater.UpdateChecker:getComponents(... )@143 != null
presumption	com.dmdirc.updater.UpdateComponent:getName(... )@144 != null
presumption	java.util.Iterator:next(...)@143 != null
post	init'ed(return_value)
test_vector	java.lang.String:equals(...)@144: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@143: {0}, {1}

method not available - call not analyzed Info call on List com.dmdirc.updater.UpdateChecker:getCo mponents()

method not available - call not analyzed Info call on String com.dmdirc.updater.UpdateComponent:g etName()

method	bool isDownloadable()
post	return_value == 0