NumericalValidator.java

NumericalValidator.java

current inspection = 2009-09-03 21:56:13 (id #1)

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void com.dmdirc.config.prefs.validator.NumericalValidator(int, int)

Kind	Annotation Text
post	init'ed(this.max)
post	init'ed(this.min)
post	this.max == max
post	this.min == min

com.dmdirc.config.prefs.validator.NumericalValidator__static_init

Kind	Annotation Text

Kind	Annotation Text
post	return_value != -1
post	return_value == One-of{2³¹-1, this.max}

Kind	Annotation Text
post	return_value != -1
post	return_value == One-of{-2³¹, this.min}

ValidationResponse validate(Object)

Kind	Annotation Text
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	new ValidationResponse(validate#1*) num objects <= 1
post	new ValidationResponse(validate#1*).failure == &"Must be a valid number"
post	new ValidationResponse(validate#2*) num objects <= 1
post	new ValidationResponse(validate#2*).failure == &java.lang.StringBuilder:toString(...)
post	new ValidationResponse(validate#4*) num objects <= 1
post	new ValidationResponse(validate#4*).failure == &java.lang.StringBuilder:toString(...)
post	new ValidationResponse(validate#6*) num objects <= 1
post	new ValidationResponse(validate#6*).failure == null
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)}
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Throwable:__curr_excep_obj

ValidationResponse validate(String)

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