StringLengthValidator.java

StringLengthValidator.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.StringLengthValidator(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.StringLengthValidator__static_init

Kind	Annotation Text

ValidationResponse validate(Object)

Kind	Annotation Text
pre	x0 != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	new ValidationResponse(validate#1*) num objects <= 1
post	new ValidationResponse(validate#1*).failure == &java.lang.StringBuilder:toString(...)
post	new ValidationResponse(validate#3*) num objects <= 1
post	new ValidationResponse(validate#3*).failure == &java.lang.StringBuilder:toString(...)
post	new ValidationResponse(validate#5*) num objects <= 1
post	new ValidationResponse(validate#5*).failure == null
post	return_value == One-of{&new ValidationResponse( validate#1), &new ValidationResponse(validate# 3), &new ValidationResponse(validate#5*)}
post	return_value in Addr_Set{&new ValidationRespons e(validate#1),&new ValidationResponse(validate #3),&new ValidationResponse(validate#5*)}
unanalyzed	call on java.lang.String:length

ValidationResponse validate(String)

Kind	Annotation Text
pre	object != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	new ValidationResponse(validate#1) num objects <= 1
post	new ValidationResponse(validate#1).failure == &java.lang.StringBuilder:toString(...)
post	new ValidationResponse(validate#3) num objects <= 1
post	new ValidationResponse(validate#3).failure == &java.lang.StringBuilder:toString(...)
post	new ValidationResponse(validate#5) num objects <= 1
post	new ValidationResponse(validate#5).failure == null
post	return_value in Addr_Set{&new ValidationRespons e(validate#1),&new ValidationResponse(validate# 3),&new ValidationResponse(validate#5)}
test_vector	this.max: {0..2³²-2}, {-1}