method

com.dmdirc.plugins.Service__static_init

method	void com.dmdirc.plugins.Service(String, String)
post	this.name == name
post	init'ed(this.name)
post	this.serviceproviders == &new ArrayList(Service #1)
post	this.type == type
post	init'ed(this.type)
post	new ArrayList(Service#1) num objects == 1

method	String getName()
post	return_value == this.name
post	init'ed(return_value)

method	String getType()
post	return_value == this.type
post	init'ed(return_value)

method	void addProvider(ServiceProvider)
pre	this.serviceproviders != null

method	void delProvider(ServiceProvider)
pre	this.serviceproviders != null

method	List getProviders()
pre	init'ed(this.serviceproviders)
post	return_value == &new ArrayList(getProviders#1)
post	new ArrayList(getProviders#1) num objects == 1

method	ServiceProvider getActiveProvider()
pre	init'ed(this.serviceproviders)
presumption	java.util.Iterator:next(...)@102 != null
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList
test_vector	java.util.Iterator:hasNext(...)@102: {0}, {1}

method	bool isActive()
pre	init'ed(this.serviceproviders)
presumption	java.util.Iterator:next(...)@118 != null
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList
test_vector	java.util.Iterator:hasNext(...)@118: {0}, {1}

method	bool activate()
pre	(soft) init'ed(this.serviceproviders)
presumption	java.util.Iterator:next(...)@138 != null
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:iterator
unanalyzed	call on isActive
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on updateProvides
unanalyzed	call on checkRequirements
unanalyzed	call on loadRequired
unanalyzed	call on onLoad
unanalyzed	call on getName
unanalyzed	call on java.lang.Throwable:getMessage
unanalyzed	call on addError
unanalyzed	call on unloadPlugin
unanalyzed	call on getMainClass
unanalyzed	call on loadClass
unanalyzed	call on com.dmdirc.actions.ActionManager:processEve nt
unanalyzed	call on loadPlugin
test_vector	java.util.Iterator:hasNext(...)@138: {0}, {1}
test_vector	provider.plugin@138: Inverse{null}, Addr_Set{null}

method	String toString()
pre	this.serviceproviders != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuilder:toStri ng(...)