Messages

method

com.dmdirc.util.WeakList__static_init

method	void com.dmdirc.util.WeakList()
post	this.list == &new ArrayList(WeakList#1)
post	new ArrayList(WeakList#1) num objects == 1

method	void cleanUp()
pre	this.list != null
presumption	java.util.List:get(...)@56 != null
test_vector	java.lang.ref.WeakReference:get(...)@56: Inverse{null}, Addr_Set{null}

method	List dereferenceList(List)
pre	list != null
presumption	java.util.Iterator:next(...)@71 != null
post	return_value == &new ArrayList(dereferenceList# 1)
post	new ArrayList(dereferenceList#1) num objects == 1
test_vector	java.lang.ref.WeakReference:get(...)@72: Addr_Set{null}, Inverse{null}
test_vector	java.util.Iterator:hasNext(...)@71: {0}, {1}

method	Collection referenceCollection(Collection)
pre	c != null
post	return_value == &new ArrayList(referenceCollect ion#1)
post	new ArrayList(referenceCollection#1) num objects == 1
unanalyzed	call on java.lang.ref.WeakReference
test_vector	java.util.Iterator:hasNext(...)@92: {0}, {1}

method	int size()
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:remove

method	bool isEmpty()
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:remove

method	bool contains(Object)
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.lang.ref.WeakReference

method	Iterator iterator()
pre	this.list != null
post	return_value != null
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add

method	Object[] toArray()
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add

method	Object[] toArray(Object[])
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add

method	bool add(Object)
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.lang.ref.WeakReference

method	bool remove(Object)
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.lang.ref.WeakReference

method	bool containsAll(Collection)
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add

method	bool addAll(Collection)
pre	c != null
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on java.lang.ref.WeakReference
unanalyzed	call on java.util.Collection:add

method	bool addAll(int, Collection)
pre	c != null
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on java.lang.ref.WeakReference
unanalyzed	call on java.util.Collection:add

method	bool removeAll(Collection)
pre	c != null
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on java.lang.ref.WeakReference
unanalyzed	call on java.util.Collection:add

method	bool retainAll(Collection)
pre	c != null
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on java.lang.ref.WeakReference
unanalyzed	call on java.util.Collection:add

method	void clear()
pre	this.list != null

method	Object get(int)
pre	this.list != null
presumption	java.util.List:get(...)@192 != null
post	init'ed(return_value)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:remove

method	Object set(int, Object)
pre	this.list != null
post	return_value == element
post	init'ed(return_value)
unanalyzed	call on java.lang.ref.WeakReference

method	void add(int, Object)
pre	this.list != null
unanalyzed	call on java.lang.ref.WeakReference

method	Object remove(int)
pre	this.list != null
presumption	java.util.List:remove(...)@212 != null
post	init'ed(return_value)

method	int indexOf(Object)
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:remove

method	int lastIndexOf(Object)
pre	this.list != null
post	init'ed(return_value)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:remove

method	ListIterator listIterator()
pre	this.list != null
post	return_value != null
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:remove
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add

method	ListIterator listIterator(int)
pre	this.list != null
post	return_value != null
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:remove
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add

method	List subList(int, int)
pre	this.list != null
presumption	java.util.List:subList(...)@250 != null
post	return_value == &new ArrayList(dereferenceList# 1)
post	new ArrayList(dereferenceList#1) num objects == 1
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.lang.ref.WeakReference:get
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add