Messages

method

net.sourceforge.pebble.domain.FileManager__static_ init

method	void net.sourceforge.pebble.domain. FileManager(Blog, String)
pre	blog != null
pre	type != null
post	this.root in Addr_Set{&new File(FileManager#3), &new File(FileManager#2),&new File(getPathToLiveTheme#1),&new File(FileManager#1)}
post	this.type == type
post	this.type != null
post	new File(FileManager#1) num objects <= 1
post	new File(FileManager#2) num objects <= 1
post	new File(FileManager#3) num objects <= 1
post	new File(getPathToLiveTheme#1) num objects <= 1
unanalyzed	call on java.io.File
test_vector	java.lang.String:equals(...)@70: {0}, {1}
test_vector	java.lang.String:equals(...)@72: {0}, {1}
test_vector	java.lang.String:equals(...)@74: {0}, {1}
pre	(soft) blog.editableTheme != null
pre	(soft) init'ed(blog.editableTheme.name)
pre	(soft) init'ed(blog.editableTheme.pathToLiveThemes)
pre	(soft) init'ed(blog.root)
unanalyzed	call on java.lang.String:valueOf

method	File getRootDirectory()
pre	init'ed(this.root)
post	return_value == this.root
post	init'ed(return_value)

method	FileMetaData getFileMetaData(String)
pre	init'ed(this.type)
pre	(soft) init'ed(this.root)
presumption	java.util.Iterator:next(...)@110 != null
post	return_value == &new FileMetaData(getFileMetaDa ta#1)
post	new Date(getFileMetaData#2) num objects <= 1
post	new FileMetaData(getFileMetaData#1) num objects == 1
post	return_value.context == this
post	return_value.context != null
post	init'ed(return_value.directory)
post	init'ed(return_value.lastModified)
post	return_value.name != null
post	return_value.path != null
post	init'ed(return_value.size)
post	return_value.type == this.type
post	init'ed(return_value.type)
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith
test_vector	java.io.File:exists(...)@102: {0}, {1}
test_vector	java.io.File:isDirectory(...)@103: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@109: {1}, {0}

method	FileMetaData getParent(FileMetaData)
pre	file != null
pre	init'ed(file.name)
pre	file.path != null
pre	(soft) init'ed(this.root)
pre	(soft) init'ed(this.type)
post	return_value in Addr_Set{null,&new FileMetaData(getFileMetaData#1)}
post	new Date(getFileMetaData#2) num objects <= 1
post	new FileMetaData(getFileMetaData#1) num objects <= 1
post	new FileMetaData(getFileMetaData#1).context == this
post	new FileMetaData(getFileMetaData#1).context != null
post	init'ed(new FileMetaData(getFileMetaData#1). directory)
post	init'ed(new FileMetaData(getFileMetaData#1). lastModified)
post	new FileMetaData(getFileMetaData#1).name != null
post	new FileMetaData(getFileMetaData#1).path != null
post	init'ed(new FileMetaData(getFileMetaData#1).size)
post	new FileMetaData(getFileMetaData#1).type == this.type
post	(soft) init'ed(new FileMetaData(getFileMetaData#1). type)
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith
test_vector	java.lang.String:equals(...)@127: {0}, {1}

method	FileMetaData getFileMetaData(String, String)
pre	init'ed(this.type)
pre	(soft) init'ed(this.root)
post	return_value == &new FileMetaData(getFileMetaDa ta#1*)
post	new Date(getFileMetaData#2*) num objects <= 1
post	new FileMetaData(getFileMetaData#1*) num objects == 1
post	new FileMetaData(getFileMetaData#1*).context != null
post	init'ed(new FileMetaData(getFileMetaData#1*). directory)
post	init'ed(new FileMetaData(getFileMetaData#1*). lastModified)
post	new FileMetaData(getFileMetaData#1*).name != null
post	new FileMetaData(getFileMetaData#1*).path != null
post	init'ed(new FileMetaData(getFileMetaData#1*).size)
post	init'ed(new FileMetaData(getFileMetaData#1*).type)
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith
test_vector	path: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:endsWith(...)@142: {0}, {1}

method	File getFile(String)
pre	init'ed(this.root)
post	return_value == &new File(getFile#1)
post	new File(getFile#1) num objects == 1
test_vector	path: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:startsWith(...)@158: {0}, {1}

method	File getFile(FileMetaData)
pre	file != null
pre	init'ed(file.name)
pre	file.path != null
pre	init'ed(this.root)
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

method	bool isUnderneathRootDirectory(File)
pre	init'ed(this.root)
post	init'ed(return_value)

info method not available -- call on bool net.sourceforge.pebble.util. FileUtils:underneathRoot(File, File)

method	File createDirectory(String, String)
pre	init'ed(this.type)
pre	(soft) init'ed(this.root)
presumption	net.sourceforge.pebble.util.FileUtils:underneathRoo t(...)@187 == 1
post	return_value == &new File(createDirectory#1)
post	new File(createDirectory#1) num objects == 1
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith

method	File copyFile(String, String, String)
pre	(soft) init'ed(this.root)
pre	(soft) init'ed(this.type)
presumption	net.sourceforge.pebble.util.FileUtils:underneathRoo t(...)@187 == 1
post	return_value in Addr_Set{null,&new File(copyFile#2)}
post	new File(copyFile#2) num objects <= 1
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith
test_vector	newName: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:equals(...)@221: {1}, {0}
test_vector	java.lang.String:length(...)@221: {0}, {1..2³²-1}

info method not available -- call on void net.sourceforge.pebble.util. FileUtils:copyFile(File, File)

method	File renameFile(String, String, String)
pre	(soft) init'ed(this.root)
pre	(soft) init'ed(this.type)
presumption	net.sourceforge.pebble.util.FileUtils:underneathRoo t(...)@187 == 1
post	return_value in Addr_Set{null,&new File(renameFile#2)}
post	new File(renameFile#2) num objects <= 1
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith
test_vector	newName: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:equals(...)@249: {1}, {0}
test_vector	java.lang.String:length(...)@249: {0}, {1..2³²-1}

method	void deleteFile(String, String)
pre	init'ed(this.root)
pre	init'ed(this.type)
presumption	net.sourceforge.pebble.util.FileUtils:underneathRoo t(...)@187 == 1
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith

info method not available -- call on void net.sourceforge.pebble.util. FileUtils:deleteFile(File)

method	String loadFile(String, String)
pre	init'ed(this.root)
pre	init'ed(this.type)
presumption	net.sourceforge.pebble.util.FileUtils:underneathRoo t(...)@187 == 1
post	return_value != null
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith
test_vector	java.io.BufferedReader:readLine(...)@306: Addr_Set{null}, Inverse{null}

method	void saveFile(String, String, String)
pre	init'ed(this.type)
pre	(soft) init'ed(this.root)
presumption	net.sourceforge.pebble.util.FileUtils:underneathRoo t(...)@187 == 1
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith

method	FileMetaData saveFile(String, byte[])
pre	init'ed(this.root)
pre	init'ed(this.type)
presumption	net.sourceforge.pebble.util.FileUtils:underneathRoo t(...)@187 == 1
post	return_value == &new FileMetaData(getFileMetaDa ta#1)
post	new Date(getFileMetaData#2) num objects <= 1
post	new FileMetaData(getFileMetaData#1) num objects == 1
post	return_value.context == this
post	return_value.context != null
post	init'ed(return_value.directory)
post	init'ed(return_value.lastModified)
post	return_value.name != null
post	return_value.path != null
post	init'ed(return_value.size)
post	return_value.type == this.type
post	init'ed(return_value.type)
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf

method	List getFiles(String)
pre	init'ed(this.type)
pre	(soft) init'ed(this.root)
post	return_value == &new ArrayList(getFiles#1*)
post	new ArrayList(getFiles#1*) num objects == 1
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith

method	List getFiles(String, bool)
pre	init'ed(this.type)
pre	(soft) init'ed(this.root)
post	return_value == &new ArrayList(getFiles#1*)
post	new ArrayList(getFiles#1*) num objects == 1
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith

method	List getFiles(FileMetaData, bool)
pre	init'ed(this.root)
pre	(soft) path != null
pre	(soft) init'ed(path.name)
pre	(soft) path.path != null
pre	(soft) init'ed(this.type)
presumption	f.length@389 <= 2³²-1
presumption	f[i]@389 != null
presumption	net.sourceforge.pebble.util.FileUtils:underneathRoo t(...)@187 == 1
post	return_value == &new ArrayList(getFiles#1)
post	new ArrayList(getFiles#1) num objects == 1
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith
test_vector	includeChildren: {0}, {1}
test_vector	java.io.File:isDirectory(...)@394: {0}, {1}
test_vector	java.io.File:isFile(...)@408: {0}, {1}
test_vector	java.io.File:listFiles(...)@389: Addr_Set{null}, Inverse{null}

method	double getCurrentUsage(Blog)
pre	blog != null
post	return_value in (-Inf..+Inf)
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
pre	(soft) blog.editableTheme != null
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
pre	(soft) init'ed(blog.editableTheme.name)
unanalyzed	call on java.util.Date
pre	(soft) init'ed(blog.editableTheme.pathToLiveThemes)
unanalyzed	call on setLastModified
pre	(soft) init'ed(blog.root)
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:startsWith

method	bool hasEnoughSpace(Blog, double)
pre	(soft) blog != null
post	init'ed(return_value)
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:underneathRoot
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File
unanalyzed	call on getFileMetaData
unanalyzed	call on getFiles
unanalyzed	call on getFile
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on getAbsolutePath
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:addAll
unanalyzed	call on net.sourceforge.pebble.comparator. FileMetaDataComparator
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.io.File:isFile
unanalyzed	call on net.sourceforge.pebble.domain.FileMetaData
unanalyzed	call on setType
unanalyzed	call on java.io.File:exists
unanalyzed	call on setDirectory
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getSize
unanalyzed	call on setSize
unanalyzed	call on java.io.File:length
unanalyzed	call on java.io.File:lastModified
unanalyzed	call on java.util.Date
unanalyzed	call on setLastModified
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
pre	(soft) blog.editableTheme != null
pre	(soft) init'ed(blog.editableTheme.name)
pre	(soft) init'ed(blog.editableTheme.pathToLiveThemes)
unanalyzed	call on getSizeInKB
unanalyzed	call on java.lang.String:length
pre	(soft) init'ed(blog.root)
unanalyzed	call on java.lang.String:indexOf
presumption	net.sourceforge.pebble.PebbleContext:getConfigurati on(...)@447 != null
unanalyzed	call on java.lang.String:lastIndexOf
presumption	net.sourceforge.pebble.PebbleContext:getInstance(.. .)@447 != null
unanalyzed	call on java.lang.String:startsWith
test_vector	net.sourceforge.pebble.PebbleContext:getConfigurati on(...).fileUploadQuota@447: {-1}, {-9_223_372_036_ 854_775_808..-2, 0..2⁶⁴-1}

info method not available -- call on PebbleContext net.sourceforge.pebble. PebbleContext:getInstance()

info method not available -- call on Configuration net.sourceforge.pebble. PebbleContext:getConfiguration()

	info	method not available	-- call on PebbleContext net.sourceforge.pebble. PebbleContext:getInstance()
	info	method not available	-- call on Configuration net.sourceforge.pebble. PebbleContext:getConfiguration()