FileNameValidator.java

FileNameValidator.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.FileNameValidator()

Kind	Annotation Text

com.dmdirc.config.prefs.validator.FileNameValidator__static_init

Kind	Annotation Text

ValidationResponse validate(Object)

Kind	Annotation Text
pre	x0 != null
post	new ValidationResponse(validate#1*) num objects <= 1
post	new ValidationResponse(validate#1*).failure == null
post	new ValidationResponse(validate#2*) num objects <= 1
post	new ValidationResponse(validate#2*).failure == &"Must be a valid filename"
post	return_value == One-of{&new ValidationResponse( validate#1), &new ValidationResponse(validate# 2)}
post	return_value in Addr_Set{&new ValidationRespons e(validate#1),&new ValidationResponse(validate #2)}
unanalyzed	call on java.lang.String:matches

ValidationResponse validate(String)

Kind	Annotation Text
pre	object != null
post	new ValidationResponse(validate#1) num objects <= 1
post	new ValidationResponse(validate#1).failure == null
post	new ValidationResponse(validate#2) num objects <= 1
post	new ValidationResponse(validate#2).failure == &"Must be a valid filename"
post	return_value in Addr_Set{&new ValidationRespons e(validate#2),&new ValidationResponse(validate# 1)}
test_vector	java.lang.String:matches(...)@45: {0}, {1}