Messages

method

com.dmdirc.addons.ui_swing.wizard.StepLayout__ static_init

method	void com.dmdirc.addons.ui_swing.wizard. StepLayout()
post	this.currentStep == -1
post	this.hGap == 0
post	this.vGap == 0
post	this.steps == &new ArrayList(StepLayout#1)
post	new ArrayList(StepLayout#1) num objects == 1
unanalyzed	call on java.util.ArrayList

method	void com.dmdirc.addons.ui_swing.wizard. StepLayout(Container)
post	this.currentStep == -1
post	this.hGap == 0
post	this.vGap == 0
post	this.parent == parent
post	init'ed(this.parent)
post	this.steps == &new ArrayList(StepLayout#1)
post	new ArrayList(StepLayout#1) num objects == 1
unanalyzed	call on java.util.ArrayList

method	void com.dmdirc.addons.ui_swing.wizard. StepLayout(int, int)
post	this.currentStep == -1
post	this.hGap == hGap
post	init'ed(this.hGap)
post	this.steps == &new ArrayList(StepLayout#1)
post	this.vGap == vGap
post	init'ed(this.vGap)
post	new ArrayList(StepLayout#1) num objects == 1

method	void com.dmdirc.addons.ui_swing.wizard. StepLayout(int, int, Container)
post	this.currentStep == -1
post	this.hGap == hGap
post	init'ed(this.hGap)
post	this.parent == parent
post	init'ed(this.parent)
post	this.steps == &new ArrayList(StepLayout#1)
post	this.vGap == vGap
post	init'ed(this.vGap)
post	new ArrayList(StepLayout#1) num objects == 1

method	int size()
pre	this.steps != null
post	init'ed(return_value)

method	bool isEmpty()
pre	this.steps != null
post	init'ed(return_value)

method	Step getStep(int)
pre	this.steps != null
post	init'ed(return_value)

method	List getSteps()
post	return_value == this.steps
post	init'ed(return_value)

method	void first(Container)
pre	parent != null
pre	(soft) this.steps != null
post	possibly_updated(this.currentStep)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.awt.Container:validate

method	void last(Container)
pre	parent != null
pre	(soft) this.steps != null
presumption	java.awt.Container:getComponentCount(...)@153 >= -2³¹+1
post	possibly_updated(this.currentStep)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.awt.Container:validate

method	void next(Container)
pre	this.currentStep <= 2³²-2
pre	parent != null
pre	(soft) this.steps != null
post	init'ed(this.currentStep)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.awt.Container:validate

method	void previous(Container)
pre	this.currentStep >= -2³¹+1
pre	parent != null
pre	(soft) this.steps != null
post	init'ed(this.currentStep)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.awt.Container:validate

method	void show(Step, Container)
pre	parent != null
pre	this.steps != null
post	possibly_updated(this.currentStep)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.awt.Container:validate

method	void show(int, Container)
pre	parent != null
pre	(soft) this.steps != null
presumption	java.awt.Container:getComponent(...)@202 != null
presumption	java.awt.Container:getComponent(...)@210 != null
presumption	java.util.List:size(...)@194 >= -2³¹+1
post	possibly_updated(this.currentStep)
test_vector	step: {-2³¹..-2, 0..2³²-1}, {-1}
test_vector	java.awt.Component:isVisible(...)@203: {0}, {1}
test_vector	java.util.List:size(...)@193: {0..2³²-1}, {-2³¹..-1}

method	void addLayoutComponent(Component, Object)
pre	comp != null
pre	this.steps != null
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on com.dmdirc.addons.ui_swing.wizard. Step:getTreeLock
unanalyzed	call on com.dmdirc.addons.ui_swing.wizard. Step:setVisible
unanalyzed	call on java.util.List:add

method	void addLayoutComponent(String, Component)
pre	comp != null
pre	this.steps != null
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on com.dmdirc.addons.ui_swing.wizard. Step:getTreeLock
unanalyzed	call on com.dmdirc.addons.ui_swing.wizard. Step:setVisible
unanalyzed	call on java.util.List:add

method	void addLayoutComponent(Step)
pre	step != null
pre	this.steps != null
test_vector	java.util.List:isEmpty(...)@251: {1}, {0}

method not available - call not analyzed Info call on Object com.dmdirc.addons.ui_swing.wizard. Step:getTreeLock()

method not available - call not analyzed Info call on void com.dmdirc.addons.ui_swing.wizard. Step:setVisible(bool)

method	void removeLayoutComponent(Component)
pre	comp != null
pre	this.currentStep <= 2³²-2
pre	(soft) this.steps != null
presumption	java.awt.Component:getParent(...)@265 != null
post	init'ed(this.currentStep)
unanalyzed	call on java.util.List:size
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.awt.Container:validate
test_vector	java.awt.Component:isVisible(...)@262: {0}, {1}

method	Dimension preferredLayoutSize(Container)
pre	parent != null
pre	init'ed(this.hGap)
pre	init'ed(this.vGap)
presumption	java.awt.Component:getPreferredSize(...)@285 != null
presumption	java.awt.Container:getComponent(...)@284 != null
presumption	java.awt.Container:getInsets(...)@278 != null
post	return_value == &new Dimension(preferredLayoutS ize#1)
post	new Dimension(preferredLayoutSize#1) num objects == 1

method	Dimension minimumLayoutSize(Container)
pre	parent != null
pre	init'ed(this.hGap)
pre	init'ed(this.vGap)
presumption	java.awt.Component:getMinimumSize(...)@313 != null
presumption	java.awt.Container:getComponent(...)@312 != null
presumption	java.awt.Container:getInsets(...)@306 != null
post	return_value == &new Dimension(minimumLayoutSiz e#1)
post	new Dimension(minimumLayoutSize#1) num objects == 1

method	Dimension maximumLayoutSize(Container)
post	return_value == &new Dimension(maximumLayoutSiz e#1)
post	new Dimension(maximumLayoutSize#1) num objects == 1

method	float getLayoutAlignmentX(Container)
post	return_value == 1/2

method	float getLayoutAlignmentY(Container)
post	return_value == 1/2

method

void invalidateLayout(Container)

method	void layoutContainer(Container)
pre	parent != null
pre	(soft) init'ed(this.hGap)
pre	(soft) init'ed(this.vGap)
presumption	java.awt.Container:getComponent(...)@382 != null
presumption	java.awt.Container:getComponent(...)@393 != null
presumption	java.awt.Container:getHeight(...)@383 - (this.vGap*2 + insets.top@376 + insets. bottom@376) in {-2³¹..2³²-1}
presumption	java.awt.Container:getInsets(...)@376 != null
presumption	java.awt.Container:getWidth(...)@383 - (this.hGap*2 + insets.left@376 + insets. right@376) in {-2³¹..2³²-1}
presumption	this.hGap + insets.left@376 in {-2³¹.. 2³²-1}
presumption	this.hGap*2 + insets.left@376 in {-2³².. 8_589_934_590}
presumption	this.hGap*2 + insets.left@376 + insets.right@376 in {-6_442_450_943..6_442_450_943}
presumption	this.vGap + insets.top@376 in {-2³¹.. 2³²-1}
presumption	this.vGap*2 + insets.top@376 in {-2³².. 8_589_934_590}
presumption	this.vGap*2 + insets.top@376 + insets.bottom@376 in {-6_442_450_943..6_442_450_943}
test_vector	java.awt.Component:isVisible(...)@387: {0}, {1}