Messages

method

com.dmdirc.actions.ConditionTree__static_init

method	ConditionTree$OPERATION[] values()
pre	(soft) init'ed($VALUES[...])
post	return_value == &new ConditionTree$OPERATION[]( values#1)
post	new ConditionTree$OPERATION[](values#1) num objects == 1
post	return_value.length == 5
post	return_value[...] == One-of{$VALUES[...], undefined}

method	ConditionTree$OPERATION valueOf(String)
post	init'ed(return_value)

method

void com.dmdirc.actions.ConditionTree$OPERATION(St ring, int)

method	com.dmdirc.actions.ConditionTree$OPERATION__ static_init
post	$VALUES == &new ConditionTree$OPERATION[](Condi tionTree$OPERATION__static_init#6)
post	AND == &new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#1)
post	$VALUES[0] == &new ConditionTree$OPERATION(Cond itionTree$OPERATION__static_init#1)
post	NOOP == &new ConditionTree$OPERATION(ConditionT ree$OPERATION__static_init#5)
post	$VALUES[4] == &new ConditionTree$OPERATION(Cond itionTree$OPERATION__static_init#5)
post	NOT == &new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#4)
post	$VALUES[3] == &new ConditionTree$OPERATION(Cond itionTree$OPERATION__static_init#4)
post	OR == &new ConditionTree$OPERATION(ConditionTre e$OPERATION__static_init#2)
post	$VALUES[1] == &new ConditionTree$OPERATION(Cond itionTree$OPERATION__static_init#2)
post	VAR == &new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#3)
post	$VALUES[2] == &new ConditionTree$OPERATION(Cond itionTree$OPERATION__static_init#3)
post	new ConditionTree$OPERATION(ConditionTree$OPERATION __static_init#1) num objects == 1
post	new ConditionTree$OPERATION(ConditionTree$OPERATION __static_init#2) num objects == 1
post	new ConditionTree$OPERATION(ConditionTree$OPERATION __static_init#3) num objects == 1
post	new ConditionTree$OPERATION(ConditionTree$OPERATION __static_init#4) num objects == 1
post	new ConditionTree$OPERATION(ConditionTree$OPERATION __static_init#5) num objects == 1
post	new ConditionTree$OPERATION[](ConditionTree$OPERATI ON__static_init#6) num objects == 1
post	$VALUES.length == 5
unanalyzed	call on java.lang.Enum

method	void com.dmdirc.actions.ConditionTree(ConditionTre e$OPERATION, ConditionTree, ConditionTree)
post	this.argument == -1
post	this.leftArg == leftArg
post	init'ed(this.leftArg)
post	this.op == op
post	init'ed(this.op)
post	this.rightArg == rightArg
post	init'ed(this.rightArg)

method	void com.dmdirc.actions.ConditionTree(ConditionTre e$OPERATION, ConditionTree)
post	this.argument == -1
post	this.leftArg == argument
post	init'ed(this.leftArg)
post	this.op == op
post	init'ed(this.op)
post	this.rightArg == null

method	void com.dmdirc.actions.ConditionTree(int)
post	this.argument == argument
post	init'ed(this.argument)
post	this.leftArg == null
post	this.rightArg == null
post	this.op == &com.dmdirc.actions.ConditionTree$OP ERATION__static_init.new ConditionTree$OPERATION(Co nditionTree$OPERATION__static_init#3)

method	void com.dmdirc.actions.ConditionTree()
post	this.argument == -1
post	this.leftArg == null
post	this.rightArg == null
post	this.op == &com.dmdirc.actions.ConditionTree$OP ERATION__static_init.new ConditionTree$OPERATION(Co nditionTree$OPERATION__static_init#5)

method	int getMaximumArgument()
pre	(soft) init'ed(this...argument)
pre	(soft) this...leftArg != null
pre	(soft) this...rightArg != null
pre	(soft) init'ed(this.argument)
pre	(soft) this.leftArg != null
pre	(soft) this.rightArg != null
post	init'ed(return_value)
unanalyzed	call on getMaximumArgument
unanalyzed	call on java.lang.Math:max

method	com.dmdirc.actions.ConditionTree$1__static_init
pre	(soft) init'ed(com.dmdirc.actions.ConditionTree$OPE RATION__static_init.new ConditionTree$OPERATION[](C onditionTree$OPERATION__static_init#6)[...])
presumption	com.dmdirc.actions.ConditionTree_OPERATION:ordinal( ...)@131 in {0..4}
presumption	com.dmdirc.actions.ConditionTree_OPERATION:ordinal( ...)@131 - values(...).length in range
post	new int[](ConditionTree$1__static_init#1) num objects == 1

method	bool evaluate(bool[])
pre	this.op != null
pre	(soft) init'ed(com.dmdirc.actions.ConditionTree$1__ static_init.new int[](ConditionTree$1__static_init# 1)[...])
pre	(soft) conditions != null
pre	(soft) conditions.length >= 1
pre	(soft) this.argument < conditions.length
pre	(soft) init'ed(conditions[...])
pre	(soft) this...argument >= 0
pre	(soft) this...leftArg != null
pre	(soft) this...op != null
pre	(soft) this...rightArg != null
pre	(soft) this.argument >= 0
pre	(soft) this.leftArg != null
pre	(soft) this.rightArg != null
presumption	com.dmdirc.actions.ConditionTree_OPERATION:ordinal( ...)@131 in {0..4}
post	init'ed(return_value)
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on evaluate
test_vector	com.dmdirc.actions.ConditionTree$1__static_init. new int[](ConditionTree$1__static_init#1)[...]: {1}, {2}, {3}, {4}, {-2³¹..0, 5..2³²-1}

method not available - call not analyzed Info call on int com.dmdirc.actions.ConditionTree$OPERAT ION:ordinal()

method not available - call not analyzed Info call on int com.dmdirc.actions.ConditionTree$OPERAT ION:ordinal()

method	bool equals(Object)
pre	(soft) init'ed(com.dmdirc.actions.ConditionTree$1__ static_init.new int[](ConditionTree$1__static_init# 1)[...])
pre	(soft) init'ed(obj.argument)
pre	(soft) init'ed(obj.leftArg)
pre	(soft) obj.op != null
pre	(soft) init'ed(obj.rightArg)
pre	(soft) init'ed(this.argument)
pre	(soft) init'ed(this.leftArg)
pre	(soft) this.op != null
pre	(soft) init'ed(this.rightArg)
post	init'ed(return_value)
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on java.lang.String:valueOf

method	int hashCode()
pre	this.op != null
pre	(soft) init'ed(com.dmdirc.actions.ConditionTree$1__ static_init.new int[](ConditionTree$1__static_init# 1)[...])
pre	(soft) init'ed(this.argument)
pre	(soft) init'ed(this.leftArg)
pre	(soft) init'ed(this.rightArg)
post	init'ed(return_value)
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on java.lang.String:valueOf

method	String toString()
pre	this.op != null
pre	(soft) init'ed(com.dmdirc.actions.ConditionTree$1__ static_init.new int[](ConditionTree$1__static_init# 1)[...])
pre	(soft) init'ed(this.argument)
pre	(soft) init'ed(this.leftArg)
pre	(soft) init'ed(this.rightArg)
presumption	com.dmdirc.actions.ConditionTree_OPERATION:ordinal( ...)@168 in {0..4}
post	java.lang.String:valueOf(...)._tainted == 0
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value in Addr_Set{&java.lang. String:valueOf(...),&java.lang.StringBuilder:to String(...),&java.lang.StringBuilder:toString(. ..),&java.lang.StringBuilder:toString(...), &""}
test_vector	com.dmdirc.actions.ConditionTree$1__static_init. new int[](ConditionTree$1__static_init#1)[...]: {1}, {2}, {3}, {4}, {-2³¹..0, 5..2³²-1}

method not available - call not analyzed Info call on int com.dmdirc.actions.ConditionTree$OPERAT ION:ordinal()

method	ConditionTree parseString(String)
pre	string != null
post	init'ed(return_value)
post	new ConditionTree(parseStack#3) num objects <= 1
post	new ConditionTree(parseStack#3).argument == -1
post	new ConditionTree(parseStack#3).leftArg == null
post	new ConditionTree(parseStack#3).op == &com.dmdirc.actions.ConditionTree$OPERATION__ static_init.new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#5)
post	new ConditionTree(parseStack#3).rightArg == null
post	init'ed(new ConditionTree(readTerm#1) num objects)
post	new ConditionTree(readTerm#1).argument == 0, if init'ed
post	new ConditionTree(readTerm#1).leftArg == null
post	new ConditionTree(readTerm#1).op == null
post	new ConditionTree(readTerm#1).rightArg == null
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on readTerm
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on parseStack
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:size
test_vector	java.lang.String:charAt(...)@193: {32}, {48..57}, {9}, {10}, {13}, {0..8, 11,12, 14..31, 33..47, 58..2¹⁶-1}
test_vector	java.lang.String:charAt(...)@198: {0..47, 58..2¹⁶-1}, {48..57}

method	ConditionTree parseStack(Deque)
pre	stack != null
post	init'ed(return_value)
post	new ConditionTree(parseStack#3) num objects <= 1
post	new ConditionTree(parseStack#3).argument == -1
post	new ConditionTree(parseStack#3).leftArg == null
post	new ConditionTree(parseStack#3).op == &com.dmdirc.actions.ConditionTree$OPERATION__ static_init.new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#5)
post	new ConditionTree(parseStack#3).rightArg == null
post	init'ed(new ConditionTree(readTerm#1) num objects)
post	not_init'ed(new ConditionTree(readTerm#1). argument)
post	not_init'ed(new ConditionTree(readTerm#1).leftArg)
post	not_init'ed(new ConditionTree(readTerm#1).op)
post	not_init'ed(new ConditionTree(readTerm#1). rightArg)
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on readTerm
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on parseStack
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:size
test_vector	java.lang.Character:charValue(...)@230: {0..40, 42..2¹⁶-1}, {41}
test_vector	java.lang.Character:charValue(...)@271: {0..37, 39..2¹⁶-1}, {38}
test_vector	java.lang.Character:charValue(...)@273: {0..123, 125..2¹⁶-1}, {124}
test_vector	java.util.Deque:isEmpty(...)@227: {1}, {0}
test_vector	java.util.Deque:isEmpty(...)@243: {1}, {0}
test_vector	java.util.Deque:isEmpty(...)@257: {0}, {1}
test_vector	java.util.Deque:isEmpty(...)@263: {0}, {1}
test_vector	java.util.Deque:size(...)@244: {-2³¹..0, 2..2³²-1}, {1}

method	ConditionTree readTerm(Deque)
pre	stack != null
post	init'ed(return_value)
post	new ConditionTree(readTerm#1) num objects <= 1
post	new ConditionTree(readTerm#1).argument == -1
post	init'ed(new ConditionTree(readTerm#1).leftArg)
post	new ConditionTree(readTerm#1).op == &com.dmdirc.actions.ConditionTree$OPERATION__ static_init.new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#4)
post	new ConditionTree(readTerm#1).rightArg == null
post	new ConditionTree(readTerm#1*) num objects <= 1
post	not_init'ed(new ConditionTree(readTerm#1*). argument)
post	not_init'ed(new ConditionTree(readTerm#1*). leftArg)
post	not_init'ed(new ConditionTree(readTerm#1*).op)
post	not_init'ed(new ConditionTree(readTerm#1*). rightArg)
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on readTerm
test_vector	java.lang.Character:charValue(...)@299: {0..32, 34..2¹⁶-1}, {33}
test_vector	java.util.Deque:isEmpty(...)@300: {0}, {1}

method	ConditionTree readBracket(Deque)
pre	(soft) stack != null
post	init'ed(return_value)
post	new ConditionTree(parseStack#3) num objects <= 1
post	new ConditionTree(parseStack#3).argument == -1
post	new ConditionTree(parseStack#3).leftArg == null
post	new ConditionTree(parseStack#3).op == &com.dmdirc.actions.ConditionTree$OPERATION__ static_init.new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#5)
post	new ConditionTree(parseStack#3).rightArg == null
post	init'ed(new ConditionTree(readTerm#1) num objects)
post	new ConditionTree(readTerm#1).argument == 0, if init'ed
post	new ConditionTree(readTerm#1).leftArg == null
post	new ConditionTree(readTerm#1).op == null
post	new ConditionTree(readTerm#1).rightArg == null
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on readTerm
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on parseStack
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:size
test_vector	java.lang.Character:charValue(...)@329: {0..39, 41..2¹⁶-1}, {40}
test_vector	java.util.Deque:isEmpty(...)@326: {1}, {0}

method	bool isInt(char)
post	init'ed(return_value)

method	ConditionTree createDisjunction(int)
post	init'ed(return_value)
post	new ConditionTree(parseStack#3) num objects <= 1
post	new ConditionTree(parseStack#3).argument == -1
post	new ConditionTree(parseStack#3).leftArg == null
post	new ConditionTree(parseStack#3).op == &com.dmdirc.actions.ConditionTree$OPERATION__ static_init.new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#5)
post	new ConditionTree(parseStack#3).rightArg == null
post	init'ed(new ConditionTree(readTerm#1) num objects)
post	new ConditionTree(readTerm#1).argument == 0, if init'ed
post	new ConditionTree(readTerm#1).leftArg == null
post	new ConditionTree(readTerm#1).op == null
post	new ConditionTree(readTerm#1).rightArg == null
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on readTerm
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on parseStack
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:size
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.Character:valueOf
test_vector	java.lang.StringBuilder:length(...)@364: {0}, {-2³¹..-1, 1..2³²-1}

method	ConditionTree createConjunction(int)
post	init'ed(return_value)
post	new ConditionTree(parseStack#3) num objects <= 1
post	new ConditionTree(parseStack#3).argument == -1
post	new ConditionTree(parseStack#3).leftArg == null
post	new ConditionTree(parseStack#3).op == &com.dmdirc.actions.ConditionTree$OPERATION__ static_init.new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#5)
post	new ConditionTree(parseStack#3).rightArg == null
post	init'ed(new ConditionTree(readTerm#1) num objects)
post	new ConditionTree(readTerm#1).argument == 0, if init'ed
post	new ConditionTree(readTerm#1).leftArg == null
post	new ConditionTree(readTerm#1).op == null
post	new ConditionTree(readTerm#1).rightArg == null
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:charValue
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on readTerm
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on parseStack
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:size
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.lang.Character:valueOf
test_vector	java.lang.StringBuilder:length(...)@385: {0}, {-2³¹..-1, 1..2³²-1}

	method not available - call not analyzed	Info	call on int com.dmdirc.actions.ConditionTree$OPERAT ION:ordinal()
	method not available - call not analyzed	Info	call on int com.dmdirc.actions.ConditionTree$OPERAT ION:ordinal()