method

com.dmdirc.installer.cliparser.IntegerParam__ static_init

method	void com.dmdirc.installer.cliparser. IntegerParam(char, String, String)
post	this.charFlag == chr
post	init'ed(this.charFlag)
post	this.description == desc
post	init'ed(this.description)
post	this.myValue == 0
post	this.stringFlag == str
post	init'ed(this.stringFlag)

method	bool setValue(String)
post	init'ed(return_value)
post	possibly_updated(this.myValue)

method	int getValue()
pre	init'ed(this.myValue)
post	return_value == this.myValue
post	init'ed(return_value)

method	String getStringValue()
pre	init'ed(this.myValue)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuilder:toStri ng(...)