MediaSourceState.java

MediaSourceState.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

Kind	Annotation Text
post	init'ed(this.niceName)
post	this.niceName == niceName

Kind	Annotation Text
post	$VALUES == &new MediaSourceState[](MediaSourceS tate__static_init#6)
post	$VALUES.length == 5
post	$VALUES[0] == &new MediaSourceState(MediaSource State__static_init#1)
post	$VALUES[1] == &new MediaSourceState(MediaSource State__static_init#2)
post	$VALUES[2] == &new MediaSourceState(MediaSource State__static_init#3)
post	$VALUES[3] == &new MediaSourceState(MediaSource State__static_init#4)
post	$VALUES[4] == &new MediaSourceState(MediaSource State__static_init#5)
post	CLOSED == &new MediaSourceState(MediaSourceStat e__static_init#1)
post	CLOSED.niceName == &"Closed"
post	NOTKNOWN == &new MediaSourceState(MediaSourceSt ate__static_init#5)
post	NOTKNOWN.niceName == &"Unknown"
post	PAUSED == &new MediaSourceState(MediaSourceStat e__static_init#3)
post	PAUSED.niceName == &"Paused"
post	PLAYING == &new MediaSourceState(MediaSourceSta te__static_init#4)
post	PLAYING.niceName == &"Playing"
post	STOPPED == &new MediaSourceState(MediaSourceSta te__static_init#2)
post	STOPPED.niceName == &"Stopped"
post	new MediaSourceState(MediaSourceState__static_ init#1) num objects == 1
post	new MediaSourceState(MediaSourceState__static_ init#2) num objects == 1
post	new MediaSourceState(MediaSourceState__static_ init#3) num objects == 1
post	new MediaSourceState(MediaSourceState__static_ init#4) num objects == 1
post	new MediaSourceState(MediaSourceState__static_ init#5) num objects == 1
post	new MediaSourceState[](MediaSourceState__static_ init#6) num objects == 1
unanalyzed	call on java.lang.Enum

Kind	Annotation Text
post	init'ed(return_value)
post	return_value == this.niceName

Kind	Annotation Text
post	init'ed(return_value)

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