method

com.dmdirc.config.prefs.validator.NumericalValidat or__static_init

method	ValidationResponse validate(Object)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value == One-of{&new ValidationResponse( validate#1*), &new ValidationResponse(validate# 2*), &new ValidationResponse(validate#4*), &new ValidationResponse(validate#6*)}
post	return_value in Addr_Set{&new ValidationRespons e(validate#1*),&new ValidationResponse(validate #2*),&new ValidationResponse(validate#4*), &new ValidationResponse(validate#6*)}
post	new ValidationResponse(validate#1*) num objects <= 1
post	new ValidationResponse(validate#1*).failure == &amp;"Must be a valid number"
post	new ValidationResponse(validate#2*) num objects <= 1
post	new ValidationResponse(validate#2*).failure == &amp;java.lang.StringBuilder:toString(...)
post	new ValidationResponse(validate#4*) num objects <= 1
post	new ValidationResponse(validate#4*).failure == &amp;java.lang.StringBuilder:toString(...)
post	new ValidationResponse(validate#6*) num objects <= 1
post	new ValidationResponse(validate#6*).failure == null
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Throwable:__curr_excep_obj

method	void com.dmdirc.config.prefs.validator. NumericalValidator(int, int)
post	this.max == max
post	init'ed(this.max)
post	this.min == min
post	init'ed(this.min)

method	int getMax()
post	return_value == One-of{231-1, this.max}
post	return_value != -1

method	int getMin()
post	return_value == One-of{-231, this.min}
post	return_value != -1

method	ValidationResponse validate(String)
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value in Addr_Set{&new ValidationRespons e(validate#2),&new ValidationResponse(validate# 4),&new ValidationResponse(validate#6), &new ValidationResponse(validate#1)}
post	new ValidationResponse(validate#1) num objects <= 1
post	new ValidationResponse(validate#1).failure == &amp;"Must be a valid number"
post	new ValidationResponse(validate#2) num objects <= 1
post	new ValidationResponse(validate#2).failure == &amp;java.lang.StringBuilder:toString(...)
post	new ValidationResponse(validate#4) num objects <= 1
post	new ValidationResponse(validate#4).failure == &amp;java.lang.StringBuilder:toString(...)
post	new ValidationResponse(validate#6) num objects <= 1
post	new ValidationResponse(validate#6).failure == null
test_vector	this.max: {-1}, {-231..-2, 0..232-2}
test_vector	this.min: {-1}, {-231+1..-2, 0..232-1}
test_vector	java.lang.Integer:parseInt(...)@72: {-231..-2}, {0..232-1}