Formatter.java

Formatter.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

Kind	Annotation Text
pre	(soft) args.length <= 2³²-1
pre	(soft) args[...] != null
pre	args != null
pre	format != null
presumption	arr$.length@108 - args.length in {-2³²+1.. 0}
presumption	arr$.length@108 <= 2³²-1
presumption	arr$[i$]@108 != null
presumption	java.lang.Integer:valueOf(...)@141 != null
presumption	java.lang.Long:longValue(...)@134 in {-9_223_372_036_854_775..18_446_744_073_709_551}
presumption	java.lang.Long:valueOf(...)@134 != null
presumption	java.util.Map:get(...)@108 != null
post	init'ed(java.lang.String:valueOf(...)._tainted)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	new Object[](castArguments#1) num objects == 1
post	possibly_updated(return_value[...])
post	return_value == &new Object[](castArguments#1)
post	return_value.length <= 2³²-1
post	return_value.length == args.length
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.util.Map:put
test_vector	java.lang.Character:charValue(...)@113: {65, 69, 71, 97, 101..103}, {66, 72, 83, 98, 104, 115}, {67, 99}, {84, 116}, {88, 100, 111, 120}, {117}, {0..64, 68, 70, 73..82, 85..87, 89..96, 105..110, 112..114, 118,119, 121..2¹⁶-1}
test_vector	java.lang.String:instanceof(...)@132: {0}, {1}
test_vector	java.util.Map:containsKey(...)@101: {1}, {0}

Kind	Annotation Text

Kind	Annotation Text
post	new HashMap(Formatter__static_init#1) num objects == 1
post	typeCache == &new HashMap(Formatter__static_ init#1)

Kind	Annotation Text
pre	(soft) builder != null
pre	(soft) current/duration in {-2³¹.. 2³²-1}
pre	(soft) duration != 0
pre	(soft) duration*(current/duration) in {-2³¹..2³²-1}
post	init'ed(builder._tainted)
post	init'ed(return_value)
post	return_value == One-of{0, duration*(current/duratio n)}
test_vector	duration - current: {1..6_442_450_943}, {-6_442_450_943..0}
test_vector	java.lang.StringBuilder:length(...)@170: {-2³¹..0}, {1..2³²-1}

Kind	Annotation Text
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &java.lang.StringBuilder:toStri ng(...)
unanalyzed	call on java.lang.Character:valueOf

Kind	Annotation Text
pre	(soft) arguments != null
pre	(soft) arguments.length <= 2³²-1
pre	(soft) arguments[...] != null
pre	config != null
pre	messageType != null
presumption	com.dmdirc.config.ConfigManager:getOption(...)@66 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	init'ed(return_value)
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Float:valueOf
unanalyzed	call on java.lang.Integer:intValue
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.Long:longValue
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.Object:toString
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:instanceof
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.Map:put
test_vector	com.dmdirc.config.ConfigManager:hasOptionString(... )@66: {1}, {0}