Messages

Last Msg First Msg

method

org.apache.roller.weblogger.business. FileManagerImpl$1__static_init

method

org.apache.roller.weblogger.business. FileManagerImpl$WeblogResourceFile$1__static_init

method

org.apache.roller.weblogger.business. FileManagerImpl$WeblogResourceFile__static_init

method	org.apache.roller.weblogger.business. FileManagerImpl__static_init
post	init'ed(log)

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

method	void org.apache.roller.weblogger.business. FileManagerImpl()
pre	org/apache/roller/weblogger/config/WebloggerConfig. config != null
pre	org/apache/roller/weblogger/config/WebloggerConfig. log != null
presumption	init'ed(java.io.File.separator)
presumption	init'ed(java.io.File.separatorChar)
post	this.upload_dir != null
unanalyzed	call on java.lang.String:trim
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on java.util.Properties:getProperty
test_vector	java.lang.String:endsWith(...)@62: {1}, {0}
test_vector	java.lang.String:length(...)@59: {1.. 2³²-1}, {0}

method	ThemeResource getFile(Weblog, String)
pre	init'ed(this.upload_dir)
pre	weblog != null
presumption	java.io.File:isDirectory(...)@79 == 0
post	return_value == &new FileManagerImpl$WeblogReso urceFile(getFile#3)
post	new File(getRealFile#6) num objects == 1
post	new FileManagerImpl$WeblogResourceFile(getFile#3) num objects == 1
post	new FileManagerImpl$WeblogResourceFile(getFile#3). relativePath == path
post	init'ed(new FileManagerImpl$WeblogResourceFile(getF ile#3).relativePath)
post	new FileManagerImpl$WeblogResourceFile(getFile#3). resourceFile == &new File(getRealFile#6)
post	new FileManagerImpl$WeblogResourceFile(getFile#3). weblog == weblog
post	new FileManagerImpl$WeblogResourceFile(getFile#3). weblog != null
unanalyzed	call on java.lang.String:replace
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:getCanonicalPath
unanalyzed	call on java.lang.Throwable:__curr_excep_obj

method	ThemeResource[] getFiles(Weblog, String)
pre	init'ed(this.upload_dir)
pre	weblog != null
presumption	java.io.File:isDirectory(...)@99 == 1
post	init'ed(return_value)
unanalyzed	call on java.lang.String:replace
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:getCanonicalPath
unanalyzed	call on java.lang.Throwable:__curr_excep_obj

info method not available -- call on ThemeResource[] org.apache.roller. weblogger.pojos.ThemeResource:getChildren()

method	ThemeResource[] getDirectories(Weblog)
pre	init'ed(this.upload_dir)
pre	weblog != null
presumption	dirFiles.length@121 <= 2³²-1
presumption	java.io.File:listFiles(...)@121 != null
post	return_value == &new ThemeResource[](getDirecto ries#2)
post	(soft) new FileManagerImpl$WeblogResourceFile(getDi rectories#3) num objects <= 2³²-1
post	init'ed(new FileManagerImpl$WeblogResourceFile(getD irectories#3).relativePath)
post	new FileManagerImpl$WeblogResourceFile(getDirectori es#3).resourceFile == null
post	new FileManagerImpl$WeblogResourceFile(getDirectori es#3).weblog == weblog
post	new FileManagerImpl$WeblogResourceFile(getDirectori es#3).weblog != null
post	new ThemeResource[](getDirectories#2) num objects == 1
post	(soft) return_value.length <= 2³²-1
post	possibly_updated(return_value[...])
post	(soft) new FileManagerImpl$WeblogResourceFile(getDi rectories#3) num objects == dirFiles.length@121
unanalyzed	call on java.lang.String:replace
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:getCanonicalPath
unanalyzed	call on java.lang.Throwable:__curr_excep_obj

method

void org.apache.roller.weblogger.business. FileManagerImpl$1(FileManagerImpl)

method	bool accept(File)
post	init'ed(return_value)

Prev Msg Next Msg

+

click for all messages in this file medium

null dereference check might fail: requires not_init'ed(dirFiles[i])

Prev Msg Next Msg

method	void saveFile(Weblog, String, String, long, InputStream)
pre	is != null
pre	log != null
pre	path != null
pre	init'ed(this.upload_dir)
pre	weblog != null
pre	(soft) org/apache/roller/weblogger/business/Weblogg erFactory.webloggerProvider != null
pre	(soft) org/apache/roller/weblogger/business/Weblogg erFactory.webloggerProvider.webloggerInstance != null
pre	(soft) org/apache/roller/weblogger/config/Weblogger RuntimeConfig.log != null
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:replace
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:getCanonicalPath
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:length
unanalyzed	call on getDirSize
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on getBooleanProperty
unanalyzed	call on org.apache.roller.weblogger.util. RollerMessages:addError
unanalyzed	call on getProperty
unanalyzed	call on java.math.BigDecimal
unanalyzed	call on java.math.BigDecimal:doubleValue
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on java.math.BigDecimal:toString
unanalyzed	call on org.apache.commons.lang.StringUtils:deleteW hitespace
unanalyzed	call on org.apache.commons.lang.StringUtils:split
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on java.io.File:mkdir
unanalyzed	call on org.apache.roller.weblogger.util. RollerMessages
unanalyzed	call on org.apache.roller.weblogger.util. RollerMessages:toString
unanalyzed	call on java.io.FileOutputStream
unanalyzed	call on java.io.InputStream:read
unanalyzed	call on java.io.OutputStream:write
unanalyzed	call on java.io.OutputStream:flush
unanalyzed	call on java.io.OutputStream:close
unanalyzed	call on getWeblogger
unanalyzed	call on getPropertiesManager
unanalyzed	call on java.lang.ThreadLocal:get
unanalyzed	call on javax.persistence.EntityManagerFactory:crea teEntityManager
unanalyzed	call on java.lang.ThreadLocal:set
unanalyzed	call on javax.persistence.EntityManager:getTransact ion
unanalyzed	call on javax.persistence.EntityTransaction:isActiv e
unanalyzed	call on javax.persistence.EntityTransaction:begin
unanalyzed	call on javax.persistence.EntityManager:find
unanalyzed	call on org.apache.roller.weblogger.pojos. RuntimeConfigProperty:getValue
unanalyzed	call on org.apache.commons.logging.Log:warn
unanalyzed	call on java.lang.Boolean
unanalyzed	call on java.lang.Boolean:booleanValue

method	void saveFile(Weblog, String, String, long, InputStream, bool)
pre	is != null
pre	log != null
pre	path != null
pre	init'ed(this.upload_dir)
pre	weblog != null
pre	(soft) contentType init'ed
pre	(soft) org/apache/roller/weblogger/business/Weblogg erFactory.webloggerProvider != null
pre	(soft) org/apache/roller/weblogger/business/Weblogg erFactory.webloggerProvider.webloggerInstance != null
pre	(soft) org/apache/roller/weblogger/config/Weblogger RuntimeConfig.log != null
presumption	(int) (java.math.BigDecimal:doubleValue(... )@366*1024000) in range
presumption	(int) (java.math.BigDecimal:doubleValue(... )@366*1024000) - size in range
presumption	size <= (int) (java.math.BigDecimal:doubleValue(... )@366*1024000) \| canSave(...) == 0
presumption	(size + canSave(...)) - (int) (java.math. BigDecimal:doubleValue(...)@377*1024000) in range
presumption	true
presumption	init'ed(java.io.File.separator)
presumption	java.lang.String:indexOf(...)@456 in range
presumption	(int) (java.math.BigDecimal:doubleValue(... )@3661024000) < size \| canSave(...) == 0 \| size + canSave(...) <= (int) (java.math.BigDecimal:double Value(...)@3771024000)
presumption	(int) (java.math.BigDecimal:doubleValue(... )@3661024000) < size \| canSave(...) == 0 \| (int) (java.math.BigDecimal:doubleValue(... )@3771024000) < size + canSave(...) \| checkFileType(...) == 0 \| java.lang. String:indexOf(...)@402 == -1 \| java.lang....
presumption	(int) (java.math.BigDecimal:doubleValue(... )@3661024000) < size \| canSave(...) == 0 \| (int) (java.math.BigDecimal:doubleValue(... )@3771024000) < size + canSave(...) \| checkFileType(...) != 0
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:replace
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:getCanonicalPath
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:length
unanalyzed	call on getDirSize
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on getBooleanProperty
unanalyzed	call on org.apache.roller.weblogger.util. RollerMessages:addError
unanalyzed	call on getProperty
unanalyzed	call on java.math.BigDecimal
unanalyzed	call on java.math.BigDecimal:doubleValue
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on java.math.BigDecimal:toString
unanalyzed	call on org.apache.commons.lang.StringUtils:deleteW hitespace
unanalyzed	call on org.apache.commons.lang.StringUtils:split
unanalyzed	call on java.lang.RuntimeException
unanalyzed	call on getWeblogger
unanalyzed	call on getPropertiesManager
unanalyzed	call on java.lang.ThreadLocal:get
unanalyzed	call on javax.persistence.EntityManagerFactory:crea teEntityManager
unanalyzed	call on java.lang.ThreadLocal:set
unanalyzed	call on javax.persistence.EntityManager:getTransact ion
unanalyzed	call on javax.persistence.EntityTransaction:isActiv e
unanalyzed	call on javax.persistence.EntityTransaction:begin
unanalyzed	call on javax.persistence.EntityManager:find
unanalyzed	call on org.apache.roller.weblogger.pojos. RuntimeConfigProperty:getValue
unanalyzed	call on org.apache.commons.logging.Log:warn
unanalyzed	call on java.lang.Boolean
unanalyzed	call on java.lang.Boolean:booleanValue
test_vector	checkCanSave: {0}, {1}
test_vector	java.io.File:exists(...)@180: {1}, {0}
test_vector	java.io.InputStream:read(...)@195: {-1}, {-2³¹..-2, 0..2³²-1}
test_vector	java.lang.String:indexOf(...)@177: {-1}, {-2³¹..-2, 0..2³²-1}
test_vector	java.lang.String:startsWith(...)@163: {0}, {1}

info method not available -- call on void org.apache.roller.weblogger.util. RollerMessages()

Prev Msg Next Msg

+

click for all messages in this file medium

conditional throw check might fail: requires canSave(...) != 0

Prev Msg Next Msg

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

method	void createDirectory(Weblog, String)
pre	path != null
pre	init'ed(this.upload_dir)
pre	weblog != null
presumption	init'ed(java.io.File.separator)
presumption	java.io.File:getCanonicalPath(...)@243 != null
presumption	java.io.File:mkdir(...)@253 == 1
presumption	java.lang.String:indexOf(...)@227 == -1
presumption	java.lang.String:startsWith(...)@243 == 1
unanalyzed	call on java.lang.String:replace
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:getCanonicalPath
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
test_vector	java.io.File:canRead(...)@236: {0}, {1}
test_vector	java.io.File:exists(...)@236: {0}, {1}
test_vector	java.io.File:isDirectory(...)@236: {0}, {1}
test_vector	java.lang.String:startsWith(...)@223: {0}, {1}

Prev Msg Next Msg

+

click for all messages in this file warning

test always goes same way test predetermined because savePath != null

Prev Msg Next Msg

method	void deleteFile(Weblog, String)
pre	init'ed(this.upload_dir)
pre	weblog != null
presumption	java.io.File:delete(...)@270 == 1
unanalyzed	call on java.lang.String:replace
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:getCanonicalPath
unanalyzed	call on java.lang.Throwable:__curr_excep_obj

method	void deleteAllFiles(Weblog)
pre	(soft) init'ed(this.upload_dir)
pre	(soft) weblog != null
unanalyzed	call on java.lang.String:replace
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:getCanonicalPath
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on deleteAllFiles
unanalyzed	call on java.io.File:delete

method	void deleteAllFiles(File)
pre	dir != null
presumption	dirFiles.length@302 <= 2³²-1
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on deleteAllFiles
unanalyzed	call on java.io.File:delete
test_vector	dirFiles.length@302: {0}, {1..2³²-1}
test_vector	java.io.File:isDirectory(...)@305: {0}, {1}
test_vector	java.io.File:listFiles(...)@302: Addr_Set{null}, Inverse{null}

Prev Msg Next Msg

+

click for all messages in this file high

null dereference check fails here: requires file != null

Prev Msg Next Msg

method	bool overQuota(Weblog)
pre	org/apache/roller/weblogger/config/WebloggerRuntime Config.log != null
pre	init'ed(this.upload_dir)
pre	weblog != null
pre	(soft) org/apache/roller/weblogger/business/Weblogg erFactory.webloggerProvider != null
pre	(soft) org/apache/roller/weblogger/business/Weblogg erFactory.webloggerProvider.webloggerInstance != null
presumption	(int) (java.math.BigDecimal:doubleValue(... )@329*1024000) in -2⁶³.. 2⁶⁴-1
post	init'ed(return_value)
unanalyzed	call on java.lang.String:replace
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:getCanonicalPath
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:length
unanalyzed	call on getDirSize
unanalyzed	call on getWeblogger
unanalyzed	call on getPropertiesManager
unanalyzed	call on getProperty
unanalyzed	call on java.lang.ThreadLocal:get
unanalyzed	call on javax.persistence.EntityManagerFactory:crea teEntityManager
unanalyzed	call on java.lang.ThreadLocal:set
unanalyzed	call on javax.persistence.EntityManager:getTransact ion
unanalyzed	call on javax.persistence.EntityTransaction:isActiv e
unanalyzed	call on javax.persistence.EntityTransaction:begin
unanalyzed	call on javax.persistence.EntityManager:find
unanalyzed	call on org.apache.roller.weblogger.pojos. RuntimeConfigProperty:getValue
unanalyzed	call on org.apache.commons.logging.Log:warn
unanalyzed	call on org.apache.commons.logging.Log:debug

Prev Msg Next Msg

+

click for all messages in this file warning

unused assignment unused assignment into maxFileSize

Prev Msg Next Msg

method

void release()

method	bool canSave(Weblog, String, String, long, RollerMessages)
pre	org/apache/roller/weblogger/config/WebloggerRuntime Config.log != null
pre	(soft) log != null
pre	(soft) messages != null
pre	(soft) org/apache/roller/weblogger/business/Weblogg erFactory.webloggerProvider != null
pre	(soft) org/apache/roller/weblogger/business/Weblogg erFactory.webloggerProvider.webloggerInstance != null
pre	(soft) path != null
pre	(soft) init'ed(this.upload_dir)
pre	(soft) weblog != null
presumption	(int) (java.math.BigDecimal:doubleValue(... )@366*1024000) in -2³¹..2³²-1
presumption	(int) (java.math.BigDecimal:doubleValue(... )@377*1024000) in -2⁶³.. 2⁶⁴-1
presumption	allowFiles.length@394 <= 2³²-1
presumption	forbidFiles.length@395 <= 2³²-1
post	init'ed(return_value)
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:replace
unanalyzed	call on org.apache.roller.weblogger.pojos. Weblog:getHandle
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:mkdirs
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.lang.String:lastIndexOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
unanalyzed	call on java.io.File:getAbsolutePath
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:getCanonicalPath
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:length
unanalyzed	call on getDirSize
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on getWeblogger
unanalyzed	call on getPropertiesManager
unanalyzed	call on getProperty
unanalyzed	call on java.lang.ThreadLocal:get
unanalyzed	call on javax.persistence.EntityManagerFactory:crea teEntityManager
unanalyzed	call on java.lang.ThreadLocal:set
unanalyzed	call on javax.persistence.EntityManager:getTransact ion
unanalyzed	call on javax.persistence.EntityTransaction:isActiv e
unanalyzed	call on javax.persistence.EntityTransaction:begin
unanalyzed	call on javax.persistence.EntityManager:find
unanalyzed	call on org.apache.roller.weblogger.pojos. RuntimeConfigProperty:getValue
unanalyzed	call on org.apache.commons.logging.Log:warn
unanalyzed	call on org.apache.commons.logging.Log:debug
unanalyzed	call on java.lang.Boolean
unanalyzed	call on java.lang.Boolean:booleanValue
test_vector	java.lang.String:indexOf(...)@402: {-1}, {-2³¹..-2, 0..2³²-1}

info method not available -- call on void org.apache.roller.weblogger.util. RollerMessages:addError(String)

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

info method not available -- call on void org.apache.roller.weblogger.util. RollerMessages:addError(String, String)

info method not available -- call on String org.apache.commons.lang. StringUtils:deleteWhitespace(String)

info method not available -- call on String[] org.apache.commons.lang. StringUtils:split(String, String)

info method not available -- call on void org.apache.roller.weblogger.util. RollerMessages:addError(String, String)

info method not available -- call on void org.apache.roller.weblogger.util. RollerMessages:addError(String)

method	long getDirSize(File, bool)
pre	dir != null
presumption	files.length@424 <= 2³²-1
presumption	java.io.File:listFiles(...)@424 != null
post	init'ed(return_value)
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.File:canRead
unanalyzed	call on java.io.File:isDirectory
unanalyzed	call on java.io.File:listFiles
unanalyzed	call on java.io.File:length
unanalyzed	call on getDirSize
test_vector	recurse: {0}, {1}
test_vector	java.io.File:canRead(...)@423: {0}, {1}
test_vector	java.io.File:exists(...)@423: {0}, {1}
test_vector	java.io.File:isDirectory(...)@423: {0}, {1}
test_vector	java.io.File:isDirectory(...)@427: {1}, {0}

Prev Msg Next Msg

+

click for all messages in this file high

null dereference check fails here: requires files[i] != null

Prev Msg Next Msg

method	bool checkFileType(String[], String[], String, String)
pre	(soft) allowFiles.length <= 2³²-1
pre	(soft) allowFiles[...] != null
pre	(soft) fileName != null
pre	(soft) forbidFiles.length <= 2³²-1
pre	(soft) forbidFiles[...] != null
post	init'ed(return_value)
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.lang.String:split
test_vector	allowFiles: Inverse{null}, Addr_Set{null}
test_vector	allowFiles.length: {1..2³²-1}, {0}
test_vector	contentType: Addr_Set{null}, Inverse{null}
test_vector	forbidFiles: Addr_Set{null}, Inverse{null}
test_vector	forbidFiles.length: {0}, {1..2³²-1}
test_vector	java.lang.String:endsWith(...)@476: {0}, {1}
test_vector	java.lang.String:endsWith(...)@503: {0}, {1}
test_vector	java.lang.String:indexOf(...)@456: {-2³¹. .-2, 0..2³²-1}, {-1}

method	bool matchContentType(String, String)
pre	rangeRule != null
pre	(soft) contentType != null
post	init'ed(return_value)
test_vector	java.lang.String:equals(...)@532: {0}, {1}
test_vector	java.lang.String:equals(...)@533: {0}, {1}
test_vector	java.lang.String:equals(...)@536: {0}, {1}

Prev Msg Next Msg

+

click for all messages in this file high

array index out of bounds check fails here: requires ruleParts.length >= 2

+

medium

null dereference check might fail: requires not_init'ed(ruleParts[0] )

+

click for all messages in this file medium

null dereference check might fail: requires not_init'ed(ruleParts[1] )

+

low

use of default init check might fail: requires init'ed(ruleParts. length)

+

click for all messages in this file low

use of default init check might fail: requires init'ed(typeParts. length)

Prev Msg Next Msg

method	File getRealFile(Weblog, String)
pre	init'ed(this.upload_dir)
pre	weblog != null
presumption	init'ed(java.io.File.separator)
presumption	init'ed(java.io.File.separatorChar)
presumption	java.io.File:canRead(...)@584 == 1
presumption	java.io.File:exists(...)@581 == 1
presumption	java.io.File:getCanonicalPath(...)@591 != null
presumption	java.lang.String:indexOf(...)@563 - java.lang.String:lastIndexOf(...)@563 in 0..6_442_450_943
presumption	java.lang.String:startsWith(...)@591 == 1
post	return_value == &new File(getRealFile#6)
post	new File(getRealFile#6) num objects == 1
unanalyzed	call on org.apache.roller.weblogger. WebloggerException
unanalyzed	call on org.apache.roller.RollerException
test_vector	path: Addr_Set{null}, Inverse{null}
test_vector	java.io.File:exists(...)@551: {1}, {0}
test_vector	java.lang.String:startsWith(...)@557: {0}, {1}

info method not available -- call on String org.apache.roller.weblogger. pojos.Weblog:getHandle()

method	void org.apache.roller.weblogger.business. FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)
post	this.relativePath == path
post	init'ed(this.relativePath)
post	this.resourceFile == file
post	init'ed(this.resourceFile)
post	this.weblog == weblog
post	init'ed(this.weblog)

method	Weblog getWeblog()
pre	init'ed(this.weblog)
post	return_value == this.weblog
post	init'ed(return_value)

method	ThemeResource[] getChildren()
pre	this.resourceFile != null
pre	(soft) init'ed(this.relativePath)
pre	(soft) init'ed(this.weblog)
presumption	dirFiles.length@643 <= 2³²-1
presumption	java.io.File:listFiles(...)@643 != null
post	init'ed(java.lang.StringBuilder:toString(...)._ tainted)
post	return_value in Addr_Set{null,&new ThemeResource[](getChildren#2)}
post	new FileManagerImpl$WeblogResourceFile(getChildren# 4) num objects <= 2³²-1
post	possibly_updated(new FileManagerImpl$WeblogResource File(getChildren#4).relativePath)
post	new FileManagerImpl$WeblogResourceFile(getChildren# 4).resourceFile == null
post	new FileManagerImpl$WeblogResourceFile(getChildren# 4).weblog == this.weblog
post	(soft) init'ed(new FileManagerImpl$WeblogResourceFi le(getChildren#4).weblog)
post	new ThemeResource[](getChildren#2) num objects <= 1
post	(soft) new ThemeResource[](getChildren#2).length <= 2³²-1
post	possibly_updated(new ThemeResource[](getChildren#2) [...])
test_vector	this.relativePath: Addr_Set{null}, Inverse{null}
test_vector	java.io.File:isDirectory(...)@638: {1}, {0}
test_vector	java.lang.String:equals(...)@653: {1}, {0}

method

void org.apache.roller.weblogger.business. FileManagerImpl$WeblogResourceFile$1(FileManagerImp l$WeblogResourceFile)

method	bool accept(File)
post	init'ed(return_value)

Prev Msg Next Msg

+

click for all messages in this file medium

null dereference check might fail: requires not_init'ed(dirFiles[i])

Prev Msg Next Msg

method	String getName()
pre	this.resourceFile != null
post	init'ed(return_value)

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

method	long getLastModified()
pre	this.resourceFile != null
post	init'ed(return_value)

method	long getLength()
pre	this.resourceFile != null
post	init'ed(return_value)

method	bool isDirectory()
pre	this.resourceFile != null
post	init'ed(return_value)

method	bool isFile()
pre	this.resourceFile != null
post	init'ed(return_value)

method	InputStream getInputStream()
pre	init'ed(this.resourceFile)
post	return_value == &new FileInputStream(getInputSt ream#1)
post	new FileInputStream(getInputStream#1) num objects == 1

	info	method not available	-- call on String org.apache.commons.lang. StringUtils:deleteWhitespace(String)
	info	method not available	-- call on String[] org.apache.commons.lang. StringUtils:split(String, String)