ReverseFileReader.java

ReverseFileReader.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	this.file != null
post	this.file == null

void com.dmdirc.addons.logging.ReverseFileReader(File)

Kind	Annotation Text
post	new RandomAccessFile(ReverseFileReader#1) num objects == 1
post	this.file == &new RandomAccessFile(ReverseFileR eader#1)
post	this.seekLength == 50
unanalyzed	call on java.io.RandomAccessFile:length
unanalyzed	call on java.io.RandomAccessFile:seek

void com.dmdirc.addons.logging.ReverseFileReader(String)

Kind	Annotation Text
post	new RandomAccessFile(ReverseFileReader#1) num objects == 1
post	this.file == &new RandomAccessFile(ReverseFileR eader#1)
post	this.seekLength == 50
unanalyzed	call on java.io.RandomAccessFile:length
unanalyzed	call on java.io.RandomAccessFile:seek

com.dmdirc.addons.logging.ReverseFileReader__static_init

Kind	Annotation Text

Stack getLines(int)

Kind	Annotation Text
pre	(soft) init'ed(this.seekLength)
pre	(soft) this.file != null
post	new Stack(getLines#1) num objects == 1
post	return_value == &new Stack(getLines#1)
unanalyzed	call on java.io.RandomAccessFile:getFilePointer
unanalyzed	call on java.io.RandomAccessFile:read
unanalyzed	call on java.io.RandomAccessFile:seek
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Byte:valueOf
unanalyzed	call on java.lang.String
unanalyzed	call on java.nio.charset.Charset:forName
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:add
unanalyzed	call on java.util.ArrayList:get
unanalyzed	call on java.util.ArrayList:size

String getLinesAsString(int)

Kind	Annotation Text
pre	(soft) init'ed(this.seekLength)
pre	(soft) this.file != null
post	java.lang.StringBuilder:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuilder:toStri ng(...)
unanalyzed	call on java.io.RandomAccessFile:getFilePointer
unanalyzed	call on java.io.RandomAccessFile:read
unanalyzed	call on java.io.RandomAccessFile:seek
unanalyzed	call on java.lang.Byte:byteValue
unanalyzed	call on java.lang.Byte:valueOf
unanalyzed	call on java.lang.String
unanalyzed	call on java.nio.charset.Charset:forName
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.ArrayList:add
unanalyzed	call on java.util.ArrayList:get
unanalyzed	call on java.util.ArrayList:size
test_vector	java.lang.StringBuilder:charAt(...)@245: {0..9, 11..2¹⁶-1}, {10}

String getNextLine()

Kind	Annotation Text
pre	init'ed(this.seekLength)
pre	this.file != null
presumption	java.io.RandomAccessFile:getFilePointer(...)@134 != 0
presumption	java.io.RandomAccessFile:getFilePointer(...)@145 - this.seekLength in {-2_147_483_903.. 2⁶⁴-1}
presumption	java.io.RandomAccessFile:getFilePointer(...)@145 >= -2³¹
presumption	java.util.ArrayList:get(...)@205 != null
presumption	java.util.ArrayList:size(...)@204 >= 1
presumption	java.util.ArrayList:size(...)@205 - java.util.ArrayList:size(...)@204 in {-6_442_450_943..0}
post	new String(getNextLine#4) num objects == 1
post	return_value == &new String(getNextLine#4)
test_vector	bytes[i]@162: {13}, {10}, {-128..9, 11,12, 14..255}
test_vector	java.io.RandomAccessFile:getFilePointer(...)@145 - this.seekLength: {1..2⁶⁴-1}, {-2_147_483_903..-1}

byte getSeekLength()

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

Kind	Annotation Text
pre	this.file != null

void setSeekLength(byte)

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