Messages

Last Msg First Msg

method	com.dmdirc.ui.messages.Formatter__static_init
post	typeCache == &new HashMap(Formatter__static_ init#1)
post	new HashMap(Formatter__static_init#1) num objects == 1

method

void com.dmdirc.ui.messages.Formatter()

method	String formatMessage(ConfigManager, String, Object[])
pre	config != null
pre	messageType != null
pre	(soft) arguments != null
pre	(soft) arguments.length <= 2³²-1
pre	(soft) arguments[...] != 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.String:indexOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:containsKey
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Integer:valueOf
unanalyzed	call on java.lang.Float:valueOf
unanalyzed	call on java.lang.String:instanceof
unanalyzed	call on java.lang.Long:valueOf
unanalyzed	call on java.lang.Long:longValue
unanalyzed	call on java.lang.Object:toString
unanalyzed	call on java.lang.Integer:intValue
test_vector	com.dmdirc.config.ConfigManager:hasOptionString(... )@66: {1}, {0}

method not available - call not analyzed Info call on bool com.dmdirc.config.ConfigManager:hasOpt ionString(String, String)

method not available - call not analyzed Info call on String com.dmdirc.config.ConfigManager:getO ption(String, String)

method	Object[] castArguments(String, Object[])
pre	args != null
pre	format != null
pre	(soft) args.length <= 2³²-1
pre	(soft) args[...] != null
presumption	arr$.length@108 <= 2³²-1
presumption	arr$.length@108 - args.length in {-2³²+1.. 0}
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	return_value == &new Object[](castArguments#1)
post	new Object[](castArguments#1) num objects == 1
post	return_value.length == args.length
post	return_value.length <= 2³²-1
post	possibly_updated(return_value[...])
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.Character:valueOf
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}

method	int doDuration(StringBuilder, int, int, String)
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	return_value == One-of{0, duration*(current/duratio n)}
post	init'ed(return_value)
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}

method	String formatDuration(int)
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value == &java.lang.StringBuilder:toStri ng(...)
unanalyzed	call on java.lang.Character:valueOf

Prev Msg Next Msg

unused assignment in callee

click for all messages in this file Low Prob.

Unused assignment to (java.lang.StringBuilder:appen d.return_value@176._tainted) in doDuration

Prev Msg Next Msg

Prev Msg Next Msg

unused assignment

click for all messages in this file Low Prob.

Unused assignment into seconds

Prev Msg Next Msg

method	void analyseFormat(String, Object[])
pre	args != null
pre	args.length <= 2³²-1
pre	(soft) format != null
presumption	java.lang.String:indexOf(...)@212 <= 2³²-4
test_vector	java.lang.String:indexOf(...)@212: {-2³¹. .-1}, {0..2³²-4}

	method not available - call not analyzed	Info	call on bool com.dmdirc.config.ConfigManager:hasOpt ionString(String, String)
	method not available - call not analyzed	Info	call on String com.dmdirc.config.ConfigManager:getO ption(String, String)