filemetadata.java

filemetadata.java

current inspection = 2010-07-22 15:04:21 (id #4)

base = 2010-07-16 16:14:15 (id #1)

Filter Options

History:

+	added
-	dropped
U	unchanged

Annotation Kind:

pre

presumption

post

unanalyzed

test

String getAbsolutePath()

-/+	Kind	Annotation Text	Date
U	pre	init'ed(this.name)	2010-07-16 16:14:15
U	pre	this.path != null	2010-07-16 16:14:15
U	post	return_value != null	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@116: {1}, {0}	2010-07-16 16:14:15

-/+	Kind	Annotation Text	Date
U	pre	init'ed(this.context.root)	2010-07-16 16:14:15
U	pre	init'ed(this.name)	2010-07-16 16:14:15
U	pre	this.context != null	2010-07-16 16:14:15
U	pre	this.path != null	2010-07-16 16:14:15
U	post	new File(getFile#1*) num objects == 1	2010-07-16 16:14:15
U	post	return_value == &new File(getFile#1*)	2010-07-16 16:14:15
U	unanalyzed	call on java.io.File	2010-07-16 16:14:15
U	unanalyzed	call on java.lang.String:endsWith	2010-07-16 16:14:15
U	unanalyzed	call on java.lang.String:startsWith	2010-07-16 16:14:15
U	unanalyzed	call on java.lang.String:substring	2010-07-16 16:14:15
U	unanalyzed	call on java.lang.String:valueOf	2010-07-16 16:14:15

Date getLastModified()

-/+	Kind	Annotation Text	Date
U	pre	init'ed(this.lastModified)	2010-07-16 16:14:15
U	post	init'ed(return_value)	2010-07-16 16:14:15
U	post	return_value == this.lastModified	2010-07-16 16:14:15

String getName()

-/+	Kind	Annotation Text	Date
U	pre	init'ed(this.name)	2010-07-16 16:14:15
U	post	init'ed(return_value)	2010-07-16 16:14:15
U	post	return_value == this.name	2010-07-16 16:14:15

String getPath()

-/+	Kind	Annotation Text	Date
U	pre	init'ed(this.path)	2010-07-16 16:14:15
U	post	init'ed(return_value)	2010-07-16 16:14:15
U	post	return_value == this.path	2010-07-16 16:14:15

-/+	Kind	Annotation Text	Date
U	pre	init'ed(this.size)	2010-07-16 16:14:15
U	post	init'ed(return_value)	2010-07-16 16:14:15
U	post	return_value == this.size	2010-07-16 16:14:15

double getSizeInKB()

-/+	Kind	Annotation Text	Date
U	pre	init'ed(this.size)	2010-07-16 16:14:15
U	post	return_value == (float) (this.size)/1024	2010-07-16 16:14:15
U	post	return_value in (-Inf..+Inf)	2010-07-16 16:14:15

String getUrl()

-/+	Kind	Annotation Text	Date
U	pre	(soft) init'ed(this.directory)	2010-07-16 16:14:15
U	pre	(soft) init'ed(this.name)	2010-07-16 16:14:15
U	pre	(soft) this.path != null	2010-07-16 16:14:15
U	pre	init'ed(this.type)	2010-07-16 16:14:15
U	post	init'ed(return_value)	2010-07-16 16:14:15
U	unanalyzed	call on java.lang.String:endsWith	2010-07-16 16:14:15
U	unanalyzed	call on java.lang.String:valueOf	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@134: {1}, {0}	2010-07-16 16:14:15
U	test_vector	java.lang.String:equals(...)@126: {0}, {1}	2010-07-16 16:14:15
U	test_vector	java.lang.String:equals(...)@128: {0}, {1}	2010-07-16 16:14:15
U	test_vector	java.lang.String:equals(...)@130: {0}, {1}	2010-07-16 16:14:15
U	test_vector	this.directory: {0}, {1}	2010-07-16 16:14:15
U	test_vector	this.type: Addr_Set{null}, Inverse{null}	2010-07-16 16:14:15

bool isDirectory()

-/+	Kind	Annotation Text	Date
U	pre	init'ed(this.directory)	2010-07-16 16:14:15
U	post	init'ed(return_value)	2010-07-16 16:14:15
U	post	return_value == this.directory	2010-07-16 16:14:15

bool isEditable()

-/+	Kind	Annotation Text	Date
U	pre	(soft) this.name != null	2010-07-16 16:14:15
U	pre	init'ed(this.directory)	2010-07-16 16:14:15
U	post	init'ed(return_value)	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@147: {1}, {0}	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@148: {1}, {0}	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@149: {1}, {0}	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@150: {1}, {0}	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@151: {1}, {0}	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@152: {1}, {0}	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@153: {1}, {0}	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@154: {1}, {0}	2010-07-16 16:14:15
U	test_vector	this.directory: {0}, {1}	2010-07-16 16:14:15

void net.sourceforge.pebble.domain.FileMetaData(FileManager, String)

-/+	Kind	Annotation Text	Date
U	presumption	java.lang.String:lastIndexOf(...)@74 <= 2³²-2	2010-07-16 16:14:15
U	post	init'ed(this.context)	2010-07-16 16:14:15
U	post	this.context == context	2010-07-16 16:14:15
U	post	this.name != null	2010-07-16 16:14:15
U	post	this.path != null	2010-07-16 16:14:15
U	test_vector	absolutePath: Addr_Set{null}, Inverse{null}	2010-07-16 16:14:15
U	test_vector	java.lang.String:endsWith(...)@65: {0}, {1}	2010-07-16 16:14:15
U	test_vector	java.lang.String:equals(...)@61: {0}, {1}	2010-07-16 16:14:15
U	test_vector	java.lang.String:equals(...)@61: {1}, {0}	2010-07-16 16:14:15
U	test_vector	java.lang.String:indexOf(...)@69: {-2³¹.. -1}, {0..2³²-1}	2010-07-16 16:14:15
U	test_vector	java.lang.String:length(...)@71: {1.. 2³²-1}, {0}	2010-07-16 16:14:15
U	test_vector	java.lang.String:startsWith(...)@81: {1}, {0}	2010-07-16 16:14:15

net.sourceforge.pebble.domain.FileMetaData__static_init

-/+	Kind	Annotation Text	Date

void setDirectory(bool)

-/+	Kind	Annotation Text	Date
U	post	init'ed(this.directory)	2010-07-16 16:14:15
U	post	this.directory == directory	2010-07-16 16:14:15

void setLastModified(Date)

-/+	Kind	Annotation Text	Date
U	post	init'ed(this.lastModified)	2010-07-16 16:14:15
U	post	this.lastModified == lastModified	2010-07-16 16:14:15

void setName(String)

-/+	Kind	Annotation Text	Date
U	post	init'ed(this.name)	2010-07-16 16:14:15
U	post	this.name == name	2010-07-16 16:14:15

void setSize(long)

-/+	Kind	Annotation Text	Date
U	post	init'ed(this.size)	2010-07-16 16:14:15
U	post	this.size == size	2010-07-16 16:14:15

void setType(String)

-/+	Kind	Annotation Text	Date
U	post	init'ed(this.type)	2010-07-16 16:14:15
U	post	this.type == type	2010-07-16 16:14:15