Messages

method	net.sourceforge.pebble.domain.Theme__static_init
post	init'ed(log)

info method not available -- call on Log org.apache.commons.logging. LogFactory:getLog(Class)

method	void net.sourceforge.pebble.domain.Theme(Blog, String, String)
post	this.blog == blog
post	init'ed(this.blog)
post	this.name == name
post	init'ed(this.name)
post	this.pathToLiveThemes == pathToLiveThemes
post	init'ed(this.pathToLiveThemes)

method	String getBackupThemeDirectory()
pre	this.blog != null
presumption	init'ed(java.io.File.separator)
post	return_value != null

info method not available -- call on String net.sourceforge.pebble.domain. Blog:getRoot()

method	File getPathToLiveTheme()
pre	init'ed(this.name)
pre	init'ed(this.pathToLiveThemes)
post	return_value == &new File(getPathToLiveTheme#1)
post	new File(getPathToLiveTheme#1) num objects == 1

method	void restore()
pre	log != null
pre	this.blog != null
pre	init'ed(this.name)
pre	init'ed(this.pathToLiveThemes)
unanalyzed	call on net.sourceforge.pebble.domain.Blog:getRoot
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdir
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:getName
unanalyzed	call on copy
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.FileInputStream:getChannel
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.FileOutputStream:getChannel
unanalyzed	call on java.nio.channels.FileChannel:size
unanalyzed	call on java.nio.channels.FileChannel:transferFrom
unanalyzed	call on java.nio.channels.FileChannel:close
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:deleteFile
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on java.io.File:renameTo
unanalyzed	call on org.apache.commons.logging.Log:info

method	void restore(String)
pre	log != null
pre	this.blog != null
pre	init'ed(this.name)
pre	init'ed(this.pathToLiveThemes)
presumption	java.io.File:listFiles(...)@105 != null
unanalyzed	call on net.sourceforge.pebble.domain.Blog:getRoot
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdir
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:getName
unanalyzed	call on copy
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.FileInputStream:getChannel
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.FileOutputStream:getChannel
unanalyzed	call on java.nio.channels.FileChannel:size
unanalyzed	call on java.nio.channels.FileChannel:transferFrom
unanalyzed	call on java.nio.channels.FileChannel:close
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:deleteFile
unanalyzed	call on java.io.File:renameTo
unanalyzed	call on org.apache.commons.logging.Log:info
test_vector	java.io.File:exists(...)@105: {0}, {1}
test_vector	java.io.File:listFiles(...).length@105: {1..+Inf}, {0}

info method not available -- call on void org.apache.commons.logging. Log:debug(Object)

method	void restoreToSpecifiedTheme(String)
pre	log != null
pre	this.blog != null
pre	init'ed(this.name)
pre	init'ed(this.pathToLiveThemes)
unanalyzed	call on net.sourceforge.pebble.domain.Blog:getRoot
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdir
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:getName
unanalyzed	call on copy
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.FileInputStream:getChannel
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.FileOutputStream:getChannel
unanalyzed	call on java.nio.channels.FileChannel:size
unanalyzed	call on java.nio.channels.FileChannel:transferFrom
unanalyzed	call on java.nio.channels.FileChannel:close
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:deleteFile
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on java.io.File:renameTo
unanalyzed	call on org.apache.commons.logging.Log:info

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

method	void backup()
pre	log != null
pre	this.blog != null
pre	init'ed(this.name)
pre	init'ed(this.pathToLiveThemes)
unanalyzed	call on net.sourceforge.pebble.domain.Blog:getRoot
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdir
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:getName
unanalyzed	call on copy
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.FileInputStream:getChannel
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.FileOutputStream:getChannel
unanalyzed	call on java.nio.channels.FileChannel:size
unanalyzed	call on java.nio.channels.FileChannel:transferFrom
unanalyzed	call on java.nio.channels.FileChannel:close
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on net.sourceforge.pebble.util. FileUtils:deleteFile
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on java.io.File:renameTo

method	void backup(String)
pre	log != null
pre	this.blog != null
pre	init'ed(this.pathToLiveThemes)
unanalyzed	call on net.sourceforge.pebble.domain.Blog:getRoot
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdir
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.io.File
unanalyzed	call on copy
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.FileInputStream:getChannel
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.FileOutputStream:getChannel
unanalyzed	call on java.nio.channels.FileChannel:size
unanalyzed	call on java.nio.channels.FileChannel:transferFrom
unanalyzed	call on java.nio.channels.FileChannel:close
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on org.apache.commons.logging.Log:error
test_vector	java.io.File:exists(...)@141: {0}, {1}

info method not available -- call on void org.apache.commons.logging. Log:debug(Object)

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

method	void copy(String)
pre	log != null
pre	this.blog != null
pre	init'ed(this.pathToLiveThemes)
unanalyzed	call on net.sourceforge.pebble.domain.Blog:getRoot
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdir
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.io.File
unanalyzed	call on copy
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.FileInputStream:getChannel
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.FileOutputStream:getChannel
unanalyzed	call on java.nio.channels.FileChannel:size
unanalyzed	call on java.nio.channels.FileChannel:transferFrom
unanalyzed	call on java.nio.channels.FileChannel:close
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on org.apache.commons.logging.Log:error
test_vector	java.io.File:exists(...)@159: {0}, {1}

info method not available -- call on void org.apache.commons.logging. Log:info(Object)

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

method	void copy(File, File)
pre	destination != null
pre	source != null
pre	(soft) log != null
presumption	files.length@177 <= 2³²-1
presumption	files[i]@177 != null
presumption	java.io.FileInputStream:getChannel(...)@184 != null
presumption	java.io.FileOutputStream:getChannel(...)@185 != null
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdir
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:getName
unanalyzed	call on java.io.File
unanalyzed	call on copy
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.FileInputStream:getChannel
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.FileOutputStream:getChannel
unanalyzed	call on java.nio.channels.FileChannel:size
unanalyzed	call on java.nio.channels.FileChannel:transferFrom
unanalyzed	call on java.nio.channels.FileChannel:close
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on org.apache.commons.logging.Log:error
test_vector	java.io.File:exists(...)@173: {1}, {0}
test_vector	java.io.File:isDirectory(...)@180: {0}, {1}
test_vector	java.io.File:listFiles(...)@177: Addr_Set{null}, Inverse{null}

info method not available -- call on void org.apache.commons.logging. Log:error(Object, Throwable)

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