//# 24 errors, 1,206 messages
//#
/*
    //#FileManagerImpl.java:1:1: class: org.apache.roller.weblogger.business.FileManagerImpl$1
    //#FileManagerImpl.java:1:1: method: org.apache.roller.weblogger.business.FileManagerImpl$1.org.apache.roller.weblogger.business.FileManagerImpl$1__static_init
    //#FileManagerImpl.java:1:1: class: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1
    //#FileManagerImpl.java:1:1: method: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1.org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1__static_init
    //#FileManagerImpl.java:1:1: class: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile
    //#FileManagerImpl.java:1:1: method: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init
    //#FileManagerImpl.java:1:1: class: org.apache.roller.weblogger.business.FileManagerImpl
 * Licensed to the Apache Software Foundation (ASF) under one or more
 *  contributor license agreements.  The ASF licenses this file to You
 * under the Apache License, Version 2.0 (the "License"); you may not
 * use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.  For additional information regarding
 * copyright in this work, please see the NOTICE file in the top level
 * directory of this distribution.
 */

package org.apache.roller.weblogger.business;

import java.io.File;
import java.io.FileFilter;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.OutputStream;
import java.math.BigDecimal;
import org.apache.commons.lang.StringUtils;
import org.apache.commons.logging.Log;
import org.apache.commons.logging.LogFactory;
import org.apache.roller.weblogger.config.WebloggerConfig;
import org.apache.roller.weblogger.config.WebloggerRuntimeConfig;
import org.apache.roller.weblogger.pojos.ThemeResource;
import org.apache.roller.weblogger.pojos.Weblog;
import org.apache.roller.weblogger.util.RollerMessages;


/**
 * Manages files uploaded to Roller weblogs.  
 * 
 * This base implementation writes resources to a filesystem.
 */
public class FileManagerImpl implements FileManager {
    
