Messages

method | net.sourceforge.pebble.domain.FileMetaData__ static_init

method | void net.sourceforge.pebble.domain. FileMetaData(FileManager, String)
presumption | java.lang.String:lastIndexOf(...)@74 <= 232-2
post | this.context == context
post | init'ed(this.context)
post | this.name != null
post | this.path != null
test_vector | absolutePath: Addr_Set{null}, Inverse{null}
test_vector | java.lang.String:endsWith(...)@65: {0}, {1}
test_vector | java.lang.String:equals(...)@61: {1}, {0}
test_vector | java.lang.String:equals(...)@61: {0}, {1}
test_vector | java.lang.String:indexOf(...)@69: {-231.. -1}, {0..232-1}
test_vector | java.lang.String:length(...)@71: {1.. 232-1}, {0}
test_vector | java.lang.String:startsWith(...)@81: {1}, {0}

method | String getName()
pre | init'ed(this.name)
post | return_value == this.name
post | init'ed(return_value)

method | void setName(String)
post | this.name == name
post | init'ed(this.name)

method | Date getLastModified()
pre | init'ed(this.lastModified)
post | return_value == this.lastModified
post | init'ed(return_value)

method | void setLastModified(Date)
post | this.lastModified == lastModified
post | init'ed(this.lastModified)

method | bool isDirectory()
pre | init'ed(this.directory)
post | return_value == this.directory
post | init'ed(return_value)

method | void setDirectory(bool)
post | this.directory == directory
post | init'ed(this.directory)

method | String getPath()
pre | init'ed(this.path)
post | return_value == this.path
post | init'ed(return_value)

method | String getAbsolutePath()
pre | init'ed(this.name)
pre | this.path != null
post | return_value != null
test_vector | java.lang.String:endsWith(...)@116: {1}, {0}

method | String getUrl()
pre | init'ed(this.type)
pre | (soft) init'ed(this.directory)
pre | (soft) init'ed(this.name)
pre | (soft) this.path != null
post | init'ed(return_value)
unanalyzed | call on java.lang.String:endsWith
unanalyzed | call on java.lang.String:valueOf
test_vector | this.directory: {0}, {1}
test_vector | this.type: Addr_Set{null}, Inverse{null}
test_vector | java.lang.String:endsWith(...)@134: {1}, {0}
test_vector | java.lang.String:equals(...)@126: {0}, {1}
test_vector | java.lang.String:equals(...)@128: {0}, {1}
test_vector | java.lang.String:equals(...)@130: {0}, {1}

method | bool isEditable()
pre | init'ed(this.directory)
pre | (soft) this.name != null
post | init'ed(return_value)
test_vector | this.directory: {0}, {1}
test_vector | java.lang.String:endsWith(...)@147: {1}, {0}
test_vector | java.lang.String:endsWith(...)@148: {1}, {0}
test_vector | java.lang.String:endsWith(...)@149: {1}, {0}
test_vector | java.lang.String:endsWith(...)@150: {1}, {0}
test_vector | java.lang.String:endsWith(...)@151: {1}, {0}
test_vector | java.lang.String:endsWith(...)@152: {1}, {0}
test_vector | java.lang.String:endsWith(...)@153: {1}, {0}
test_vector | java.lang.String:endsWith(...)@154: {1}, {0}

method | long getSize()
pre | init'ed(this.size)
post | return_value == this.size
post | init'ed(return_value)

method | double getSizeInKB()
pre | init'ed(this.size)
post | return_value == (float) (this.size)/1024
post | return_value in (-Inf..+Inf)

method | void setSize(long)
post | this.size == size
post | init'ed(this.size)

method | void setType(String)
post | this.type == type
post | init'ed(this.type)

method | File getFile()
pre | this.context != null
pre | init'ed(this.context.root)
pre | init'ed(this.name)
pre | this.path != null
post | return_value == &new File(getFile#1*)
post | new File(getFile#1*) num objects == 1
unanalyzed | call on java.lang.String:endsWith
unanalyzed | call on java.lang.String:valueOf
unanalyzed | call on java.lang.String:startsWith
unanalyzed | call on java.lang.String:substring
unanalyzed | call on java.io.File