Messages

Last Msg First Msg

method

com.dmdirc.config.prefs.validator.StringLengthVali dator__static_init

method	ValidationResponse validate(Object)
pre	x0 != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
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*)}
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
unanalyzed	call on java.lang.String:length

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

method	ValidationResponse validate(String)
pre	object != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value in Addr_Set{&new ValidationRespons e(validate#1),&new ValidationResponse(validate# 3),&new ValidationResponse(validate#5)}
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
test_vector	this.max: {0..2³²-2}, {-1}

Prev Msg Next Msg

test always goes same way

click for all messages in this file Low Prob.

Test predetermined because this.min in {1..2³²-1}

Prev Msg Next Msg