ConditionTree.java

ConditionTree.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

com.dmdirc.actions.ConditionTree$1__static_init

Kind	Annotation Text
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 - values(...).length in range
presumption	com.dmdirc.actions.ConditionTree_OPERATION:ordinal( ...)@131 in {0..4}
post	new int[](ConditionTree$1__static_init#1) num objects == 1

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

Kind	Annotation Text

com.dmdirc.actions.ConditionTree$OPERATION__static_init

Kind	Annotation Text
post	$VALUES == &new ConditionTree$OPERATION[](Condi tionTree$OPERATION__static_init#6)
post	$VALUES.length == 5
post	$VALUES[0] == &new ConditionTree$OPERATION(Cond itionTree$OPERATION__static_init#1)
post	$VALUES[1] == &new ConditionTree$OPERATION(Cond itionTree$OPERATION__static_init#2)
post	$VALUES[2] == &new ConditionTree$OPERATION(Cond itionTree$OPERATION__static_init#3)
post	$VALUES[3] == &new ConditionTree$OPERATION(Cond itionTree$OPERATION__static_init#4)
post	$VALUES[4] == &new ConditionTree$OPERATION(Cond itionTree$OPERATION__static_init#5)
post	AND == &new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#1)
post	NOOP == &new ConditionTree$OPERATION(ConditionT ree$OPERATION__static_init#5)
post	NOT == &new ConditionTree$OPERATION(ConditionTr ee$OPERATION__static_init#4)
post	OR == &new ConditionTree$OPERATION(ConditionTre e$OPERATION__static_init#2)
post	VAR == &new ConditionTree$OPERATION(ConditionTr ee$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
unanalyzed	call on java.lang.Enum

void com.dmdirc.actions.ConditionTree()

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

void com.dmdirc.actions.ConditionTree(int)

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

void com.dmdirc.actions.ConditionTree(ConditionTree$OPERATION, ConditionTree)

Kind	Annotation Text
post	init'ed(this.leftArg)
post	init'ed(this.op)
post	this.argument == -1
post	this.leftArg == argument
post	this.op == op
post	this.rightArg == null

void com.dmdirc.actions.ConditionTree(ConditionTree$OPERATION, ConditionTree, ConditionTree)

Kind	Annotation Text
post	init'ed(this.leftArg)
post	init'ed(this.op)
post	init'ed(this.rightArg)
post	this.argument == -1
post	this.leftArg == leftArg
post	this.op == op
post	this.rightArg == rightArg

com.dmdirc.actions.ConditionTree__static_init

Kind	Annotation Text

ConditionTree createConjunction(int)

Kind	Annotation Text
post	init'ed(new ConditionTree(readTerm#1) num objects)
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	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.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:size
unanalyzed	call on parseStack
unanalyzed	call on readTerm
test_vector	java.lang.StringBuilder:length(...)@385: {0}, {-2³¹..-1, 1..2³²-1}

ConditionTree createDisjunction(int)

Kind	Annotation Text
post	init'ed(new ConditionTree(readTerm#1) num objects)
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	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.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.lang.Character:valueOf
unanalyzed	call on java.lang.Integer:parseInt
unanalyzed	call on java.lang.String:charAt
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:size
unanalyzed	call on parseStack
unanalyzed	call on readTerm
test_vector	java.lang.StringBuilder:length(...)@364: {0}, {-2³¹..-1, 1..2³²-1}

bool equals(Object)

Kind	Annotation Text
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) init'ed(obj.rightArg)
pre	(soft) init'ed(this.argument)
pre	(soft) init'ed(this.leftArg)
pre	(soft) init'ed(this.rightArg)
pre	(soft) obj.op != null
pre	(soft) this.op != null
post	init'ed(return_value)
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on java.lang.String:valueOf

bool evaluate(bool[])

Kind	Annotation Text
pre	(soft) conditions != null
pre	(soft) conditions.length >= 1
pre	(soft) init'ed(com.dmdirc.actions.ConditionTree$1__ static_init.new int[](ConditionTree$1__static_init# 1)[...])
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 < conditions.length
pre	(soft) this.argument >= 0
pre	(soft) this.leftArg != null
pre	(soft) this.rightArg != null
pre	this.op != 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}

int getMaximumArgument()

Kind	Annotation Text
pre	(soft) init'ed(this...argument)
pre	(soft) init'ed(this.argument)
pre	(soft) this...leftArg != null
pre	(soft) this...rightArg != null
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

int hashCode()

Kind	Annotation Text
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)
pre	this.op != null
post	init'ed(return_value)
unanalyzed	call on com.dmdirc.actions.ConditionTree$OPERATION: ordinal
unanalyzed	call on java.lang.String:valueOf

bool isInt(char)

Kind	Annotation Text
post	init'ed(return_value)

ConditionTree parseStack(Deque)

Kind	Annotation Text
pre	stack != null
post	init'ed(new ConditionTree(readTerm#1) num objects)
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	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.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:size
unanalyzed	call on parseStack
unanalyzed	call on readTerm
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}

ConditionTree parseString(String)

Kind	Annotation Text
pre	string != null
post	init'ed(new ConditionTree(readTerm#1) num objects)
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	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.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:size
unanalyzed	call on parseStack
unanalyzed	call on readTerm
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}

ConditionTree readBracket(Deque)

Kind	Annotation Text
pre	(soft) stack != null
post	init'ed(new ConditionTree(readTerm#1) num objects)
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	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.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.util.ArrayDeque
unanalyzed	call on java.util.Deque:add
unanalyzed	call on java.util.Deque:addFirst
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:poll
unanalyzed	call on java.util.Deque:pollFirst
unanalyzed	call on java.util.Deque:pollLast
unanalyzed	call on java.util.Deque:size
unanalyzed	call on parseStack
unanalyzed	call on readTerm
test_vector	java.lang.Character:charValue(...)@329: {0..39, 41..2¹⁶-1}, {40}
test_vector	java.util.Deque:isEmpty(...)@326: {1}, {0}

ConditionTree readTerm(Deque)

Kind	Annotation Text
pre	stack != null
post	init'ed(new ConditionTree(readTerm#1).leftArg)
post	init'ed(return_value)
post	new ConditionTree(readTerm#1) num objects <= 1
post	new ConditionTree(readTerm#1).argument == -1
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.lang.Character:charValue
unanalyzed	call on java.lang.Character:instanceof
unanalyzed	call on java.util.Deque:isEmpty
unanalyzed	call on java.util.Deque:pollFirst
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}

String toString()

Kind	Annotation Text
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)
pre	this.op != null
presumption	com.dmdirc.actions.ConditionTree_OPERATION:ordinal( ...)@168 in {0..4}
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	java.lang.String:valueOf(...)._tainted == 0
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}

ConditionTree$OPERATION valueOf(String)

Kind	Annotation Text
post	init'ed(return_value)

ConditionTree$OPERATION[] values()

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