method

com.dmdirc.addons.logging.ReverseFileReader__ static_init

method	void com.dmdirc.addons.logging.ReverseFileReader(S tring)
post	this.file == &new RandomAccessFile(ReverseFileR eader#1)
post	this.seekLength == 50
post	new RandomAccessFile(ReverseFileReader#1) num objects == 1
unanalyzed	call on java.io.RandomAccessFile:seek
unanalyzed	call on java.io.RandomAccessFile:length

method	void com.dmdirc.addons.logging.ReverseFileReader(F ile)
post	this.file == &new RandomAccessFile(ReverseFileR eader#1)
post	this.seekLength == 50
post	new RandomAccessFile(ReverseFileReader#1) num objects == 1
unanalyzed	call on java.io.RandomAccessFile:seek
unanalyzed	call on java.io.RandomAccessFile:length

method	void reset()
pre	this.file != null

method	byte getSeekLength()
pre	init'ed(this.seekLength)
post	return_value == this.seekLength
post	init'ed(return_value)

method	void setSeekLength(byte)
post	this.seekLength == newValue
post	init'ed(this.seekLength)

method	void close()
pre	this.file != null
post	this.file == null

method	String getNextLine()
pre	this.file != null
pre	init'ed(this.seekLength)
presumption	java.io.RandomAccessFile:getFilePointer(...)@134 != 0
presumption	java.io.RandomAccessFile:getFilePointer(...)@145 >= -231
presumption	java.io.RandomAccessFile:getFilePointer(...)@145 - this.seekLength in {-2_147_483_903.. 264-1}
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	return_value == &new String(getNextLine#4)
post	new String(getNextLine#4) num objects == 1
test_vector	bytes[i]@162: {13}, {10}, {-128..9, 11,12, 14..255}
test_vector	java.io.RandomAccessFile:getFilePointer(...)@145 - this.seekLength: {1..264-1}, {-2_147_483_903..-1}

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

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