Messages

method

com.dmdirc.installer.ui.StepLayout__static_init

method	void com.dmdirc.installer.ui.StepLayout()
post	this.currentStep == -1
post	this.hGap == 0
post	this.vGap == 0
post	this.parent == null
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.installer.ui.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.installer.ui.StepLayout(int, int)
post	this.currentStep == -1
post	this.hGap == hGap
post	init'ed(this.hGap)
post	this.parent == null
post	this.steps == &new ArrayList(StepLayout#1)
post	this.vGap == vGap
post	init'ed(this.vGap)
post	new ArrayList(StepLayout#1) num objects == 1
unanalyzed	call on java.util.ArrayList

method	void com.dmdirc.installer.ui.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	int getCurrentStepIndex()
pre	init'ed(this.currentStep)
post	return_value == this.currentStep
post	init'ed(return_value)

method	String getCurrentStepName()
pre	init'ed(this.currentStep)
pre	this.steps != null
presumption	java.util.List:get(...)@152 != null
post	init'ed(return_value)

method not available - call not analyzed Info call on String com.dmdirc.installer.ui. SwingStep:getStepName()

method	Step getCurrentStep()
pre	init'ed(this.currentStep)
pre	this.steps != null
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(...)@179 >= -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(...)@228 != null
presumption	java.awt.Container:getComponent(...)@236 != null
presumption	java.util.List:size(...)@220 >= -2³¹+1
post	possibly_updated(this.currentStep)
test_vector	step: {-2³¹..-2, 0..2³²-1}, {-1}
test_vector	java.awt.Component:isVisible(...)@229: {0}, {1}
test_vector	java.util.List:size(...)@219: {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.installer.ui.SwingStep:getTreeLo ck
unanalyzed	call on com.dmdirc.installer.ui.SwingStep:setVisibl e
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.installer.ui.SwingStep:getTreeLo ck
unanalyzed	call on com.dmdirc.installer.ui.SwingStep:setVisibl e
unanalyzed	call on java.util.List:add

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

method not available - call not analyzed Info call on Object com.dmdirc.installer.ui. SwingStep:getTreeLock()

method not available - call not analyzed Info call on void com.dmdirc.installer.ui. SwingStep:setVisible(bool)

method	void removeLayoutComponent(Component)
pre	comp != null
pre	this.currentStep <= 2³²-2
pre	(soft) this.steps != null
presumption	java.awt.Component:getParent(...)@293 != 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(...)@290: {0}, {1}

method	Dimension preferredLayoutSize(Container)
pre	parent != null
pre	init'ed(this.hGap)
pre	init'ed(this.vGap)
presumption	java.awt.Component:getPreferredSize(...)@313 != null
presumption	java.awt.Container:getComponent(...)@312 != null
presumption	java.awt.Container:getInsets(...)@306 != 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(...)@341 != null
presumption	java.awt.Container:getComponent(...)@340 != null
presumption	java.awt.Container:getInsets(...)@334 != 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(...)@410 != null
presumption	java.awt.Container:getComponent(...)@422 != null
presumption	java.awt.Container:getHeight(...)@411 - (this.vGap*2 + insets.top@404 + insets. bottom@404) in {-2³¹..2³²-1}
presumption	java.awt.Container:getInsets(...)@404 != null
presumption	java.awt.Container:getWidth(...)@411 - (this.hGap*2 + insets.left@404 + insets. right@404) in {-2³¹..2³²-1}
presumption	this.hGap + insets.left@404 in {-2³¹.. 2³²-1}
presumption	this.hGap*2 + insets.left@404 in {-2³².. 8_589_934_590}
presumption	this.hGap*2 + insets.left@404 + insets.right@404 in {-6_442_450_943..6_442_450_943}
presumption	this.vGap + insets.top@404 in {-2³¹.. 2³²-1}
presumption	this.vGap*2 + insets.top@404 in {-2³².. 8_589_934_590}
presumption	this.vGap*2 + insets.top@404 + insets.bottom@404 in {-6_442_450_943..6_442_450_943}
test_vector	java.awt.Component:isVisible(...)@416: {0}, {1}