    private static Log log = LogFactory.getLog(FileManagerImpl.class);
    //#FileManagerImpl.java:46: method: org.apache.roller.weblogger.business.FileManagerImpl.org.apache.roller.weblogger.business.FileManagerImpl__static_init
    //#FileManagerImpl.java:46: Warning: method not available
    //#    -- call on Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: org.apache.roller.weblogger.business.FileManagerImpl__static_init
    //#    unanalyzed callee: Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl]
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.canSave(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;Ljava/lang/String;JLorg/apache/roller/weblogger/util/RollerMessages;)Z
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.checkFileType([Ljava/lang/String;[Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;)Z
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.createDirectory(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)V
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.deleteAllFiles(Ljava/io/File;)V
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.deleteAllFiles(Lorg/apache/roller/weblogger/pojos/Weblog;)V
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.deleteFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)V
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.getDirSize(Ljava/io/File;Z)J
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.getDirectories(Lorg/apache/roller/weblogger/pojos/Weblog;)[Lorg/apache/roller/weblogger/pojos/ThemeResource;
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.getFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/ThemeResource;
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.getFiles(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)[Lorg/apache/roller/weblogger/pojos/ThemeResource;
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.getRealFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)Ljava/io/File;
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.matchContentType(Ljava/lang/String;Ljava/lang/String;)Z
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.overQuota(Lorg/apache/roller/weblogger/pojos/Weblog;)Z
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.release()V
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.saveFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;Ljava/lang/String;JLjava/io/InputStream;)V
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.saveFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;Ljava/lang/String;JLjava/io/InputStream;Z)V
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): log
    //#output(org.apache.roller.weblogger.business.FileManagerImpl__static_init): org/apache/roller/weblogger/business/FileManager.__Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl]
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): org/apache/roller/weblogger/business/FileManager.__Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.canSave(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;Ljava/lang/String;JLorg/apache/roller/weblogger/util/RollerMessages;)Z == &canSave
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.checkFileType([Ljava/lang/String;[Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;)Z == &checkFileType
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.createDirectory(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)V == &createDirectory
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.deleteAllFiles(Ljava/io/File;)V == &deleteAllFiles
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.deleteAllFiles(Lorg/apache/roller/weblogger/pojos/Weblog;)V == &deleteAllFiles
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.deleteFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)V == &deleteFile
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.getDirSize(Ljava/io/File;Z)J == &getDirSize
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.getDirectories(Lorg/apache/roller/weblogger/pojos/Weblog;)[Lorg/apache/roller/weblogger/pojos/ThemeResource; == &getDirectories
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.getFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/ThemeResource; == &getFile
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.getFiles(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)[Lorg/apache/roller/weblogger/pojos/ThemeResource; == &getFiles
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.getRealFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)Ljava/io/File; == &getRealFile
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.matchContentType(Ljava/lang/String;Ljava/lang/String;)Z == &matchContentType
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.overQuota(Lorg/apache/roller/weblogger/pojos/Weblog;)Z == &overQuota
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.release()V == &release
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.saveFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;Ljava/lang/String;JLjava/io/InputStream;)V == &saveFile
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): __Dispatch_Table.saveFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;Ljava/lang/String;JLjava/io/InputStream;Z)V == &saveFile
    //#post(org.apache.roller.weblogger.business.FileManagerImpl__static_init): init'ed(log)
    //#FileManagerImpl.java:46: end of method: org.apache.roller.weblogger.business.FileManagerImpl.org.apache.roller.weblogger.business.FileManagerImpl__static_init
    
    private String upload_dir = null;
    
    
    /**
     * Create file manager.
     */
    public FileManagerImpl() {
    //#FileManagerImpl.java:54: method: void org.apache.roller.weblogger.business.FileManagerImpl.org.apache.roller.weblogger.business.FileManagerImpl()
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): "="._tainted
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): "Fetching property ["._tainted
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): "]"._tainted
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): "roller_data"._tainted
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): "uploads"._tainted
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): "uploads.dir"._tainted
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): java.io.File.separator
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): java.io.File.separator._tainted
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): java.io.File.separatorChar
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): org/apache/roller/weblogger/config/WebloggerConfig.config
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): org/apache/roller/weblogger/config/WebloggerConfig.log
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl()): this
    //#output(void org.apache.roller.weblogger.business.FileManagerImpl()): this.upload_dir
    //#pre[1] (void org.apache.roller.weblogger.business.FileManagerImpl()): org/apache/roller/weblogger/config/WebloggerConfig.config != null
    //#pre[2] (void org.apache.roller.weblogger.business.FileManagerImpl()): org/apache/roller/weblogger/config/WebloggerConfig.log != null
    //#presumption(void org.apache.roller.weblogger.business.FileManagerImpl()): init'ed(java.io.File.separator)
    //#presumption(void org.apache.roller.weblogger.business.FileManagerImpl()): init'ed(java.io.File.separatorChar)
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl()): this.upload_dir != null
    //#unanalyzed(void org.apache.roller.weblogger.business.FileManagerImpl()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void org.apache.roller.weblogger.business.FileManagerImpl()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void org.apache.roller.weblogger.business.FileManagerImpl()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void org.apache.roller.weblogger.business.FileManagerImpl()): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(void org.apache.roller.weblogger.business.FileManagerImpl()): Effects-of-calling:org.apache.commons.logging.Log:debug
    //#unanalyzed(void org.apache.roller.weblogger.business.FileManagerImpl()): Effects-of-calling:java.util.Properties:getProperty
    //#test_vector(void org.apache.roller.weblogger.business.FileManagerImpl()): java.lang.String:endsWith(...)@62: {1}, {0}
    //#test_vector(void org.apache.roller.weblogger.business.FileManagerImpl()): java.lang.String:length(...)@59: {1..4_294_967_295}, {0}
        String uploaddir = WebloggerConfig.getProperty("uploads.dir");
        
        // Note: System property expansion is now handled by WebloggerConfig.
        
        if(uploaddir == null || uploaddir.trim().length() < 1)
            uploaddir = System.getProperty("user.home") + File.separator+"roller_data"+File.separator+"uploads";
        
        if( ! uploaddir.endsWith(File.separator))
            uploaddir += File.separator;
        
        this.upload_dir = uploaddir.replace('/',File.separatorChar);
    }
    //#FileManagerImpl.java:66: end of method: void org.apache.roller.weblogger.business.FileManagerImpl.org.apache.roller.weblogger.business.FileManagerImpl()
    
    
    /**
     * @see org.apache.roller.weblogger.model.FileManager#getFile(weblog, java.lang.String)
     */
    public ThemeResource getFile(Weblog weblog, String path) 
            throws FileNotFoundException, FilePathException {
        
        // get a reference to the file, checks that file exists & is readable
        File resourceFile = this.getRealFile(weblog, path);
    //#FileManagerImpl.java:76: method: ThemeResource org.apache.roller.weblogger.business.FileManagerImpl.getFile(Weblog, String)
    //#input(ThemeResource getFile(Weblog, String)): "Invalid path ["._tainted
    //#input(ThemeResource getFile(Weblog, String)): "], "._tainted
    //#input(ThemeResource getFile(Weblog, String)): "cannot read from path."._tainted
    //#input(ThemeResource getFile(Weblog, String)): "directory doesn't exist."._tainted
    //#input(ThemeResource getFile(Weblog, String)): "path is a directory."._tainted
    //#input(ThemeResource getFile(Weblog, String)): "trying to get outside uploads dir."._tainted
    //#input(ThemeResource getFile(Weblog, String)): "trying to use nested directories."._tainted
    //#input(ThemeResource getFile(Weblog, String)): java.io.File.separator
    //#input(ThemeResource getFile(Weblog, String)): java.io.File.separator._tainted
    //#input(ThemeResource getFile(Weblog, String)): java.io.File.separatorChar
    //#input(ThemeResource getFile(Weblog, String)): path
    //#input(ThemeResource getFile(Weblog, String)): path._tainted
    //#input(ThemeResource getFile(Weblog, String)): this
    //#input(ThemeResource getFile(Weblog, String)): this.upload_dir
    //#input(ThemeResource getFile(Weblog, String)): this.upload_dir._tainted
    //#input(ThemeResource getFile(Weblog, String)): weblog
    //#output(ThemeResource getFile(Weblog, String)): new File(getRealFile#6) num objects
    //#output(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3) num objects
    //#output(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).__Tag
    //#output(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).relativePath
    //#output(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).resourceFile
    //#output(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).this$0
    //#output(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).weblog
    //#output(ThemeResource getFile(Weblog, String)): return_value
    //#new obj(ThemeResource getFile(Weblog, String)): new File(getRealFile#6)
    //#new obj(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3)
    //#pre[4] (ThemeResource getFile(Weblog, String)): init'ed(this.upload_dir)
    //#pre[6] (ThemeResource getFile(Weblog, String)): weblog != null
    //#presumption(ThemeResource getFile(Weblog, String)): java.io.File:isDirectory(...)@79 == 0
    //#post(ThemeResource getFile(Weblog, String)): return_value == &new FileManagerImpl$WeblogResourceFile(getFile#3)
    //#post(ThemeResource getFile(Weblog, String)): new File(getRealFile#6) num objects == 1
    //#post(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3) num objects == 1
    //#post(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).__Tag == org/apache/roller/weblogger/business/FileManagerImpl$WeblogResourceFile
    //#post(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).relativePath == path
    //#post(ThemeResource getFile(Weblog, String)): init'ed(new FileManagerImpl$WeblogResourceFile(getFile#3).relativePath)
    //#post(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).resourceFile == &new File(getRealFile#6)
    //#post(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).this$0 == this
    //#post(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).this$0 != null
    //#post(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).weblog == weblog
    //#post(ThemeResource getFile(Weblog, String)): new FileManagerImpl$WeblogResourceFile(getFile#3).weblog != null
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.io.File
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(ThemeResource getFile(Weblog, String)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
        
        // make sure file is not a directory
        if(resourceFile.isDirectory()) {
            throw new FilePathException("Invalid path ["+path+"], "+
                    "path is a directory.");
        }
        
        // everything looks good, return resource
        return new WeblogResourceFile(weblog, path, resourceFile);
    //#FileManagerImpl.java:85: end of method: ThemeResource org.apache.roller.weblogger.business.FileManagerImpl.getFile(Weblog, String)
    }
    
    
    /**
     * @see org.apache.roller.weblogger.model.FileManager#getFiles(weblog, java.lang.String)
     */
    public ThemeResource[] getFiles(Weblog weblog, String path) 
            throws FileNotFoundException, FilePathException {
        
        // get a reference to the dir, checks that dir exists & is readable
        File dirFile = this.getRealFile(weblog, path);
    //#FileManagerImpl.java:96: method: ThemeResource[] org.apache.roller.weblogger.business.FileManagerImpl.getFiles(Weblog, String)
    //#input(ThemeResource[] getFiles(Weblog, String)): "Invalid path ["._tainted
    //#input(ThemeResource[] getFiles(Weblog, String)): "], "._tainted
    //#input(ThemeResource[] getFiles(Weblog, String)): "cannot read from path."._tainted
    //#input(ThemeResource[] getFiles(Weblog, String)): "directory doesn't exist."._tainted
    //#input(ThemeResource[] getFiles(Weblog, String)): "path is not a directory."._tainted
    //#input(ThemeResource[] getFiles(Weblog, String)): "trying to get outside uploads dir."._tainted
    //#input(ThemeResource[] getFiles(Weblog, String)): "trying to use nested directories."._tainted
    //#input(ThemeResource[] getFiles(Weblog, String)): java.io.File.separator
    //#input(ThemeResource[] getFiles(Weblog, String)): java.io.File.separator._tainted
    //#input(ThemeResource[] getFiles(Weblog, String)): java.io.File.separatorChar
    //#input(ThemeResource[] getFiles(Weblog, String)): path
    //#input(ThemeResource[] getFiles(Weblog, String)): path._tainted
    //#input(ThemeResource[] getFiles(Weblog, String)): this
    //#input(ThemeResource[] getFiles(Weblog, String)): this.upload_dir
    //#input(ThemeResource[] getFiles(Weblog, String)): this.upload_dir._tainted
    //#input(ThemeResource[] getFiles(Weblog, String)): weblog
    //#output(ThemeResource[] getFiles(Weblog, String)): return_value
    //#pre[4] (ThemeResource[] getFiles(Weblog, String)): init'ed(this.upload_dir)
    //#pre[6] (ThemeResource[] getFiles(Weblog, String)): weblog != null
    //#presumption(ThemeResource[] getFiles(Weblog, String)): java.io.File:isDirectory(...)@99 == 1
    //#post(ThemeResource[] getFiles(Weblog, String)): init'ed(return_value)
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.io.File
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(ThemeResource[] getFiles(Weblog, String)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
        
        // make sure path is a directory
        if(!dirFile.isDirectory()) {
            throw new FilePathException("Invalid path ["+path+"], "+
                    "path is not a directory.");
        }
        
        // everything looks good, list contents
        ThemeResource dir = new WeblogResourceFile(weblog, path, dirFile);
        
        return dir.getChildren();
    //#FileManagerImpl.java:107: Warning: method not available
    //#    -- call on ThemeResource[] org.apache.roller.weblogger.pojos.ThemeResource:getChildren()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: ThemeResource[] getFiles(Weblog, String)
    //#    unanalyzed callee: ThemeResource[] org.apache.roller.weblogger.pojos.ThemeResource:getChildren()
    //#FileManagerImpl.java:107: end of method: ThemeResource[] org.apache.roller.weblogger.business.FileManagerImpl.getFiles(Weblog, String)
    }
    
    
    /**
     * @see org.apache.roller.weblogger.model.FileManager#getDirectories(weblog)
     */
    public ThemeResource[] getDirectories(Weblog weblog)
            throws FileNotFoundException, FilePathException {
        
        // get a reference to the root dir, checks that dir exists & is readable
        File dirFile = this.getRealFile(weblog, null);
    //#FileManagerImpl.java:118: method: ThemeResource[] org.apache.roller.weblogger.business.FileManagerImpl.getDirectories(Weblog)
    //#input(ThemeResource[] getDirectories(Weblog)): "Invalid path ["._tainted
    //#input(ThemeResource[] getDirectories(Weblog)): "], "._tainted
    //#input(ThemeResource[] getDirectories(Weblog)): "cannot read from path."._tainted
    //#input(ThemeResource[] getDirectories(Weblog)): "directory doesn't exist."._tainted
    //#input(ThemeResource[] getDirectories(Weblog)): "trying to get outside uploads dir."._tainted
    //#input(ThemeResource[] getDirectories(Weblog)): "trying to use nested directories."._tainted
    //#input(ThemeResource[] getDirectories(Weblog)): java.io.File.separator
    //#input(ThemeResource[] getDirectories(Weblog)): java.io.File.separator._tainted
    //#input(ThemeResource[] getDirectories(Weblog)): java.io.File.separatorChar
    //#input(ThemeResource[] getDirectories(Weblog)): this
    //#input(ThemeResource[] getDirectories(Weblog)): this.upload_dir
    //#input(ThemeResource[] getDirectories(Weblog)): this.upload_dir._tainted
    //#input(ThemeResource[] getDirectories(Weblog)): weblog
    //#output(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3) num objects
    //#output(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).__Tag
    //#output(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).relativePath
    //#output(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).resourceFile
    //#output(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).this$0
    //#output(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).weblog
    //#output(ThemeResource[] getDirectories(Weblog)): new ThemeResource[](getDirectories#2) num objects
    //#output(ThemeResource[] getDirectories(Weblog)): return_value.length
    //#output(ThemeResource[] getDirectories(Weblog)): return_value[0..4_294_967_295]
    //#output(ThemeResource[] getDirectories(Weblog)): return_value
    //#new obj(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3)
    //#new obj(ThemeResource[] getDirectories(Weblog)): new ThemeResource[](getDirectories#2)
    //#pre[2] (ThemeResource[] getDirectories(Weblog)): init'ed(this.upload_dir)
    //#pre[4] (ThemeResource[] getDirectories(Weblog)): weblog != null
    //#presumption(ThemeResource[] getDirectories(Weblog)): dirFiles.length@121 <= 4_294_967_295
    //#presumption(ThemeResource[] getDirectories(Weblog)): java.io.File:listFiles(...)@121 != null
    //#post(ThemeResource[] getDirectories(Weblog)): return_value == &new ThemeResource[](getDirectories#2)
    //#post(ThemeResource[] getDirectories(Weblog)): (soft) new FileManagerImpl$WeblogResourceFile(getDirectories#3) num objects <= 4_294_967_295
    //#post(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).__Tag == org/apache/roller/weblogger/business/FileManagerImpl$WeblogResourceFile
    //#post(ThemeResource[] getDirectories(Weblog)): init'ed(new FileManagerImpl$WeblogResourceFile(getDirectories#3).relativePath)
    //#post(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).resourceFile == null
    //#post(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).this$0 == this
    //#post(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).this$0 != null
    //#post(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).weblog == weblog
    //#post(ThemeResource[] getDirectories(Weblog)): new FileManagerImpl$WeblogResourceFile(getDirectories#3).weblog != null
    //#post(ThemeResource[] getDirectories(Weblog)): new ThemeResource[](getDirectories#2) num objects == 1
    //#post(ThemeResource[] getDirectories(Weblog)): (soft) return_value.length <= 4_294_967_295
    //#post(ThemeResource[] getDirectories(Weblog)): possibly_updated(return_value[0..4_294_967_295])
    //#post(ThemeResource[] getDirectories(Weblog)): (soft) new FileManagerImpl$WeblogResourceFile(getDirectories#3) num objects == dirFiles.length@121
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.io.File
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(ThemeResource[] getDirectories(Weblog)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
        
        // we only want a list of directories
        File[] dirFiles = dirFile.listFiles(new FileFilter() {
    //#FileManagerImpl.java:121: method: void org.apache.roller.weblogger.business.FileManagerImpl$1.org.apache.roller.weblogger.business.FileManagerImpl$1(FileManagerImpl)
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl$1(FileManagerImpl)): Param_1
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl$1(FileManagerImpl)): this
    //#output(void org.apache.roller.weblogger.business.FileManagerImpl$1(FileManagerImpl)): this.this$0
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$1(FileManagerImpl)): this.this$0 == Param_1
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$1(FileManagerImpl)): init'ed(this.this$0)
    //#FileManagerImpl.java:121: end of method: void org.apache.roller.weblogger.business.FileManagerImpl$1.org.apache.roller.weblogger.business.FileManagerImpl$1(FileManagerImpl)
            public boolean accept(File f) {
                return (f != null) ? f.isDirectory() : false;
    //#FileManagerImpl.java:123: method: bool org.apache.roller.weblogger.business.FileManagerImpl$1.accept(File)
    //#input(bool accept(File)): f
    //#output(bool accept(File)): return_value
    //#post(bool accept(File)): init'ed(return_value)
    //#FileManagerImpl.java:123: end of method: bool org.apache.roller.weblogger.business.FileManagerImpl$1.accept(File)
            }
        });
        
        // convert 'em to ThemeResource objects
        ThemeResource[] resources = new ThemeResource[dirFiles.length];
        for(int i=0; i < dirFiles.length; i++) {
            String filePath = dirFiles[i].getName();
    //#FileManagerImpl.java:130: ?use of default init
    //#    init'ed(dirFiles[i])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: ThemeResource[] getDirectories(Weblog)
    //#    basic block: bb_3
    //#    assertion: init'ed(dirFiles[i])
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    //#FileManagerImpl.java:130: ?null dereference
    //#    not_init'ed(dirFiles[i])
    //#    severity: MEDIUM
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: ThemeResource[] getDirectories(Weblog)
    //#    basic block: bb_3
    //#    assertion: not_init'ed(dirFiles[i])
    //#    VN: undefined
    //#    Expected: Inverse{null} or Invalid
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
            resources[i] = new WeblogResourceFile(weblog, filePath, dirFiles[i]);
    //#FileManagerImpl.java:131: ?use of default init
    //#    init'ed(dirFiles[i])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: ThemeResource[] getDirectories(Weblog)
    //#    basic block: bb_3
    //#    assertion: init'ed(dirFiles[i])
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
        }
            
        return resources;
    //#FileManagerImpl.java:134: end of method: ThemeResource[] org.apache.roller.weblogger.business.FileManagerImpl.getDirectories(Weblog)
    }
    
    
    /**
     * @see org.apache.roller.weblogger.model.FileManager#saveFile(weblog, java.lang.String, java.lang.String, long, java.io.InputStream)
     */
    public void saveFile(Weblog weblog, 
                         String path, 
                         String contentType, 
                         long size, 
                         InputStream is) 
            throws FileNotFoundException, FilePathException, FileIOException {
        
        saveFile(weblog, path, contentType, size, is, true);
    //#FileManagerImpl.java:148: method: void org.apache.roller.weblogger.business.FileManagerImpl.saveFile(Weblog, String, String, long, InputStream)
    //#FileManagerImpl.java:148: Warning: suspicious precondition
    //#    the precondition for org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: void saveFile(Weblog, String, String, long, InputStream)
    //#    suspicious precondition index: [6]
    //#    Attribs:  Soft
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "="._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "Creating directory ["._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "Invalid path ["._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "The file has been written to ["._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "Trouble accessing property: "._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "] automatically"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "]"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "], "._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "attempted save file size = "._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "cannot read from path."._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "directory doesn't exist."._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "fetched property ["._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "max allowed file size = "._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "trying to get outside uploads dir."._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "trying to use nested directories."._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "uploads.dir.maxsize"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "uploads.enabled"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "uploads.file.maxsize"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "uploads.types.allowed"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): "uploads.types.forbid"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): __Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): __Descendant_Table[others]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): __Dispatch_Table.saveFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;Ljava/lang/String;JLjava/io/InputStream;Z)V
    //#input(void saveFile(Weblog, String, String, long, InputStream)): contentType
    //#input(void saveFile(Weblog, String, String, long, InputStream)): contentType._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): is
    //#input(void saveFile(Weblog, String, String, long, InputStream)): java.io.File.separator
    //#input(void saveFile(Weblog, String, String, long, InputStream)): java.io.File.separator._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): java.io.File.separatorChar
    //#input(void saveFile(Weblog, String, String, long, InputStream)): log
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/GuiceWebloggerProvider.__Dispatch_Table.getWeblogger()Lorg/apache/roller/weblogger/business/Weblogger;
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[org/apache/roller/weblogger/business/PropertiesManager]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAPropertiesManagerImpl]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[others]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/PropertiesManager.__Dispatch_Table.getProperty(Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/RuntimeConfigProperty;
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerImpl]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/Weblogger]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[others]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/Weblogger.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.__Tag
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.__Tag
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy.__Tag
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy.threadLocalEntityManager
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerImpl.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[org/apache/roller/weblogger/business/GuiceWebloggerProvider]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerProvider]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[others]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/WebloggerProvider.__Dispatch_Table.getWeblogger()Lorg/apache/roller/weblogger/business/Weblogger;
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Descendant_Table[others]
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Dispatch_Table.load(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Object;
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/jpa/JPAPropertiesManagerImpl.__Dispatch_Table.getProperty(Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/RuntimeConfigProperty;
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(void saveFile(Weblog, String, String, long, InputStream)): org/apache/roller/weblogger/config/WebloggerRuntimeConfig.log
    //#input(void saveFile(Weblog, String, String, long, InputStream)): path
    //#input(void saveFile(Weblog, String, String, long, InputStream)): path._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): size
    //#input(void saveFile(Weblog, String, String, long, InputStream)): this
    //#input(void saveFile(Weblog, String, String, long, InputStream)): this.__Tag
    //#input(void saveFile(Weblog, String, String, long, InputStream)): this.upload_dir
    //#input(void saveFile(Weblog, String, String, long, InputStream)): this.upload_dir._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream)): weblog
    //#pre[3] (void saveFile(Weblog, String, String, long, InputStream)): is != null
    //#pre[4] (void saveFile(Weblog, String, String, long, InputStream)): log != null
    //#pre[16] (void saveFile(Weblog, String, String, long, InputStream)): path != null
    //#pre[20] (void saveFile(Weblog, String, String, long, InputStream)): this.__Tag == org/apache/roller/weblogger/business/FileManagerImpl
    //#pre[21] (void saveFile(Weblog, String, String, long, InputStream)): init'ed(this.upload_dir)
    //#pre[23] (void saveFile(Weblog, String, String, long, InputStream)): weblog != null
    //#pre[5] (void saveFile(Weblog, String, String, long, InputStream)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider != null
    //#pre[6] (void saveFile(Weblog, String, String, long, InputStream)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag in {org/apache/roller/weblogger/business/GuiceWebloggerProvider, org/apache/roller/weblogger/business/WebloggerProvider}
    //#pre[7] (void saveFile(Weblog, String, String, long, InputStream)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance != null
    //#pre[15] (void saveFile(Weblog, String, String, long, InputStream)): (soft) org/apache/roller/weblogger/config/WebloggerRuntimeConfig.log != null
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.String:endsWith
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.File
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.File:isDirectory
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.File:listFiles
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.File:length
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:getDirSize
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.String:split
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.String:toLowerCase
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:getBooleanProperty
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.roller.weblogger.util.RollerMessages:addError
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:getProperty
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.math.BigDecimal
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.math.BigDecimal:doubleValue
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.commons.logging.Log:debug
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.math.BigDecimal:toString
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.commons.lang.StringUtils:deleteWhitespace
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.commons.lang.StringUtils:split
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.RuntimeException
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.File:mkdir
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.roller.weblogger.util.RollerMessages
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.roller.weblogger.util.RollerMessages:toString
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.FileOutputStream
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.InputStream:read
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.OutputStream:write
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.OutputStream:flush
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.io.OutputStream:close
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:getWeblogger
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:getPropertiesManager
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.ThreadLocal:get
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:javax.persistence.EntityManagerFactory:createEntityManager
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.ThreadLocal:set
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:javax.persistence.EntityManager:getTransaction
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:javax.persistence.EntityTransaction:isActive
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:javax.persistence.EntityTransaction:begin
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:javax.persistence.EntityManager:find
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.roller.weblogger.pojos.RuntimeConfigProperty:getValue
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:org.apache.commons.logging.Log:warn
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.Boolean
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream)): Effects-of-calling:java.lang.Boolean:booleanValue
    }
    //#FileManagerImpl.java:149: end of method: void org.apache.roller.weblogger.business.FileManagerImpl.saveFile(Weblog, String, String, long, InputStream)
    
    /**
     * @see org.apache.roller.weblogger.model.FileManager#saveFile(weblog, java.lang.String, java.lang.String, long, java.io.InputStream)
     */
    public void saveFile(Weblog weblog, 
                         String path, 
                         String contentType, 
                         long size, 
                         InputStream is,
                         boolean checkCanSave)
            throws FileNotFoundException, FilePathException, FileIOException {
        
        String savePath = path;
    //#FileManagerImpl.java:162: method: void org.apache.roller.weblogger.business.FileManagerImpl.saveFile(Weblog, String, String, long, InputStream, bool)
    //#FileManagerImpl.java:162: Warning: suspicious precondition
    //#    the precondition for org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: void saveFile(Weblog, String, String, long, InputStream, bool)
    //#    suspicious precondition index: [7]
    //#    Attribs:  Soft
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "="._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "Creating directory ["._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "Invalid path ["._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "The file has been written to ["._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "Trouble accessing property: "._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "] automatically"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "]"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "], "._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "attempted save file size = "._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "cannot read from path."._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "directory doesn't exist."._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "fetched property ["._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "max allowed file size = "._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "trying to get outside uploads dir."._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "trying to use nested directories."._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "uploads.dir.maxsize"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "uploads.enabled"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "uploads.file.maxsize"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "uploads.types.allowed"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): "uploads.types.forbid"._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): checkCanSave
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): contentType
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): contentType._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): is
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): java.io.File.separator
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): java.io.File.separator._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): java.io.File.separatorChar
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): log
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/GuiceWebloggerProvider.__Dispatch_Table.getWeblogger()Lorg/apache/roller/weblogger/business/Weblogger;
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[org/apache/roller/weblogger/business/PropertiesManager]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAPropertiesManagerImpl]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[others]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/PropertiesManager.__Dispatch_Table.getProperty(Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/RuntimeConfigProperty;
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerImpl]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/Weblogger]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[others]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/Weblogger.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.__Tag
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.__Tag
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy.__Tag
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy.threadLocalEntityManager
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerImpl.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[org/apache/roller/weblogger/business/GuiceWebloggerProvider]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerProvider]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[others]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/WebloggerProvider.__Dispatch_Table.getWeblogger()Lorg/apache/roller/weblogger/business/Weblogger;
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Descendant_Table[others]
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Dispatch_Table.load(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Object;
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/jpa/JPAPropertiesManagerImpl.__Dispatch_Table.getProperty(Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/RuntimeConfigProperty;
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): org/apache/roller/weblogger/config/WebloggerRuntimeConfig.log
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): path
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): path._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): size
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): this
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): this.upload_dir
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): this.upload_dir._tainted
    //#input(void saveFile(Weblog, String, String, long, InputStream, bool)): weblog
    //#pre[4] (void saveFile(Weblog, String, String, long, InputStream, bool)): is != null
    //#pre[5] (void saveFile(Weblog, String, String, long, InputStream, bool)): log != null
    //#pre[17] (void saveFile(Weblog, String, String, long, InputStream, bool)): path != null
    //#pre[21] (void saveFile(Weblog, String, String, long, InputStream, bool)): init'ed(this.upload_dir)
    //#pre[23] (void saveFile(Weblog, String, String, long, InputStream, bool)): weblog != null
    //#pre[2] (void saveFile(Weblog, String, String, long, InputStream, bool)): (soft) contentType init'ed
    //#pre[6] (void saveFile(Weblog, String, String, long, InputStream, bool)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider != null
    //#pre[7] (void saveFile(Weblog, String, String, long, InputStream, bool)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag in {org/apache/roller/weblogger/business/GuiceWebloggerProvider, org/apache/roller/weblogger/business/WebloggerProvider}
    //#pre[8] (void saveFile(Weblog, String, String, long, InputStream, bool)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance != null
    //#pre[16] (void saveFile(Weblog, String, String, long, InputStream, bool)): (soft) org/apache/roller/weblogger/config/WebloggerRuntimeConfig.log != null
    //#presumption(void saveFile(Weblog, String, String, long, InputStream, bool)): (int) (java.math.BigDecimal:doubleValue(...)@366*1024000) in range
    //#presumption(void saveFile(Weblog, String, String, long, InputStream, bool)): (int) (java.math.BigDecimal:doubleValue(...)@366*1024000) - size in range
    //#presumption(void saveFile(Weblog, String, String, long, InputStream, bool)): size <= (int) (java.math.BigDecimal:doubleValue(...)@366*1024000) | canSave(...) == 0
    //#presumption(void saveFile(Weblog, String, String, long, InputStream, bool)): (size + canSave(...)) - (int) (java.math.BigDecimal:doubleValue(...)@377*1024000) in range
    //#presumption(void saveFile(Weblog, String, String, long, InputStream, bool)): true
    //#presumption(void saveFile(Weblog, String, String, long, InputStream, bool)): init'ed(java.io.File.separator)
    //#presumption(void saveFile(Weblog, String, String, long, InputStream, bool)): java.lang.String:indexOf(...)@456 in range
    //#presumption(void saveFile(Weblog, String, String, long, InputStream, bool)): (int) (java.math.BigDecimal:doubleValue(...)@366*1024000) < size | canSave(...) == 0 | size + canSave(...) <= (int) (java.math.BigDecimal:doubleValue(...)@377*1024000)
    //#presumption(void saveFile(Weblog, String, String, long, InputStream, bool)): (int) (java.math.BigDecimal:doubleValue(...)@366*1024000) < size | canSave(...) == 0 | (int) (java.math.BigDecimal:doubleValue(...)@377*1024000) < size + canSave(...) | checkFileType(...) == 0 | java.lang.String:indexOf(...)@402 == -1 | java.lang.String:indexOf(...)@405 == java.lang.String:lastIndexOf(...)@405
    //#presumption(void saveFile(Weblog, String, String, long, InputStream, bool)): (int) (java.math.BigDecimal:doubleValue(...)@366*1024000) < size | canSave(...) == 0 | (int) (java.math.BigDecimal:doubleValue(...)@377*1024000) < size + canSave(...) | checkFileType(...) != 0
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.String:endsWith
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.io.File
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.io.File:isDirectory
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.io.File:listFiles
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.io.File:length
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:getDirSize
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.String:split
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.String:toLowerCase
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:getBooleanProperty
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:org.apache.roller.weblogger.util.RollerMessages:addError
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:getProperty
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.math.BigDecimal
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.math.BigDecimal:doubleValue
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:org.apache.commons.logging.Log:debug
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.math.BigDecimal:toString
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:org.apache.commons.lang.StringUtils:deleteWhitespace
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:org.apache.commons.lang.StringUtils:split
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.RuntimeException
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:getWeblogger
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:getPropertiesManager
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.ThreadLocal:get
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:javax.persistence.EntityManagerFactory:createEntityManager
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.ThreadLocal:set
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:javax.persistence.EntityManager:getTransaction
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:javax.persistence.EntityTransaction:isActive
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:javax.persistence.EntityTransaction:begin
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:javax.persistence.EntityManager:find
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:org.apache.roller.weblogger.pojos.RuntimeConfigProperty:getValue
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:org.apache.commons.logging.Log:warn
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.Boolean
    //#unanalyzed(void saveFile(Weblog, String, String, long, InputStream, bool)): Effects-of-calling:java.lang.Boolean:booleanValue
    //#test_vector(void saveFile(Weblog, String, String, long, InputStream, bool)): checkCanSave: {0}, {1}
    //#test_vector(void saveFile(Weblog, String, String, long, InputStream, bool)): java.io.File:exists(...)@180: {1}, {0}
    //#test_vector(void saveFile(Weblog, String, String, long, InputStream, bool)): java.io.InputStream:read(...)@195: {-1}, {-2_147_483_648..-2, 0..4_294_967_295}
    //#test_vector(void saveFile(Weblog, String, String, long, InputStream, bool)): java.lang.String:indexOf(...)@177: {-1}, {-2_147_483_648..-2, 0..4_294_967_295}
    //#test_vector(void saveFile(Weblog, String, String, long, InputStream, bool)): java.lang.String:startsWith(...)@163: {0}, {1}
        if(path.startsWith("/")) {
            savePath = path.substring(1);
        }
        
        // make sure we are allowed to save this file
        RollerMessages msgs = new RollerMessages();
    //#FileManagerImpl.java:168: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.util.RollerMessages()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: void saveFile(Weblog, String, String, long, InputStream, bool)
    //#    unanalyzed callee: void org.apache.roller.weblogger.util.RollerMessages()
        if (checkCanSave && !canSave(weblog, savePath, contentType, size, msgs)) {
            throw new FileIOException(msgs.toString());
    //#FileManagerImpl.java:170: ?conditional throw
    //#    canSave(...) != 0
    //#    severity: MEDIUM
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: void saveFile(Weblog, String, String, long, InputStream, bool)
    //#    basic block: bb_4
    //#    assertion: canSave(...) != 0
    //#    VN: canSave(...)
    //#    Expected: {-Inf..-1, 1..+Inf}
    //#    Bad: {0}
    //#    Attribs:  Int  Bad singleton  Bad overlaps +/-1000  Bad > Exp
        }
        
        // make sure uploads area exists for this weblog
        File dirPath = this.getRealFile(weblog, null);
        
        // if we are saving into a subfolder, make sure it exists
        if(path.indexOf("/") != -1) {
            String subDir = path.substring(0, path.indexOf("/"));
            File subDirFile = new File(dirPath.getAbsolutePath() + File.separator + subDir);
            if(!subDirFile.exists()) {
                // directory doesn't exist yet, create it
                log.debug("Creating directory ["+subDir+"] automatically");
    //#FileManagerImpl.java:182: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: void saveFile(Weblog, String, String, long, InputStream, bool)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
                subDirFile.mkdir();
            }
        }
        
        // create File that we are about to save
        File saveFile = new File(dirPath.getAbsolutePath() + File.separator + savePath);
        
        byte[] buffer = new byte[8192];
        int bytesRead = 0;
    //#FileManagerImpl.java:191: Warning: unused assignment
    //#    unused assignment into bytesRead
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: void saveFile(Weblog, String, String, long, InputStream, bool)
    //#    Attribs:  Uncertain
        OutputStream bos = null;
        try {
            bos = new FileOutputStream(saveFile);
            while ((bytesRead = is.read(buffer, 0, 8192)) != -1) {
                bos.write(buffer, 0, bytesRead);
            }
            
            log.debug("The file has been written to ["+saveFile.getAbsolutePath()+"]");
    //#FileManagerImpl.java:199: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: void saveFile(Weblog, String, String, long, InputStream, bool)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
        } catch (Exception e) {
            throw new FileIOException("ERROR uploading file", e);
        } finally {
            try {
                bos.flush();
                bos.close();
            } catch (Exception ignored) {}
        }
        
        
    }
    //#FileManagerImpl.java:210: end of method: void org.apache.roller.weblogger.business.FileManagerImpl.saveFile(Weblog, String, String, long, InputStream, bool)
    
    
    /**
     * @see org.apache.roller.weblogger.model.FileManager#createDirectory(weblog, java.lang.String)
     */
    public void createDirectory(Weblog weblog, String path)
            throws FileNotFoundException, FilePathException, FileIOException {
        
        // get path to weblog's uploads area
        File weblogDir = this.getRealFile(weblog, null);
    //#FileManagerImpl.java:220: method: void org.apache.roller.weblogger.business.FileManagerImpl.createDirectory(Weblog, String)
    //#input(void createDirectory(Weblog, String)): "Failed to create directory ["._tainted
    //#input(void createDirectory(Weblog, String)): "Invalid path ["._tainted
    //#input(void createDirectory(Weblog, String)): "], "._tainted
    //#input(void createDirectory(Weblog, String)): "cannot read from path."._tainted
    //#input(void createDirectory(Weblog, String)): "directory doesn't exist."._tainted
    //#input(void createDirectory(Weblog, String)): "probably doesn't have needed parent directories."._tainted
    //#input(void createDirectory(Weblog, String)): "trying to get outside uploads dir."._tainted
    //#input(void createDirectory(Weblog, String)): "trying to use nested directories."._tainted
    //#input(void createDirectory(Weblog, String)): java.io.File.separator
    //#input(void createDirectory(Weblog, String)): java.io.File.separator._tainted
    //#input(void createDirectory(Weblog, String)): java.io.File.separatorChar
    //#input(void createDirectory(Weblog, String)): path
    //#input(void createDirectory(Weblog, String)): path._tainted
    //#input(void createDirectory(Weblog, String)): this
    //#input(void createDirectory(Weblog, String)): this.upload_dir
    //#input(void createDirectory(Weblog, String)): this.upload_dir._tainted
    //#input(void createDirectory(Weblog, String)): weblog
    //#pre[1] (void createDirectory(Weblog, String)): path != null
    //#pre[4] (void createDirectory(Weblog, String)): init'ed(this.upload_dir)
    //#pre[6] (void createDirectory(Weblog, String)): weblog != null
    //#presumption(void createDirectory(Weblog, String)): init'ed(java.io.File.separator)
    //#presumption(void createDirectory(Weblog, String)): java.io.File:getCanonicalPath(...)@243 != null
    //#presumption(void createDirectory(Weblog, String)): java.io.File:mkdir(...)@253 == 1
    //#presumption(void createDirectory(Weblog, String)): java.lang.String:indexOf(...)@227 == -1
    //#presumption(void createDirectory(Weblog, String)): java.lang.String:startsWith(...)@243 == 1
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.io.File
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(void createDirectory(Weblog, String)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#test_vector(void createDirectory(Weblog, String)): java.io.File:canRead(...)@236: {0}, {1}
    //#test_vector(void createDirectory(Weblog, String)): java.io.File:exists(...)@236: {0}, {1}
    //#test_vector(void createDirectory(Weblog, String)): java.io.File:isDirectory(...)@236: {0}, {1}
    //#test_vector(void createDirectory(Weblog, String)): java.lang.String:startsWith(...)@223: {0}, {1}
        
        String savePath = path;
        if(path.startsWith("/")) {
            savePath = path.substring(1);
        }
        
        if(savePath != null && savePath.indexOf('/') != -1) {
    //#FileManagerImpl.java:227: Warning: test always goes same way
    //#    test predetermined because savePath != null
    //#    severity: LOW
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: void createDirectory(Weblog, String)
    //#    from bb: bb_3
    //#    live edge: bb_3-->bb_4
    //#    tested vn: savePath == null
    //#    tested vn values: {0}
            throw new FilePathException("Invalid path ["+path+"], "+
                        "trying to use nested directories.");
        }
        
        // now construct path to new directory
        File dir = new File(weblogDir.getAbsolutePath() + File.separator + savePath);
        
        // check if it already exists
        if(dir.exists() && dir.isDirectory() && dir.canRead()) {
            // already exists, we don't need to do anything
            return;
        }
        
        try {
            // make sure someone isn't trying to sneek outside the uploads dir
            if(!dir.getCanonicalPath().startsWith(weblogDir.getCanonicalPath())) {
                throw new FilePathException("Invalid path ["+path+"], "+
                        "trying to get outside uploads dir.");
            }
        } catch (IOException ex) {
            // rethrow as FilePathException
            throw new FilePathException(ex);
        }
        
        // create it
        if(!dir.mkdir()) {
            // failed for some reason
            throw new FileIOException("Failed to create directory ["+path+"], "+
                    "probably doesn't have needed parent directories.");
        }
    }
    //#FileManagerImpl.java:258: end of method: void org.apache.roller.weblogger.business.FileManagerImpl.createDirectory(Weblog, String)
    
    
    /**
     * @see org.apache.roller.weblogger.model.FileManager#deleteFile(weblog, java.lang.String)
     */
    public void deleteFile(Weblog weblog, String path) 
            throws FileNotFoundException, FilePathException, FileIOException {
        
        // get path to delete file, checks that path exists and is readable
        File delFile = this.getRealFile(weblog, path);
    //#FileManagerImpl.java:268: method: void org.apache.roller.weblogger.business.FileManagerImpl.deleteFile(Weblog, String)
    //#input(void deleteFile(Weblog, String)): "Delete failed for ["._tainted
    //#input(void deleteFile(Weblog, String)): "Invalid path ["._tainted
    //#input(void deleteFile(Weblog, String)): "], "._tainted
    //#input(void deleteFile(Weblog, String)): "cannot read from path."._tainted
    //#input(void deleteFile(Weblog, String)): "directory doesn't exist."._tainted
    //#input(void deleteFile(Weblog, String)): "possibly a non-empty directory?"._tainted
    //#input(void deleteFile(Weblog, String)): "trying to get outside uploads dir."._tainted
    //#input(void deleteFile(Weblog, String)): "trying to use nested directories."._tainted
    //#input(void deleteFile(Weblog, String)): java.io.File.separator
    //#input(void deleteFile(Weblog, String)): java.io.File.separator._tainted
    //#input(void deleteFile(Weblog, String)): java.io.File.separatorChar
    //#input(void deleteFile(Weblog, String)): path
    //#input(void deleteFile(Weblog, String)): path._tainted
    //#input(void deleteFile(Weblog, String)): this
    //#input(void deleteFile(Weblog, String)): this.upload_dir
    //#input(void deleteFile(Weblog, String)): this.upload_dir._tainted
    //#input(void deleteFile(Weblog, String)): weblog
    //#pre[4] (void deleteFile(Weblog, String)): init'ed(this.upload_dir)
    //#pre[6] (void deleteFile(Weblog, String)): weblog != null
    //#presumption(void deleteFile(Weblog, String)): java.io.File:delete(...)@270 == 1
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.io.File
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(void deleteFile(Weblog, String)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
        
        if(!delFile.delete()) {
            throw new FileIOException("Delete failed for ["+path+"], "+
                    "possibly a non-empty directory?");
        }
    }
    //#FileManagerImpl.java:274: end of method: void org.apache.roller.weblogger.business.FileManagerImpl.deleteFile(Weblog, String)
    
    
    /**
     * @inheritDoc
     */
    public void deleteAllFiles(Weblog weblog) throws FileIOException {
        
        try {
            // get path to root folder
            File delFile = this.getRealFile(weblog, "/");
    //#FileManagerImpl.java:284: method: void org.apache.roller.weblogger.business.FileManagerImpl.deleteAllFiles(Weblog)
    //#input(void deleteAllFiles(Weblog)): "."._tainted
    //#input(void deleteAllFiles(Weblog)): "Invalid path ["._tainted
    //#input(void deleteAllFiles(Weblog)): "], "._tainted
    //#input(void deleteAllFiles(Weblog)): "cannot read from path."._tainted
    //#input(void deleteAllFiles(Weblog)): "directory doesn't exist."._tainted
    //#input(void deleteAllFiles(Weblog)): "trying to get outside uploads dir."._tainted
    //#input(void deleteAllFiles(Weblog)): "trying to use nested directories."._tainted
    //#input(void deleteAllFiles(Weblog)): java.io.File.separator
    //#input(void deleteAllFiles(Weblog)): java.io.File.separator._tainted
    //#input(void deleteAllFiles(Weblog)): java.io.File.separatorChar
    //#input(void deleteAllFiles(Weblog)): this
    //#input(void deleteAllFiles(Weblog)): this.upload_dir
    //#input(void deleteAllFiles(Weblog)): this.upload_dir._tainted
    //#input(void deleteAllFiles(Weblog)): weblog
    //#pre[2] (void deleteAllFiles(Weblog)): (soft) init'ed(this.upload_dir)
    //#pre[4] (void deleteAllFiles(Weblog)): (soft) weblog != null
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.io.File
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.io.File:isDirectory
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.io.File:listFiles
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:deleteAllFiles
    //#unanalyzed(void deleteAllFiles(Weblog)): Effects-of-calling:java.io.File:delete
            
            // delete folder and it's contents
            deleteAllFiles(delFile);
            
        } catch (FileNotFoundException ex) {
            // if it doesn't exist then we already have no files, so we're done
            return;
        } catch (FilePathException ex) {
            // should never happen when trying to get root folder
        }
    }
    //#FileManagerImpl.java:295: end of method: void org.apache.roller.weblogger.business.FileManagerImpl.deleteAllFiles(Weblog)
    
    
    // convenience method to delete a folder and all of it's contents.  called recursively
    private void deleteAllFiles(File dir) {
        
        // delete directory contents
        File[] dirFiles = dir.listFiles();
    //#FileManagerImpl.java:302: method: void org.apache.roller.weblogger.business.FileManagerImpl.deleteAllFiles(File)
    //#input(void deleteAllFiles(File)): dir
    //#input(void deleteAllFiles(File)): this
    //#pre[1] (void deleteAllFiles(File)): dir != null
    //#presumption(void deleteAllFiles(File)): dirFiles.length@302 <= 4_294_967_295
    //#unanalyzed(void deleteAllFiles(File)): Effects-of-calling:java.io.File:isDirectory
    //#unanalyzed(void deleteAllFiles(File)): Effects-of-calling:java.io.File:listFiles
    //#unanalyzed(void deleteAllFiles(File)): Effects-of-calling:deleteAllFiles
    //#unanalyzed(void deleteAllFiles(File)): Effects-of-calling:java.io.File:delete
    //#test_vector(void deleteAllFiles(File)): dirFiles.length@302: {0}, {1..4_294_967_295}
    //#test_vector(void deleteAllFiles(File)): java.io.File:isDirectory(...)@305: {0}, {1}
    //#test_vector(void deleteAllFiles(File)): java.io.File:listFiles(...)@302: Addr_Set{null}, Inverse{null}
        if(dirFiles != null && dirFiles.length > 0) {
            for( File file : dirFiles ) {
    //#FileManagerImpl.java:304: ?use of default init
    //#    init'ed(arr$[i$])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: void deleteAllFiles(File)
    //#    basic block: bb_5
    //#    assertion: init'ed(arr$[i$])
    //#    VN: arr$[i$]
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
                if(file.isDirectory()) {
    //#FileManagerImpl.java:305: ?!null dereference
    //#    file != null
    //#    severity: HIGH
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: void deleteAllFiles(File)
    //#    basic block: bb_5
    //#    assertion: file != null
    //#    VN: arr$[i$]
    //#    Expected: Inverse{null} or Invalid
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
                    // recursive call
                    deleteAllFiles(file);
                } else {
                    file.delete();
                }
            }
        }
        
        // delete directory itself
        dir.delete();
    }
    //#FileManagerImpl.java:316: end of method: void org.apache.roller.weblogger.business.FileManagerImpl.deleteAllFiles(File)
    
    
    /**
     * @see org.apache.roller.weblogger.model.FileManager#overQuota(weblog)
     */
    public boolean overQuota(Weblog weblog) {
        
        String maxDir = WebloggerRuntimeConfig.getProperty("uploads.dir.maxsize");
    //#FileManagerImpl.java:324: method: bool org.apache.roller.weblogger.business.FileManagerImpl.overQuota(Weblog)
    //#FileManagerImpl.java:324: Warning: suspicious precondition
    //#    the precondition for org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool overQuota(Weblog)
    //#    suspicious precondition index: [2]
    //#    Attribs:  Soft
    //#input(bool overQuota(Weblog)): "="._tainted
    //#input(bool overQuota(Weblog)): "Invalid path ["._tainted
    //#input(bool overQuota(Weblog)): "Trouble accessing property: "._tainted
    //#input(bool overQuota(Weblog)): "]"._tainted
    //#input(bool overQuota(Weblog)): "], "._tainted
    //#input(bool overQuota(Weblog)): "cannot read from path."._tainted
    //#input(bool overQuota(Weblog)): "directory doesn't exist."._tainted
    //#input(bool overQuota(Weblog)): "fetched property ["._tainted
    //#input(bool overQuota(Weblog)): "trying to get outside uploads dir."._tainted
    //#input(bool overQuota(Weblog)): "trying to use nested directories."._tainted
    //#input(bool overQuota(Weblog)): "uploads.dir.maxsize"._tainted
    //#input(bool overQuota(Weblog)): "uploads.file.maxsize"._tainted
    //#input(bool overQuota(Weblog)): java.io.File.separator
    //#input(bool overQuota(Weblog)): java.io.File.separator._tainted
    //#input(bool overQuota(Weblog)): java.io.File.separatorChar
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/GuiceWebloggerProvider.__Dispatch_Table.getWeblogger()Lorg/apache/roller/weblogger/business/Weblogger;
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[org/apache/roller/weblogger/business/PropertiesManager]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAPropertiesManagerImpl]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[others]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/PropertiesManager.__Dispatch_Table.getProperty(Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/RuntimeConfigProperty;
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerImpl]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/Weblogger]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[others]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/Weblogger.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.__Tag
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.__Tag
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy.__Tag
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy.threadLocalEntityManager
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerImpl.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[org/apache/roller/weblogger/business/GuiceWebloggerProvider]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerProvider]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[others]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/WebloggerProvider.__Dispatch_Table.getWeblogger()Lorg/apache/roller/weblogger/business/Weblogger;
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Descendant_Table[others]
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Dispatch_Table.load(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Object;
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/jpa/JPAPropertiesManagerImpl.__Dispatch_Table.getProperty(Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/RuntimeConfigProperty;
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(bool overQuota(Weblog)): org/apache/roller/weblogger/config/WebloggerRuntimeConfig.log
    //#input(bool overQuota(Weblog)): this
    //#input(bool overQuota(Weblog)): this.upload_dir
    //#input(bool overQuota(Weblog)): this.upload_dir._tainted
    //#input(bool overQuota(Weblog)): weblog
    //#output(bool overQuota(Weblog)): return_value
    //#pre[11] (bool overQuota(Weblog)): org/apache/roller/weblogger/config/WebloggerRuntimeConfig.log != null
    //#pre[13] (bool overQuota(Weblog)): init'ed(this.upload_dir)
    //#pre[15] (bool overQuota(Weblog)): weblog != null
    //#pre[1] (bool overQuota(Weblog)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider != null
    //#pre[2] (bool overQuota(Weblog)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag in {org/apache/roller/weblogger/business/GuiceWebloggerProvider, org/apache/roller/weblogger/business/WebloggerProvider}
    //#pre[3] (bool overQuota(Weblog)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance != null
    //#presumption(bool overQuota(Weblog)): (int) (java.math.BigDecimal:doubleValue(...)@329*1024000) in -9_223_372_036_854_775_808..18_446_744_073_709_551_615
    //#post(bool overQuota(Weblog)): init'ed(return_value)
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.io.File
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.io.File:isDirectory
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.io.File:listFiles
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.io.File:length
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:getDirSize
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:getWeblogger
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:getPropertiesManager
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:getProperty
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.ThreadLocal:get
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:javax.persistence.EntityManagerFactory:createEntityManager
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:java.lang.ThreadLocal:set
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:javax.persistence.EntityManager:getTransaction
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:javax.persistence.EntityTransaction:isActive
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:javax.persistence.EntityTransaction:begin
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:javax.persistence.EntityManager:find
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:org.apache.roller.weblogger.pojos.RuntimeConfigProperty:getValue
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:org.apache.commons.logging.Log:warn
    //#unanalyzed(bool overQuota(Weblog)): Effects-of-calling:org.apache.commons.logging.Log:debug
        String maxFile = WebloggerRuntimeConfig.getProperty("uploads.file.maxsize");
        BigDecimal maxDirSize = new BigDecimal(maxDir); // in megabytes
        BigDecimal maxFileSize = new BigDecimal(maxFile); // in megabytes
    //#FileManagerImpl.java:327: Warning: unused assignment
    //#    unused assignment into maxFileSize
    //#    severity: LOW
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool overQuota(Weblog)
        
        long maxDirBytes = (long)(1024000 * maxDirSize.doubleValue());
        
        try {
            File uploadsDir = this.getRealFile(weblog, null);
            long weblogDirSize = this.getDirSize(uploadsDir, true);
            
            return weblogDirSize > maxDirBytes;
        } catch (Exception ex) {
            // shouldn't ever happen, this means user's uploads dir is bad
            // rethrow as a runtime exception
            throw new RuntimeException(ex);
    //#FileManagerImpl.java:339: end of method: bool org.apache.roller.weblogger.business.FileManagerImpl.overQuota(Weblog)
        }
    }
    
    
    public void release() {
    }
    //#FileManagerImpl.java:345: method: void org.apache.roller.weblogger.business.FileManagerImpl.release()
    //#FileManagerImpl.java:345: end of method: void org.apache.roller.weblogger.business.FileManagerImpl.release()
    
    
    /**
     * Determine if file can be saved given current WebloggerConfig settings.
     */
    private boolean canSave(Weblog weblog, 
                           String path, 
                           String contentType,
                           long size, 
                           RollerMessages messages) {
        
        // first check, is uploading enabled?
        if(!WebloggerRuntimeConfig.getBooleanProperty("uploads.enabled")) {
    //#FileManagerImpl.java:358: method: bool org.apache.roller.weblogger.business.FileManagerImpl.canSave(Weblog, String, String, long, RollerMessages)
    //#FileManagerImpl.java:358: Warning: suspicious precondition
    //#    the precondition for org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    suspicious precondition index: [6]
    //#    Attribs:  Soft
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "="._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "Invalid path ["._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "Trouble accessing property: "._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "]"._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "], "._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "attempted save file size = "._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "cannot read from path."._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "directory doesn't exist."._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "fetched property ["._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "max allowed file size = "._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "trying to get outside uploads dir."._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "trying to use nested directories."._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "uploads.dir.maxsize"._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "uploads.enabled"._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "uploads.file.maxsize"._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "uploads.types.allowed"._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): "uploads.types.forbid"._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): contentType
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): contentType._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): java.io.File.separator
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): java.io.File.separator._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): java.io.File.separatorChar
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): log
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): messages
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/GuiceWebloggerProvider.__Dispatch_Table.getWeblogger()Lorg/apache/roller/weblogger/business/Weblogger;
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[org/apache/roller/weblogger/business/PropertiesManager]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAPropertiesManagerImpl]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[others]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/PropertiesManager.__Dispatch_Table.getProperty(Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/RuntimeConfigProperty;
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerImpl]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/Weblogger]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[others]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/Weblogger.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.__Tag
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.__Tag
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy.__Tag
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy.threadLocalEntityManager
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerImpl.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[org/apache/roller/weblogger/business/GuiceWebloggerProvider]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerProvider]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[others]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/WebloggerProvider.__Dispatch_Table.getWeblogger()Lorg/apache/roller/weblogger/business/Weblogger;
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Descendant_Table[others]
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Dispatch_Table.load(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Object;
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/jpa/JPAPropertiesManagerImpl.__Dispatch_Table.getProperty(Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/RuntimeConfigProperty;
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/config/WebloggerRuntimeConfig.log
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): path
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): size
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): this
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): this.upload_dir
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): this.upload_dir._tainted
    //#input(bool canSave(Weblog, String, String, long, RollerMessages)): weblog
    //#output(bool canSave(Weblog, String, String, long, RollerMessages)): return_value
    //#pre[15] (bool canSave(Weblog, String, String, long, RollerMessages)): org/apache/roller/weblogger/config/WebloggerRuntimeConfig.log != null
    //#pre[3] (bool canSave(Weblog, String, String, long, RollerMessages)): (soft) log != null
    //#pre[4] (bool canSave(Weblog, String, String, long, RollerMessages)): (soft) messages != null
    //#pre[5] (bool canSave(Weblog, String, String, long, RollerMessages)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider != null
    //#pre[6] (bool canSave(Weblog, String, String, long, RollerMessages)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag in {org/apache/roller/weblogger/business/GuiceWebloggerProvider, org/apache/roller/weblogger/business/WebloggerProvider}
    //#pre[7] (bool canSave(Weblog, String, String, long, RollerMessages)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance != null
    //#pre[16] (bool canSave(Weblog, String, String, long, RollerMessages)): (soft) path != null
    //#pre[19] (bool canSave(Weblog, String, String, long, RollerMessages)): (soft) init'ed(this.upload_dir)
    //#pre[21] (bool canSave(Weblog, String, String, long, RollerMessages)): (soft) weblog != null
    //#presumption(bool canSave(Weblog, String, String, long, RollerMessages)): (int) (java.math.BigDecimal:doubleValue(...)@366*1024000) in -2_147_483_648..4_294_967_295
    //#presumption(bool canSave(Weblog, String, String, long, RollerMessages)): (int) (java.math.BigDecimal:doubleValue(...)@377*1024000) in -9_223_372_036_854_775_808..18_446_744_073_709_551_615
    //#presumption(bool canSave(Weblog, String, String, long, RollerMessages)): allowFiles.length@394 <= 4_294_967_295
    //#presumption(bool canSave(Weblog, String, String, long, RollerMessages)): forbidFiles.length@395 <= 4_294_967_295
    //#post(bool canSave(Weblog, String, String, long, RollerMessages)): init'ed(return_value)
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.String:endsWith
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.io.File
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.io.File:isDirectory
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.io.File:listFiles
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.io.File:length
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:getDirSize
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.String:split
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.String:toLowerCase
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:getWeblogger
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:getPropertiesManager
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:getProperty
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.ThreadLocal:get
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:javax.persistence.EntityManagerFactory:createEntityManager
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.ThreadLocal:set
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:javax.persistence.EntityManager:getTransaction
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:javax.persistence.EntityTransaction:isActive
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:javax.persistence.EntityTransaction:begin
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:javax.persistence.EntityManager:find
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:org.apache.roller.weblogger.pojos.RuntimeConfigProperty:getValue
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:org.apache.commons.logging.Log:warn
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:org.apache.commons.logging.Log:debug
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.Boolean
    //#unanalyzed(bool canSave(Weblog, String, String, long, RollerMessages)): Effects-of-calling:java.lang.Boolean:booleanValue
    //#test_vector(bool canSave(Weblog, String, String, long, RollerMessages)): java.lang.String:indexOf(...)@402: {-1}, {-2_147_483_648..-2, 0..4_294_967_295}
            messages.addError("error.upload.disabled");
    //#FileManagerImpl.java:359: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.util.RollerMessages:addError(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: void org.apache.roller.weblogger.util.RollerMessages:addError(String)
            return false;
        }
        
        // second check, does upload exceed max size for file?
        BigDecimal maxFileMB = new BigDecimal(
                WebloggerRuntimeConfig.getProperty("uploads.file.maxsize"));
        int maxFileBytes = (int)(1024000 * maxFileMB.doubleValue());
        log.debug("max allowed file size = "+maxFileBytes);
    //#FileManagerImpl.java:367: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
        log.debug("attempted save file size = "+size);
    //#FileManagerImpl.java:368: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
        if (size > maxFileBytes) {
            messages.addError("error.upload.filemax", maxFileMB.toString());
    //#FileManagerImpl.java:370: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.util.RollerMessages:addError(String, String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: void org.apache.roller.weblogger.util.RollerMessages:addError(String, String)
            return false;
        }
        
        // third check, does file cause weblog to exceed quota?
        BigDecimal maxDirMB = new BigDecimal(
                WebloggerRuntimeConfig.getProperty("uploads.dir.maxsize"));
        long maxDirBytes = (long)(1024000 * maxDirMB.doubleValue());
        try {
            File uploadsDir = this.getRealFile(weblog, null);
            long userDirSize = getDirSize(uploadsDir, true);
            if (userDirSize + size > maxDirBytes) {
                messages.addError("error.upload.dirmax", maxDirMB.toString());
    //#FileManagerImpl.java:382: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.util.RollerMessages:addError(String, String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: void org.apache.roller.weblogger.util.RollerMessages:addError(String, String)
                return false;
            }
        } catch (Exception ex) {
            // shouldn't ever happen, means the weblogs uploads dir is bad somehow
            // rethrow as a runtime exception
            throw new RuntimeException(ex);
        }
        
        // fourth check, is upload type allowed?
        String allows = WebloggerRuntimeConfig.getProperty("uploads.types.allowed");
        String forbids = WebloggerRuntimeConfig.getProperty("uploads.types.forbid");
        String[] allowFiles = StringUtils.split(StringUtils.deleteWhitespace(allows), ",");
    //#FileManagerImpl.java:394: Warning: method not available
    //#    -- call on String org.apache.commons.lang.StringUtils:deleteWhitespace(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: String org.apache.commons.lang.StringUtils:deleteWhitespace(String)
    //#FileManagerImpl.java:394: Warning: method not available
    //#    -- call on String[] org.apache.commons.lang.StringUtils:split(String, String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: String[] org.apache.commons.lang.StringUtils:split(String, String)
        String[] forbidFiles = StringUtils.split(StringUtils.deleteWhitespace(forbids), ",");
    //#FileManagerImpl.java:395: Warning: method not available
    //#    -- call on String org.apache.commons.lang.StringUtils:deleteWhitespace(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: String org.apache.commons.lang.StringUtils:deleteWhitespace(String)
    //#FileManagerImpl.java:395: Warning: method not available
    //#    -- call on String[] org.apache.commons.lang.StringUtils:split(String, String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: String[] org.apache.commons.lang.StringUtils:split(String, String)
        if (!checkFileType(allowFiles, forbidFiles, path, contentType)) {
    //#FileManagerImpl.java:396: ?!precondition failure
    //#    org/apache/roller/weblogger/business/FileManagerImpl.checkFileType: (soft) allowFiles[0..4_294_967_295] != null
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    basic block: bb_10
    //#    assertion: (soft) undefined != null
    //#    callee: bool org/apache/roller/weblogger/business/FileManagerImpl.checkFileType(String[], String[], String, String)
    //#    callee assertion: (soft) allowFiles[0..4_294_967_295] != null
    //#    callee file: FileManagerImpl.java
    //#    callee precondition index: [3]
    //#    callee srcpos: 456
    //#    VN: undefined
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null, Invalid}
    //#    Attribs:  Ptr  null in Bad  Soft
    //#FileManagerImpl.java:396: ?!precondition failure
    //#    org/apache/roller/weblogger/business/FileManagerImpl.checkFileType: (soft) forbidFiles[0..4_294_967_295] != null
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    basic block: bb_10
    //#    assertion: (soft) undefined != null
    //#    callee: bool org/apache/roller/weblogger/business/FileManagerImpl.checkFileType(String[], String[], String, String)
    //#    callee assertion: (soft) forbidFiles[0..4_294_967_295] != null
    //#    callee file: FileManagerImpl.java
    //#    callee precondition index: [10]
    //#    callee srcpos: 456
    //#    VN: undefined
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null, Invalid}
    //#    Attribs:  Ptr  null in Bad  Soft
            messages.addError("error.upload.forbiddenFile", allows);
    //#FileManagerImpl.java:397: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.util.RollerMessages:addError(String, String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: void org.apache.roller.weblogger.util.RollerMessages:addError(String, String)
            return false;
        }
        
        // fifth check, is save path viable?
        if(path.indexOf("/") != -1) {
            // just make sure there is only 1 directory, we don't allow multi
            // level directory hierarchies right now
            if(path.lastIndexOf("/") != path.indexOf("/")) {
                messages.addError("error.upload.badPath");
    //#FileManagerImpl.java:406: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.util.RollerMessages:addError(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool canSave(Weblog, String, String, long, RollerMessages)
    //#    unanalyzed callee: void org.apache.roller.weblogger.util.RollerMessages:addError(String)
                return false;
            }
        }
        
        return true;
    //#FileManagerImpl.java:411: end of method: bool org.apache.roller.weblogger.business.FileManagerImpl.canSave(Weblog, String, String, long, RollerMessages)
    }
    
    
    /**
     * Get the size in bytes of given directory.
     *
     * Optionally works recursively counting subdirectories if they exist.
     */
    private long getDirSize(File dir, boolean recurse) {
        
        long size = 0;
    //#FileManagerImpl.java:422: method: long org.apache.roller.weblogger.business.FileManagerImpl.getDirSize(File, bool)
    //#input(long getDirSize(File, bool)): dir
    //#input(long getDirSize(File, bool)): recurse
    //#input(long getDirSize(File, bool)): this
    //#output(long getDirSize(File, bool)): return_value
    //#pre[1] (long getDirSize(File, bool)): dir != null
    //#presumption(long getDirSize(File, bool)): files.length@424 <= 4_294_967_295
    //#presumption(long getDirSize(File, bool)): java.io.File:listFiles(...)@424 != null
    //#post(long getDirSize(File, bool)): init'ed(return_value)
    //#unanalyzed(long getDirSize(File, bool)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(long getDirSize(File, bool)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(long getDirSize(File, bool)): Effects-of-calling:java.io.File:isDirectory
    //#unanalyzed(long getDirSize(File, bool)): Effects-of-calling:java.io.File:listFiles
    //#unanalyzed(long getDirSize(File, bool)): Effects-of-calling:java.io.File:length
    //#unanalyzed(long getDirSize(File, bool)): Effects-of-calling:getDirSize
    //#test_vector(long getDirSize(File, bool)): recurse: {0}, {1}
    //#test_vector(long getDirSize(File, bool)): java.io.File:canRead(...)@423: {0}, {1}
    //#test_vector(long getDirSize(File, bool)): java.io.File:exists(...)@423: {0}, {1}
    //#test_vector(long getDirSize(File, bool)): java.io.File:isDirectory(...)@423: {0}, {1}
    //#test_vector(long getDirSize(File, bool)): java.io.File:isDirectory(...)@427: {1}, {0}
        if(dir.exists() && dir.isDirectory() && dir.canRead()) {
            File[] files = dir.listFiles();
            long dirSize = 0l;
            for (int i=0; i < files.length; i++) {
                if (!files[i].isDirectory()) {
    //#FileManagerImpl.java:427: ?use of default init
    //#    init'ed(files[i])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: long getDirSize(File, bool)
    //#    basic block: bb_6
    //#    assertion: init'ed(files[i])
    //#    VN: files[i]
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    //#FileManagerImpl.java:427: ?!null dereference
    //#    files[i] != null
    //#    severity: HIGH
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: long getDirSize(File, bool)
    //#    basic block: bb_6
    //#    assertion: files[i] != null
    //#    VN: files[i]
    //#    Expected: Inverse{null} or Invalid
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
                    dirSize += files[i].length();
    //#FileManagerImpl.java:428: ?overflow
    //#    dirSize + java/io/File:length(...) in -9_223_372_036_854_775_808..18_446_744_073_709_551_615
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: long getDirSize(File, bool)
    //#    basic block: bb_7
    //#    assertion: dirSize + java/io/File:length(...) in -9_223_372_036_854_775_808..18_446_744_073_709_551_615
    //#    VN: java.io.File:length(...)@428 + dirSize
    //#    Expected: {-9_223_372_036_854_775_808..18_446_744_073_709_551_615, Invalid}
    //#    Bad: {-18_446_744_073_709_551_616..-9_223_372_036_854_775_809, 18_446_744_073_709_551_616..36_893_488_147_419_103_230}
    //#    Attribs:  Int  Bad < Exp  Bad > Exp
                } else if(recurse) {
                    // count a subdirectory
                    dirSize += getDirSize(files[i], recurse);
    //#FileManagerImpl.java:431: ?overflow
    //#    dirSize + getDirSize(...) in -9_223_372_036_854_775_808..18_446_744_073_709_551_615
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: long getDirSize(File, bool)
    //#    basic block: bb_9
    //#    assertion: dirSize + getDirSize(...) in -9_223_372_036_854_775_808..18_446_744_073_709_551_615
    //#    VN: return_value + dirSize
    //#    Expected: {-9_223_372_036_854_775_808..18_446_744_073_709_551_615, Invalid}
    //#    Bad: {-18_446_744_073_709_551_616..-9_223_372_036_854_775_809, 18_446_744_073_709_551_616..36_893_488_147_419_103_230}
    //#    Attribs:  Int  Bad < Exp  Bad > Exp
                }
            }
            size += dirSize;
        }
        
        return size;
    //#FileManagerImpl.java:437: end of method: long org.apache.roller.weblogger.business.FileManagerImpl.getDirSize(File, bool)
    }
    
    
    /**
     * Return true if file is allowed to be uplaoded given specified allowed and
     * forbidden file types.
     */
    private boolean checkFileType(String[] allowFiles, String[] forbidFiles,
                                  String fileName, String contentType) {
        
        // TODO: Atom Publushing Protocol figure out how to handle file
        // allow/forbid using contentType.
        // TEMPORARY SOLUTION: In the allow/forbid lists we will continue to
        // allow user to specify file extensions (e.g. gif, png, jpeg) but will
        // now also allow them to specify content-type rules (e.g. */*, image/*,
        // text/xml, etc.).
        
        // if content type is invalid, reject file
        if (contentType == null || contentType.indexOf("/") == -1)  {
    //#FileManagerImpl.java:456: method: bool org.apache.roller.weblogger.business.FileManagerImpl.checkFileType(String[], String[], String, String)
    //#input(bool checkFileType(String[], String[], String, String)): allowFiles
    //#input(bool checkFileType(String[], String[], String, String)): allowFiles.length
    //#input(bool checkFileType(String[], String[], String, String)): allowFiles[0..4_294_967_295]
    //#input(bool checkFileType(String[], String[], String, String)): allowFiles[0..4_294_967_295]._tainted
    //#input(bool checkFileType(String[], String[], String, String)): contentType
    //#input(bool checkFileType(String[], String[], String, String)): contentType._tainted
    //#input(bool checkFileType(String[], String[], String, String)): fileName
    //#input(bool checkFileType(String[], String[], String, String)): forbidFiles
    //#input(bool checkFileType(String[], String[], String, String)): forbidFiles.length
    //#input(bool checkFileType(String[], String[], String, String)): forbidFiles[0..4_294_967_295]
    //#input(bool checkFileType(String[], String[], String, String)): forbidFiles[0..4_294_967_295]._tainted
    //#input(bool checkFileType(String[], String[], String, String)): this
    //#output(bool checkFileType(String[], String[], String, String)): return_value
    //#pre[2] (bool checkFileType(String[], String[], String, String)): (soft) allowFiles.length <= 4_294_967_295
    //#pre[3] (bool checkFileType(String[], String[], String, String)): (soft) allowFiles[0..4_294_967_295] != null
    //#pre[7] (bool checkFileType(String[], String[], String, String)): (soft) fileName != null
    //#pre[9] (bool checkFileType(String[], String[], String, String)): (soft) forbidFiles.length <= 4_294_967_295
    //#pre[10] (bool checkFileType(String[], String[], String, String)): (soft) forbidFiles[0..4_294_967_295] != null
    //#post(bool checkFileType(String[], String[], String, String)): init'ed(return_value)
    //#unanalyzed(bool checkFileType(String[], String[], String, String)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(bool checkFileType(String[], String[], String, String)): Effects-of-calling:java.lang.String:split
    //#test_vector(bool checkFileType(String[], String[], String, String)): allowFiles: Inverse{null}, Addr_Set{null}
    //#test_vector(bool checkFileType(String[], String[], String, String)): allowFiles.length: {1..4_294_967_295}, {0}
    //#test_vector(bool checkFileType(String[], String[], String, String)): contentType: Addr_Set{null}, Inverse{null}
    //#test_vector(bool checkFileType(String[], String[], String, String)): forbidFiles: Addr_Set{null}, Inverse{null}
    //#test_vector(bool checkFileType(String[], String[], String, String)): forbidFiles.length: {0}, {1..4_294_967_295}
    //#test_vector(bool checkFileType(String[], String[], String, String)): java.lang.String:endsWith(...)@476: {0}, {1}
    //#test_vector(bool checkFileType(String[], String[], String, String)): java.lang.String:endsWith(...)@503: {0}, {1}
    //#test_vector(bool checkFileType(String[], String[], String, String)): java.lang.String:indexOf(...)@456: {-2_147_483_648..-2, 0..4_294_967_295}, {-1}
            return false;
        }
        
        // default to false
        boolean allowFile = false;
        
        // if this person hasn't listed any allows, then assume they want
        // to allow *all* filetypes, except those listed under forbid
        if(allowFiles == null || allowFiles.length < 1) {
            allowFile = true;
        }
        
        // First check against what is ALLOWED
        
        // check file against allowed file extensions
        if (allowFiles != null && allowFiles.length > 0) {
            for (int y=0; y<allowFiles.length; y++) {
                // oops, this allowed rule is a content-type, skip it
                if (allowFiles[y].indexOf("/") != -1) continue;
                if (fileName.toLowerCase().endsWith(
                        allowFiles[y].toLowerCase())) {
                    allowFile = true;
                    break;
                }
            }
        }
        
        // check file against allowed contentTypes
        if (allowFiles != null && allowFiles.length > 0) {
            for (int y=0; y<allowFiles.length; y++) {
                // oops, this allowed rule is NOT a content-type, skip it
                if (allowFiles[y].indexOf("/") == -1) continue;
                if (matchContentType(allowFiles[y], contentType)) {
                    allowFile = true;
                    break;
                }
            }
        }
        
        // First check against what is FORBIDDEN
        
        // check file against forbidden file extensions, overrides any allows
        if (forbidFiles != null && forbidFiles.length > 0) {
            for (int x=0; x<forbidFiles.length; x++) {
                // oops, this forbid rule is a content-type, skip it
                if (forbidFiles[x].indexOf("/") != -1) continue;
                if (fileName.toLowerCase().endsWith(
                        forbidFiles[x].toLowerCase())) {
                    allowFile = false;
                    break;
                }
            }
        }
        
        
        // check file against forbidden contentTypes, overrides any allows
        if (forbidFiles != null && forbidFiles.length > 0) {
            for (int x=0; x<forbidFiles.length; x++) {
                // oops, this forbid rule is NOT a content-type, skip it
                if (forbidFiles[x].indexOf("/") == -1) continue;
                if (matchContentType(forbidFiles[x], contentType)) {
                    allowFile = false;
                    break;
                }
            }
        }
        
        return allowFile;
    //#FileManagerImpl.java:524: end of method: bool org.apache.roller.weblogger.business.FileManagerImpl.checkFileType(String[], String[], String, String)
    }
    
    
    /**
     * Super simple contentType range rule matching
     */
    private boolean matchContentType(String rangeRule, String contentType) {
        if (rangeRule.equals("*/*")) return true;
    //#FileManagerImpl.java:532: method: bool org.apache.roller.weblogger.business.FileManagerImpl.matchContentType(String, String)
    //#input(bool matchContentType(String, String)): contentType
    //#input(bool matchContentType(String, String)): contentType._tainted
    //#input(bool matchContentType(String, String)): rangeRule
    //#input(bool matchContentType(String, String)): rangeRule._tainted
    //#output(bool matchContentType(String, String)): return_value
    //#pre[3] (bool matchContentType(String, String)): rangeRule != null
    //#pre[1] (bool matchContentType(String, String)): (soft) contentType != null
    //#post(bool matchContentType(String, String)): init'ed(return_value)
    //#test_vector(bool matchContentType(String, String)): java.lang.String:equals(...)@532: {0}, {1}
    //#test_vector(bool matchContentType(String, String)): java.lang.String:equals(...)@533: {0}, {1}
    //#test_vector(bool matchContentType(String, String)): java.lang.String:equals(...)@536: {0}, {1}
        if (rangeRule.equals(contentType)) return true;
        String ruleParts[] = rangeRule.split("/");
        String typeParts[] = contentType.split("/");
        if (ruleParts[0].equals(typeParts[0]) && ruleParts[1].equals("*")) 
    //#FileManagerImpl.java:536: ?use of default init
    //#    init'ed(ruleParts.length)
    //#    severity: LOW
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool matchContentType(String, String)
    //#    basic block: bb_5
    //#    assertion: init'ed(ruleParts.length)
    //#    VN: undefined
    //#    Expected: {-Inf..+Inf}
    //#    Bad: {Invalid}
    //#    Attribs:  Int  Bad only invalid
    //#FileManagerImpl.java:536: ?use of default init
    //#    init'ed(typeParts.length)
    //#    severity: LOW
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool matchContentType(String, String)
    //#    basic block: bb_5
    //#    assertion: init'ed(typeParts.length)
    //#    VN: undefined
    //#    Expected: {-Inf..+Inf}
    //#    Bad: {Invalid}
    //#    Attribs:  Int  Bad only invalid
    //#FileManagerImpl.java:536: ?use of default init
    //#    init'ed(ruleParts[0])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool matchContentType(String, String)
    //#    basic block: bb_5
    //#    assertion: init'ed(ruleParts[0])
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    //#FileManagerImpl.java:536: ?null dereference
    //#    not_init'ed(ruleParts[0])
    //#    severity: MEDIUM
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool matchContentType(String, String)
    //#    basic block: bb_5
    //#    assertion: not_init'ed(ruleParts[0])
    //#    VN: undefined
    //#    Expected: Inverse{null} or Invalid
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#FileManagerImpl.java:536: ?use of default init
    //#    init'ed(typeParts[0])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool matchContentType(String, String)
    //#    basic block: bb_5
    //#    assertion: init'ed(typeParts[0])
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    //#FileManagerImpl.java:536: ?use of default init
    //#    init'ed(ruleParts.length)
    //#    severity: LOW
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool matchContentType(String, String)
    //#    basic block: bb_6
    //#    assertion: init'ed(ruleParts.length)
    //#    VN: undefined
    //#    Expected: {-Inf..+Inf}
    //#    Bad: {Invalid}
    //#    Attribs:  Int  Bad only invalid
    //#FileManagerImpl.java:536: ?!array index out of bounds
    //#    ruleParts.length >= 2
    //#    severity: HIGH
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool matchContentType(String, String)
    //#    basic block: bb_6
    //#    assertion: ruleParts.length >= 2
    //#    VN: undefined - 1
    //#    Expected: {1..+Inf}
    //#    Bad: {-1}
    //#    Attribs:  Int  Bad singleton  Bad overlaps +/-1000  Bad < Exp
    //#FileManagerImpl.java:536: ?use of default init
    //#    init'ed(ruleParts[1])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool matchContentType(String, String)
    //#    basic block: bb_6
    //#    assertion: init'ed(ruleParts[1])
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    //#FileManagerImpl.java:536: ?null dereference
    //#    not_init'ed(ruleParts[1])
    //#    severity: MEDIUM
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: bool matchContentType(String, String)
    //#    basic block: bb_6
    //#    assertion: not_init'ed(ruleParts[1])
    //#    VN: undefined
    //#    Expected: Inverse{null} or Invalid
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
            return true;
        
        return false;
    //#FileManagerImpl.java:539: end of method: bool org.apache.roller.weblogger.business.FileManagerImpl.matchContentType(String, String)
    }
    
    
    /**
     * Construct the full real path to a resource in a weblog's uploads area.
     */
    private File getRealFile(Weblog weblog, String path) 
            throws FileNotFoundException, FilePathException {
        
        // make sure uploads area exists for this weblog
        File weblogDir = new File(this.upload_dir + weblog.getHandle());
    //#FileManagerImpl.java:550: method: File org.apache.roller.weblogger.business.FileManagerImpl.getRealFile(Weblog, String)
    //#FileManagerImpl.java:550: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.Weblog:getHandle()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl
    //#    method: File getRealFile(Weblog, String)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.Weblog:getHandle()
    //#input(File getRealFile(Weblog, String)): "Invalid path ["._tainted
    //#input(File getRealFile(Weblog, String)): "], "._tainted
    //#input(File getRealFile(Weblog, String)): "cannot read from path."._tainted
    //#input(File getRealFile(Weblog, String)): "directory doesn't exist."._tainted
    //#input(File getRealFile(Weblog, String)): "trying to get outside uploads dir."._tainted
    //#input(File getRealFile(Weblog, String)): "trying to use nested directories."._tainted
    //#input(File getRealFile(Weblog, String)): java.io.File.separator
    //#input(File getRealFile(Weblog, String)): java.io.File.separator._tainted
    //#input(File getRealFile(Weblog, String)): java.io.File.separatorChar
    //#input(File getRealFile(Weblog, String)): path
    //#input(File getRealFile(Weblog, String)): path._tainted
    //#input(File getRealFile(Weblog, String)): this
    //#input(File getRealFile(Weblog, String)): this.upload_dir
    //#input(File getRealFile(Weblog, String)): this.upload_dir._tainted
    //#input(File getRealFile(Weblog, String)): weblog
    //#output(File getRealFile(Weblog, String)): new File(getRealFile#6) num objects
    //#output(File getRealFile(Weblog, String)): return_value
    //#new obj(File getRealFile(Weblog, String)): new File(getRealFile#6)
    //#pre[4] (File getRealFile(Weblog, String)): init'ed(this.upload_dir)
    //#pre[6] (File getRealFile(Weblog, String)): weblog != null
    //#presumption(File getRealFile(Weblog, String)): init'ed(java.io.File.separator)
    //#presumption(File getRealFile(Weblog, String)): init'ed(java.io.File.separatorChar)
    //#presumption(File getRealFile(Weblog, String)): java.io.File:canRead(...)@584 == 1
    //#presumption(File getRealFile(Weblog, String)): java.io.File:exists(...)@581 == 1
    //#presumption(File getRealFile(Weblog, String)): java.io.File:getCanonicalPath(...)@591 != null
    //#presumption(File getRealFile(Weblog, String)): java.lang.String:indexOf(...)@563 - java.lang.String:lastIndexOf(...)@563 in 0..6_442_450_943
    //#presumption(File getRealFile(Weblog, String)): java.lang.String:startsWith(...)@591 == 1
    //#post(File getRealFile(Weblog, String)): return_value == &new File(getRealFile#6)
    //#post(File getRealFile(Weblog, String)): new File(getRealFile#6) num objects == 1
    //#unanalyzed(File getRealFile(Weblog, String)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(File getRealFile(Weblog, String)): Effects-of-calling:org.apache.roller.RollerException
    //#test_vector(File getRealFile(Weblog, String)): path: Addr_Set{null}, Inverse{null}
    //#test_vector(File getRealFile(Weblog, String)): java.io.File:exists(...)@551: {1}, {0}
    //#test_vector(File getRealFile(Weblog, String)): java.lang.String:startsWith(...)@557: {0}, {1}
        if(!weblogDir.exists()) {
            weblogDir.mkdirs();
        }
        
        // crop leading slash if it exists
        String relPath = path;
        if(path != null && path.startsWith("/")) {
            relPath = path.substring(1);
        }
        
        // we only allow a single level of directories right now, so make
        // sure that the path doesn't try to go multiple levels
        if(relPath != null && (relPath.lastIndexOf('/') > relPath.indexOf('/'))) {
            throw new FilePathException("Invalid path ["+path+"], "+
                    "trying to use nested directories.");
        }
        
        // convert "/" to filesystem specific file separator
        if(relPath != null) {
            relPath = relPath.replace('/', File.separatorChar);
        }
        
        // now form the absolute path
        String filePath = weblogDir.getAbsolutePath();
        if(relPath != null) {
            filePath += File.separator + relPath;
        }
        
        // make sure path exists and is readable
        File file = new File(filePath);
        if(!file.exists()) {
            throw new FileNotFoundException("Invalid path ["+path+"], "+
                    "directory doesn't exist.");
        } else if(!file.canRead()) {
            throw new FilePathException("Invalid path ["+path+"], "+
                    "cannot read from path.");
        }
        
        try {
            // make sure someone isn't trying to sneek outside the uploads dir
            if(!file.getCanonicalPath().startsWith(weblogDir.getCanonicalPath())) {
                throw new FilePathException("Invalid path ["+path+"], "+
                        "trying to get outside uploads dir.");
            }
        } catch (IOException ex) {
            // rethrow as FilePathException
            throw new FilePathException(ex);
        }
        
        return file;
    //#FileManagerImpl.java:600: end of method: File org.apache.roller.weblogger.business.FileManagerImpl.getRealFile(Weblog, String)
    }
    
    
    /**
     * A FileManagerImpl specific implementation of a ThemeResource.
     *
     * ThemeResources from the FileManagerImpl are backed by a java.io.File
     * object which represents the resource on a filesystem.
     *
     * This class is internal to the FileManagerImpl class because there should 
     * not be any external classes which need to construct their own instances
     * of this class.
     */
    class WeblogResourceFile implements ThemeResource {
        
        // the physical java.io.File backing this resource
        private File resourceFile = null;
        
        // the relative path of the resource within the weblog's uploads area
        private String relativePath = null;
        
        // the weblog the resource is attached to
        private Weblog weblog = null;
        
        
        public WeblogResourceFile(Weblog weblog, String path, File file) {
    //#FileManagerImpl.java:626: method: void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): Param_1
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): file
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): path
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): this
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): weblog
    //#output(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): this.relativePath
    //#output(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): this.resourceFile
    //#output(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): this.this$0
    //#output(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): this.weblog
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): this.relativePath == path
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): init'ed(this.relativePath)
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): this.resourceFile == file
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): init'ed(this.resourceFile)
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): this.this$0 == Param_1
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): init'ed(this.this$0)
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): this.weblog == weblog
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)): init'ed(this.weblog)
            this.weblog = weblog;
            relativePath = path;
            resourceFile = file;
        }
    //#FileManagerImpl.java:630: end of method: void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile(FileManagerImpl, Weblog, String, File)
        
        public Weblog getWeblog() {
            return weblog;
    //#FileManagerImpl.java:633: method: Weblog org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getWeblog()
    //#input(Weblog getWeblog()): this
    //#input(Weblog getWeblog()): this.weblog
    //#output(Weblog getWeblog()): return_value
    //#pre[2] (Weblog getWeblog()): init'ed(this.weblog)
    //#post(Weblog getWeblog()): return_value == this.weblog
    //#post(Weblog getWeblog()): init'ed(return_value)
    //#FileManagerImpl.java:633: end of method: Weblog org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getWeblog()
        }
        
        public ThemeResource[] getChildren() {
            
            if(!resourceFile.isDirectory()) {
    //#FileManagerImpl.java:638: method: ThemeResource[] org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getChildren()
    //#input(ThemeResource[] getChildren()): "."._tainted
    //#input(ThemeResource[] getChildren()): this
    //#input(ThemeResource[] getChildren()): this.relativePath
    //#input(ThemeResource[] getChildren()): this.relativePath._tainted
    //#input(ThemeResource[] getChildren()): this.resourceFile
    //#input(ThemeResource[] getChildren()): this.this$0
    //#input(ThemeResource[] getChildren()): this.weblog
    //#output(ThemeResource[] getChildren()): java.lang.StringBuilder:toString(...)._tainted
    //#output(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4) num objects
    //#output(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4).__Tag
    //#output(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4).relativePath
    //#output(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4).resourceFile
    //#output(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4).this$0
    //#output(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4).weblog
    //#output(ThemeResource[] getChildren()): new ThemeResource[](getChildren#2) num objects
    //#output(ThemeResource[] getChildren()): new ThemeResource[](getChildren#2).length
    //#output(ThemeResource[] getChildren()): new ThemeResource[](getChildren#2)[0..4_294_967_295]
    //#output(ThemeResource[] getChildren()): return_value
    //#new obj(ThemeResource[] getChildren()): java.lang.StringBuilder:toString(...)
    //#new obj(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4)
    //#new obj(ThemeResource[] getChildren()): new ThemeResource[](getChildren#2)
    //#pre[4] (ThemeResource[] getChildren()): this.resourceFile != null
    //#pre[2] (ThemeResource[] getChildren()): (soft) init'ed(this.relativePath)
    //#pre[6] (ThemeResource[] getChildren()): (soft) init'ed(this.weblog)
    //#presumption(ThemeResource[] getChildren()): dirFiles.length@643 <= 4_294_967_295
    //#presumption(ThemeResource[] getChildren()): java.io.File:listFiles(...)@643 != null
    //#post(ThemeResource[] getChildren()): init'ed(java.lang.StringBuilder:toString(...)._tainted)
    //#post(ThemeResource[] getChildren()): return_value in Addr_Set{null,&new ThemeResource[](getChildren#2)}
    //#post(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4) num objects <= 4_294_967_295
    //#post(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4).__Tag == org/apache/roller/weblogger/business/FileManagerImpl$WeblogResourceFile
    //#post(ThemeResource[] getChildren()): possibly_updated(new FileManagerImpl$WeblogResourceFile(getChildren#4).relativePath)
    //#post(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4).resourceFile == null
    //#post(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4).this$0 == this.this$0
    //#post(ThemeResource[] getChildren()): init'ed(new FileManagerImpl$WeblogResourceFile(getChildren#4).this$0)
    //#post(ThemeResource[] getChildren()): new FileManagerImpl$WeblogResourceFile(getChildren#4).weblog == this.weblog
    //#post(ThemeResource[] getChildren()): (soft) init'ed(new FileManagerImpl$WeblogResourceFile(getChildren#4).weblog)
    //#post(ThemeResource[] getChildren()): new ThemeResource[](getChildren#2) num objects <= 1
    //#post(ThemeResource[] getChildren()): (soft) new ThemeResource[](getChildren#2).length <= 4_294_967_295
    //#post(ThemeResource[] getChildren()): possibly_updated(new ThemeResource[](getChildren#2)[0..4_294_967_295])
    //#test_vector(ThemeResource[] getChildren()): this.relativePath: Addr_Set{null}, Inverse{null}
    //#test_vector(ThemeResource[] getChildren()): java.io.File:isDirectory(...)@638: {1}, {0}
    //#test_vector(ThemeResource[] getChildren()): java.lang.String:equals(...)@653: {1}, {0}
                return null;
            }
            
            // we only want files, no directories
            File[] dirFiles = resourceFile.listFiles(new FileFilter() {
    //#FileManagerImpl.java:643: method: void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1.org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1(FileManagerImpl$WeblogResourceFile)
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1(FileManagerImpl$WeblogResourceFile)): Param_1
    //#input(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1(FileManagerImpl$WeblogResourceFile)): this
    //#output(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1(FileManagerImpl$WeblogResourceFile)): this.this$1
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1(FileManagerImpl$WeblogResourceFile)): this.this$1 == Param_1
    //#post(void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1(FileManagerImpl$WeblogResourceFile)): init'ed(this.this$1)
    //#FileManagerImpl.java:643: end of method: void org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1.org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1(FileManagerImpl$WeblogResourceFile)
                public boolean accept(File f) {
                    return (f != null) ? f.isFile() : false;
    //#FileManagerImpl.java:645: method: bool org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1.accept(File)
    //#input(bool accept(File)): f
    //#output(bool accept(File)): return_value
    //#post(bool accept(File)): init'ed(return_value)
    //#FileManagerImpl.java:645: end of method: bool org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1.accept(File)
                }
            });
            
            // convert Files into ThemeResources
            ThemeResource[] resources = new ThemeResource[dirFiles.length];
            for(int i=0; i < dirFiles.length; i++) {
                String filePath = dirFiles[i].getName();
    //#FileManagerImpl.java:652: ?use of default init
    //#    init'ed(dirFiles[i])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile
    //#    method: ThemeResource[] getChildren()
    //#    basic block: bb_5
    //#    assertion: init'ed(dirFiles[i])
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    //#FileManagerImpl.java:652: ?null dereference
    //#    not_init'ed(dirFiles[i])
    //#    severity: MEDIUM
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile
    //#    method: ThemeResource[] getChildren()
    //#    basic block: bb_5
    //#    assertion: not_init'ed(dirFiles[i])
    //#    VN: undefined
    //#    Expected: Inverse{null} or Invalid
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
                if(relativePath != null && !relativePath.trim().equals("")) {
                    filePath = relativePath + "/" + filePath;
                }
                
                resources[i] = new WeblogResourceFile(weblog, filePath, dirFiles[i]);
    //#FileManagerImpl.java:657: ?use of default init
    //#    init'ed(dirFiles[i])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile
    //#    method: ThemeResource[] getChildren()
    //#    basic block: bb_8
    //#    assertion: init'ed(dirFiles[i])
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
            }
            
            return resources;
    //#FileManagerImpl.java:660: end of method: ThemeResource[] org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getChildren()
        }
        
        public String getName() {
            return resourceFile.getName();
    //#FileManagerImpl.java:664: method: String org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getName()
    //#input(String getName()): this
    //#input(String getName()): this.resourceFile
    //#output(String getName()): return_value
    //#pre[2] (String getName()): this.resourceFile != null
    //#post(String getName()): init'ed(return_value)
    //#FileManagerImpl.java:664: end of method: String org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getName()
        }
        
        public String getPath() {
            return relativePath;
    //#FileManagerImpl.java:668: method: String org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getPath()
    //#input(String getPath()): this
    //#input(String getPath()): this.relativePath
    //#output(String getPath()): return_value
    //#pre[2] (String getPath()): init'ed(this.relativePath)
    //#post(String getPath()): return_value == this.relativePath
    //#post(String getPath()): init'ed(return_value)
    //#FileManagerImpl.java:668: end of method: String org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getPath()
        }
        
        public long getLastModified() {
            return resourceFile.lastModified();
    //#FileManagerImpl.java:672: method: long org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getLastModified()
    //#input(long getLastModified()): this
    //#input(long getLastModified()): this.resourceFile
    //#output(long getLastModified()): return_value
    //#pre[2] (long getLastModified()): this.resourceFile != null
    //#post(long getLastModified()): init'ed(return_value)
    //#FileManagerImpl.java:672: end of method: long org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getLastModified()
        }
        
        public long getLength() {
            return resourceFile.length();
    //#FileManagerImpl.java:676: method: long org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getLength()
    //#input(long getLength()): this
    //#input(long getLength()): this.resourceFile
    //#output(long getLength()): return_value
    //#pre[2] (long getLength()): this.resourceFile != null
    //#post(long getLength()): init'ed(return_value)
    //#FileManagerImpl.java:676: end of method: long org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getLength()
        }
        
        public boolean isDirectory() {
            return resourceFile.isDirectory();
    //#FileManagerImpl.java:680: method: bool org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.isDirectory()
    //#input(bool isDirectory()): this
    //#input(bool isDirectory()): this.resourceFile
    //#output(bool isDirectory()): return_value
    //#pre[2] (bool isDirectory()): this.resourceFile != null
    //#post(bool isDirectory()): init'ed(return_value)
    //#FileManagerImpl.java:680: end of method: bool org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.isDirectory()
        }
        
        public boolean isFile() {
            return resourceFile.isFile();
    //#FileManagerImpl.java:684: method: bool org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.isFile()
    //#input(bool isFile()): this
    //#input(bool isFile()): this.resourceFile
    //#output(bool isFile()): return_value
    //#pre[2] (bool isFile()): this.resourceFile != null
    //#post(bool isFile()): init'ed(return_value)
    //#FileManagerImpl.java:684: end of method: bool org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.isFile()
        }
        
        public InputStream getInputStream() {
            try {
                return new FileInputStream(resourceFile);
    //#FileManagerImpl.java:689: method: InputStream org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getInputStream()
    //#input(InputStream getInputStream()): this
    //#input(InputStream getInputStream()): this.resourceFile
    //#output(InputStream getInputStream()): new FileInputStream(getInputStream#1) num objects
    //#output(InputStream getInputStream()): return_value
    //#new obj(InputStream getInputStream()): new FileInputStream(getInputStream#1)
    //#pre[2] (InputStream getInputStream()): init'ed(this.resourceFile)
    //#post(InputStream getInputStream()): return_value == &new FileInputStream(getInputStream#1)
    //#post(InputStream getInputStream()): new FileInputStream(getInputStream#1) num objects == 1
            } catch (java.io.FileNotFoundException ex) {
                // should never happen, rethrow as runtime exception
                throw new RuntimeException("Error constructing input stream", ex);
    //#FileManagerImpl.java:692: end of method: InputStream org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.getInputStream()
            }
        }
    }
    
}
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$1__static_init): __Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl$1]
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$1__static_init): __Dispatch_Table.accept(Ljava/io/File;)Z
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$1__static_init): __Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl$1] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$1__static_init): __Dispatch_Table.accept(Ljava/io/File;)Z == &accept
    //#FileManagerImpl.java:: end of method: org.apache.roller.weblogger.business.FileManagerImpl$1.org.apache.roller.weblogger.business.FileManagerImpl$1__static_init
    //#FileManagerImpl.java:: end of class: org.apache.roller.weblogger.business.FileManagerImpl$1
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1__static_init): __Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl$WeblogResourceFile$1]
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1__static_init): __Dispatch_Table.accept(Ljava/io/File;)Z
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1__static_init): __Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl$WeblogResourceFile$1] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1__static_init): __Dispatch_Table.accept(Ljava/io/File;)Z == &accept
    //#FileManagerImpl.java:: end of method: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1.org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1__static_init
    //#FileManagerImpl.java:: end of class: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile$1
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl$WeblogResourceFile]
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getChildren()[Lorg/apache/roller/weblogger/pojos/ThemeResource;
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getInputStream()Ljava/io/InputStream;
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getLastModified()J
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getLength()J
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getName()Ljava/lang/String;
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getPath()Ljava/lang/String;
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getWeblog()Lorg/apache/roller/weblogger/pojos/Weblog;
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.isDirectory()Z
    //#output(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.isFile()Z
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl$WeblogResourceFile] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getChildren()[Lorg/apache/roller/weblogger/pojos/ThemeResource; == &getChildren
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getInputStream()Ljava/io/InputStream; == &getInputStream
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getLastModified()J == &getLastModified
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getLength()J == &getLength
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getName()Ljava/lang/String; == &getName
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getPath()Ljava/lang/String; == &getPath
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.getWeblog()Lorg/apache/roller/weblogger/pojos/Weblog; == &getWeblog
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.isDirectory()Z == &isDirectory
    //#post(org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init): __Dispatch_Table.isFile()Z == &isFile
    //#FileManagerImpl.java:: end of method: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile.org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile__static_init
    //#FileManagerImpl.java:: end of class: org.apache.roller.weblogger.business.FileManagerImpl$WeblogResourceFile
    //#FileManagerImpl.java:: end of class: org.apache.roller.weblogger.business.FileManagerImpl
