//# 10 errors, 754 messages
//#
/*
    //#ThemeManagerImpl.java:1:1: class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1
    //#ThemeManagerImpl.java:1:1: method: org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1.org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1__static_init
    //#ThemeManagerImpl.java:1:1: class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
 * 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.themes;

import java.io.File;
import java.io.FilenameFilter;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Date;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import org.apache.commons.logging.Log;
import org.apache.commons.logging.LogFactory;
import org.apache.roller.weblogger.WebloggerException;
import org.apache.roller.weblogger.business.FileManager;
import org.apache.roller.weblogger.business.InitializationException;
import org.apache.roller.weblogger.business.Weblogger;
import org.apache.roller.weblogger.business.UserManager;
import org.apache.roller.weblogger.config.WebloggerConfig;
import org.apache.roller.weblogger.pojos.Theme;
import org.apache.roller.weblogger.pojos.ThemeResource;
import org.apache.roller.weblogger.pojos.ThemeTemplate;
import org.apache.roller.weblogger.pojos.WeblogTemplate;
import org.apache.roller.weblogger.pojos.WeblogTheme;
import org.apache.roller.weblogger.pojos.Weblog;


/**
 * Base implementation of a ThemeManager.
 * 
 * This particular implementation reads theme data off the filesystem 
 * and assumes that those themes are not changable at runtime.
 */
@com.google.inject.Singleton
public class ThemeManagerImpl implements ThemeManager {
    
    private static Log log = LogFactory.getLog(ThemeManagerImpl.class);
    //#ThemeManagerImpl.java:57: method: org.apache.roller.weblogger.business.themes.ThemeManagerImpl.org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init
    //#ThemeManagerImpl.java:57: Warning: method not available
    //#    -- call on Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init
    //#    unanalyzed callee: Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeManagerImpl]
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.getEnabledThemesList()Ljava/util/List;
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.getTheme(Ljava/lang/String;)Lorg/apache/roller/weblogger/business/themes/SharedTheme;
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.getTheme(Lorg/apache/roller/weblogger/pojos/Weblog;)Lorg/apache/roller/weblogger/pojos/WeblogTheme;
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.importTheme(Lorg/apache/roller/weblogger/pojos/Weblog;Lorg/apache/roller/weblogger/business/themes/SharedTheme;)V
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.initialize()V
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.loadAllThemesFromDisk()Ljava/util/Map;
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): log
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): org/apache/roller/weblogger/business/themes/ThemeManager.__Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeManagerImpl]
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeManagerImpl] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): org/apache/roller/weblogger/business/themes/ThemeManager.__Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeManagerImpl] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.getEnabledThemesList()Ljava/util/List; == &getEnabledThemesList
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.getTheme(Ljava/lang/String;)Lorg/apache/roller/weblogger/business/themes/SharedTheme; == &getTheme
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.getTheme(Lorg/apache/roller/weblogger/pojos/Weblog;)Lorg/apache/roller/weblogger/pojos/WeblogTheme; == &getTheme
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.importTheme(Lorg/apache/roller/weblogger/pojos/Weblog;Lorg/apache/roller/weblogger/business/themes/SharedTheme;)V == &importTheme
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.initialize()V == &initialize
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): __Dispatch_Table.loadAllThemesFromDisk()Ljava/util/Map; == &loadAllThemesFromDisk
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init): init'ed(log)
    //#ThemeManagerImpl.java:57: end of method: org.apache.roller.weblogger.business.themes.ThemeManagerImpl.org.apache.roller.weblogger.business.themes.ThemeManagerImpl__static_init
    
    private final Weblogger roller;
    
    // directory where themes are kept
    private String themeDir = null;
    
    // the Map contains ... (theme id, Theme)
    private Map themes = null;
    
    
    @com.google.inject.Inject
    protected ThemeManagerImpl(Weblogger roller) {
    //#ThemeManagerImpl.java:69: method: void org.apache.roller.weblogger.business.themes.ThemeManagerImpl.org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): "="._tainted
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): "Fetching property ["._tainted
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): "]"._tainted
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): "couldn't access theme dir ["._tainted
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): "themes.dir"._tainted
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): org/apache/roller/weblogger/config/WebloggerConfig.config
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): org/apache/roller/weblogger/config/WebloggerConfig.log
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): roller
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): this
    //#output(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): java.lang.String:substring(...)._tainted
    //#output(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): this.roller
    //#output(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): this.themeDir
    //#output(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): this.themes
    //#new obj(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): java.lang.String:substring(...)
    //#pre[1] (void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): org/apache/roller/weblogger/config/WebloggerConfig.config != null
    //#pre[2] (void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): org/apache/roller/weblogger/config/WebloggerConfig.log != null
    //#presumption(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): java.io.File:canRead(...)@85 == 1
    //#presumption(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): java.io.File:exists(...)@85 == 1
    //#presumption(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): java.io.File:isDirectory(...)@85 == 1
    //#presumption(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): java.lang.String:length(...)@75 >= 1
    //#post(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): java.lang.String:substring(...)._tainted == 0
    //#post(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): this.roller == roller
    //#post(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): init'ed(this.roller)
    //#post(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): this.themeDir != null
    //#post(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): this.themes == null
    //#unanalyzed(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): Effects-of-calling:org.apache.commons.logging.Log:debug
    //#unanalyzed(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): Effects-of-calling:java.util.Properties:getProperty
    //#test_vector(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)): java.lang.String:endsWith(...)@79: {0}, {1}
        
        this.roller = roller;
        
        // get theme directory from config and verify it
        this.themeDir = WebloggerConfig.getProperty("themes.dir");
        if(themeDir == null || themeDir.trim().length() < 1) {
    //#ThemeManagerImpl.java:75: ?RuntimeException check
    //#    this.themeDir != null
    //#    severity: MEDIUM
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)
    //#    basic block: Entry_BB_1
    //#    assertion: this.themeDir != null
    //#    VN: getProperty(...) == null
    //#    Expected: {-Inf..0, 2..+Inf}
    //#    Bad: {1}
    //#    Attribs:  Int  Bad singleton  Bad overlaps +/-1000  Bad > Exp
            throw new RuntimeException("couldn't get themes directory from config");
        } else {
            // chop off trailing slash if it exists
            if(themeDir.endsWith("/")) {
                themeDir = themeDir.substring(0, themeDir.length()-1);
            }
            
            // make sure it exists and is readable
            File themeDirFile = new File(themeDir);
            if(!themeDirFile.exists() || 
                    !themeDirFile.isDirectory() || 
                    !themeDirFile.canRead()) {
                throw new RuntimeException("couldn't access theme dir ["+themeDir+"]");
            }
        }
    }
    //#ThemeManagerImpl.java:91: end of method: void org.apache.roller.weblogger.business.themes.ThemeManagerImpl.org.apache.roller.weblogger.business.themes.ThemeManagerImpl(Weblogger)
    
    
    public void initialize() throws InitializationException {
        
        log.debug("Initializing Theme Manager");
    //#ThemeManagerImpl.java:96: method: void org.apache.roller.weblogger.business.themes.ThemeManagerImpl.initialize()
    //#ThemeManagerImpl.java:96: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void initialize()
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
    //#input(void initialize()): " themes from disk."._tainted
    //#input(void initialize()): ":"._tainted
    //#input(void initialize()): "Couldn't load stylesheet theme ["._tainted
    //#input(void initialize()): "Couldn't load theme ["._tainted
    //#input(void initialize()): "Couldn't read  theme ["._tainted
    //#input(void initialize()): "Couldn't read theme ["._tainted
    //#input(void initialize()): "Exception reading theme ["._tainted
    //#input(void initialize()): "Loaded "._tainted
    //#input(void initialize()): "Loading Theme "._tainted
    //#input(void initialize()): "Parsing theme descriptor for "._tainted
    //#input(void initialize()): "Problem reading theme "._tainted
    //#input(void initialize()): "Unable to parse theme descriptor for theme "._tainted
    //#input(void initialize()): "] preview image file ["._tainted
    //#input(void initialize()): "] resource file ["._tainted
    //#input(void initialize()): "] template file ["._tainted
    //#input(void initialize()): "]"._tainted
    //#input(void initialize()): "theme.xml"._tainted
    //#input(void initialize()): java.io.File.separator
    //#input(void initialize()): java.io.File.separator._tainted
    //#input(void initialize()): log
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Descendant_Table[org/apache/roller/weblogger/business/themes/SharedThemeFromDir]
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Descendant_Table[others]
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setAuthor(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setDescription(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setEnabled(Z)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setLastModified(Ljava/util/Date;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setName(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.java.io.File.separator
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.java.io.File.separator._tainted
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.log
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeMetadata]
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.addResource(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.addTemplate(Lorg/apache/roller/weblogger/business/themes/ThemeMetadataTemplate;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getAuthor()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getId()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getPreviewImage()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getResources()Ljava/util/Set;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getStylesheet()Lorg/apache/roller/weblogger/business/themes/ThemeMetadataTemplate;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getTemplates()Ljava/util/Set;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.setAuthor(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.setName(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.setPreviewImage(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.setStylesheet(Lorg/apache/roller/weblogger/business/themes/ThemeMetadataTemplate;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataParser.__Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeMetadataParser]
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataParser.__Dispatch_Table.unmarshall(Ljava/io/InputStream;)Lorg/apache/roller/weblogger/business/themes/ThemeMetadata;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate]
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Descendant_Table[others]
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getAction()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getContentsFile()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getDescription()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getLink()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getTemplateLanguage()Ljava/lang/String;
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.isHidden()Z
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.isNavbar()Z
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setAction(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setContentType(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setContentsFile(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setDescription(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setHidden(Z)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setLink(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setName(Ljava/lang/String;)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setNavbar(Z)V
    //#input(void initialize()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setTemplateLanguage(Ljava/lang/String;)V
    //#input(void initialize()): this
    //#input(void initialize()): this.themeDir
    //#input(void initialize()): this.themeDir._tainted
    //#output(void initialize()): new HashMap(loadAllThemesFromDisk#1) num objects
    //#output(void initialize()): this.themes
    //#new obj(void initialize()): new HashMap(loadAllThemesFromDisk#1)
    //#pre[1] (void initialize()): log != null
    //#pre[5] (void initialize()): init'ed(this.themeDir)
    //#pre[3] (void initialize()): (soft) org/apache/roller/weblogger/business/themes/SharedThemeFromDir.log != null
    //#post(void initialize()): this.themes == One-of{old this.themes, &new HashMap(loadAllThemesFromDisk#1)}
    //#post(void initialize()): new HashMap(loadAllThemesFromDisk#1) num objects <= 1
    //#unanalyzed(void initialize()): Effects-of-calling:java.io.File
    //#unanalyzed(void initialize()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void initialize()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void initialize()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void initialize()): Effects-of-calling:java.util.HashMap
    //#unanalyzed(void initialize()): Effects-of-calling:java.io.File:list
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.commons.logging.Log:warn
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.commons.lang.StringUtils:replace
    //#unanalyzed(void initialize()): Effects-of-calling:java.util.Map:put
    //#unanalyzed(void initialize()): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void initialize()): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.roller.weblogger.pojos.ThemeTemplate:getName
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.roller.weblogger.pojos.ThemeTemplate:getLink
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.roller.weblogger.pojos.ThemeTemplate:getAction
    //#unanalyzed(void initialize()): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void initialize()): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void initialize()): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(void initialize()): Effects-of-calling:java.io.File:length
    //#unanalyzed(void initialize()): Effects-of-calling:java.io.FileInputStream
    //#unanalyzed(void initialize()): Effects-of-calling:java.io.InputStreamReader
    //#unanalyzed(void initialize()): Effects-of-calling:java.io.InputStreamReader:read
    //#unanalyzed(void initialize()): Effects-of-calling:java.lang.String
    //#unanalyzed(void initialize()): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(void initialize()): Effects-of-calling:getName
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.commons.logging.Log:error
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.commons.logging.Log:isDebugEnabled
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.commons.logging.Log:debug
    //#unanalyzed(void initialize()): Effects-of-calling:org.jdom.Element:getAttributeValue
    //#unanalyzed(void initialize()): Effects-of-calling:org.jdom.Element:getChildText
    //#unanalyzed(void initialize()): Effects-of-calling:java.lang.String:equalsIgnoreCase
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.commons.lang.StringUtils:isEmpty
    //#unanalyzed(void initialize()): Effects-of-calling:java.util.HashSet
    //#unanalyzed(void initialize()): Effects-of-calling:org.jdom.input.SAXBuilder
    //#unanalyzed(void initialize()): Effects-of-calling:org.jdom.input.SAXBuilder:build
    //#unanalyzed(void initialize()): Effects-of-calling:org.jdom.Document:getRootElement
    //#unanalyzed(void initialize()): Effects-of-calling:org.jdom.Element:getChild
    //#unanalyzed(void initialize()): Effects-of-calling:org.jdom.Element:getChildren
    //#unanalyzed(void initialize()): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void initialize()): Effects-of-calling:java.util.Set:add
    //#unanalyzed(void initialize()): Effects-of-calling:setId
    //#unanalyzed(void initialize()): Effects-of-calling:setName
    //#unanalyzed(void initialize()): Effects-of-calling:setDescription
    //#unanalyzed(void initialize()): Effects-of-calling:setAuthor
    //#unanalyzed(void initialize()): Effects-of-calling:java.util.Date
    //#unanalyzed(void initialize()): Effects-of-calling:setLastModified
    //#unanalyzed(void initialize()): Effects-of-calling:setEnabled
    //#unanalyzed(void initialize()): Effects-of-calling:java.io.File:lastModified
    //#unanalyzed(void initialize()): Effects-of-calling:java.util.Set:iterator
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.roller.weblogger.business.themes.SharedTheme
    //#unanalyzed(void initialize()): Effects-of-calling:org.apache.roller.weblogger.pojos.Theme:getId
    //#test_vector(void initialize()): this.themeDir: Addr_Set{null}, Inverse{null}
        
        if(themeDir != null) {
            // rather than be lazy we are going to load all themes from
            // the disk preemptively and cache them
            this.themes = loadAllThemesFromDisk();
            
            log.info("Loaded "+this.themes.size()+" themes from disk.");
    //#ThemeManagerImpl.java:103: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:info(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void initialize()
    //#    unanalyzed callee: void org.apache.commons.logging.Log:info(Object)
        }
    }
    //#ThemeManagerImpl.java:105: end of method: void org.apache.roller.weblogger.business.themes.ThemeManagerImpl.initialize()
    
    
    /**
     * @see org.apache.roller.weblogger.model.ThemeManager#getTheme(java.lang.String)
     */
    public SharedTheme getTheme(String id) 
            throws ThemeNotFoundException, WebloggerException {
        
        // try to lookup theme from library
        SharedTheme theme = (SharedTheme) this.themes.get(id);
    //#ThemeManagerImpl.java:115: method: SharedTheme org.apache.roller.weblogger.business.themes.ThemeManagerImpl.getTheme(String)
    //#input(SharedTheme getTheme(String)): "Couldn't find theme ["._tainted
    //#input(SharedTheme getTheme(String)): "]"._tainted
    //#input(SharedTheme getTheme(String)): id
    //#input(SharedTheme getTheme(String)): id._tainted
    //#input(SharedTheme getTheme(String)): org/apache/roller/weblogger/business/themes/SharedTheme.__Descendant_Table[org/apache/roller/weblogger/business/themes/SharedThemeFromDir]
    //#input(SharedTheme getTheme(String)): org/apache/roller/weblogger/business/themes/SharedTheme.__Descendant_Table[org/apache/roller/weblogger/business/themes/SharedTheme]
    //#input(SharedTheme getTheme(String)): org/apache/roller/weblogger/business/themes/SharedTheme.__Descendant_Table[others]
    //#input(SharedTheme getTheme(String)): this
    //#input(SharedTheme getTheme(String)): this.themes
    //#output(SharedTheme getTheme(String)): return_value
    //#pre[4] (SharedTheme getTheme(String)): this.themes != null
    //#presumption(SharedTheme getTheme(String)): java.util.Map:get(...).__Tag@115 in {org/apache/roller/weblogger/business/themes/SharedTheme, org/apache/roller/weblogger/business/themes/SharedThemeFromDir}
    //#presumption(SharedTheme getTheme(String)): java.util.Map:get(...)@115 != null
    //#post(SharedTheme getTheme(String)): (soft) return_value != null
    //#unanalyzed(SharedTheme getTheme(String)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(SharedTheme getTheme(String)): Effects-of-calling:org.apache.roller.RollerException
        
        // no theme?  throw exception.
        if(theme == null) {
            throw new ThemeNotFoundException("Couldn't find theme ["+id+"]");
        }
        
        return theme;
    //#ThemeManagerImpl.java:122: end of method: SharedTheme org.apache.roller.weblogger.business.themes.ThemeManagerImpl.getTheme(String)
    }
    
    
    /**
     * @see org.apache.roller.weblogger.model.ThemeManager#getTheme(weblog)
     */
    public WeblogTheme getTheme(Weblog weblog) throws WebloggerException {
        
        if(weblog == null)
    //#ThemeManagerImpl.java:131: method: WeblogTheme org.apache.roller.weblogger.business.themes.ThemeManagerImpl.getTheme(Weblog)
    //#ThemeManagerImpl.java:131: Warning: suspicious precondition
    //#    the precondition for this.roller.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: WeblogTheme getTheme(Weblog)
    //#    suspicious precondition index: [4]
    //#    Attribs:  Soft
    //#input(WeblogTheme getTheme(Weblog)): "Unable to lookup theme "._tainted
    //#input(WeblogTheme getTheme(Weblog)): log
    //#input(WeblogTheme getTheme(Weblog)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerImpl]
    //#input(WeblogTheme getTheme(Weblog)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/Weblogger]
    //#input(WeblogTheme getTheme(Weblog)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl]
    //#input(WeblogTheme getTheme(Weblog)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[others]
    //#input(WeblogTheme getTheme(Weblog)): org/apache/roller/weblogger/business/Weblogger.__Dispatch_Table.getThemeManager()Lorg/apache/roller/weblogger/business/themes/ThemeManager;
    //#input(WeblogTheme getTheme(Weblog)): org/apache/roller/weblogger/business/WebloggerImpl.__Dispatch_Table.getThemeManager()Lorg/apache/roller/weblogger/business/themes/ThemeManager;
    //#input(WeblogTheme getTheme(Weblog)): org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl.__Dispatch_Table.getThemeManager()Lorg/apache/roller/weblogger/business/themes/ThemeManager;
    //#input(WeblogTheme getTheme(Weblog)): org/apache/roller/weblogger/business/themes/SharedTheme.__Descendant_Table[org/apache/roller/weblogger/business/themes/SharedThemeFromDir]
    //#input(WeblogTheme getTheme(Weblog)): org/apache/roller/weblogger/business/themes/SharedTheme.__Descendant_Table[org/apache/roller/weblogger/business/themes/SharedTheme]
    //#input(WeblogTheme getTheme(Weblog)): org/apache/roller/weblogger/business/themes/SharedTheme.__Descendant_Table[others]
    //#input(WeblogTheme getTheme(Weblog)): this
    //#input(WeblogTheme getTheme(Weblog)): this.roller
    //#input(WeblogTheme getTheme(Weblog)): this.roller.__Tag
    //#input(WeblogTheme getTheme(Weblog)): this.roller.themeManager
    //#input(WeblogTheme getTheme(Weblog)): this.themes
    //#input(WeblogTheme getTheme(Weblog)): weblog
    //#output(WeblogTheme getTheme(Weblog)): new WeblogCustomTheme(getTheme#1) num objects
    //#output(WeblogTheme getTheme(Weblog)): new WeblogCustomTheme(getTheme#1).__Tag
    //#output(WeblogTheme getTheme(Weblog)): new WeblogSharedTheme(getTheme#2) num objects
    //#output(WeblogTheme getTheme(Weblog)): new WeblogSharedTheme(getTheme#2).__Tag
    //#output(WeblogTheme getTheme(Weblog)): new WeblogSharedTheme(getTheme#2).theme
    //#output(WeblogTheme getTheme(Weblog)): return_value
    //#new obj(WeblogTheme getTheme(Weblog)): new WeblogCustomTheme(getTheme#1)
    //#new obj(WeblogTheme getTheme(Weblog)): new WeblogSharedTheme(getTheme#2)
    //#pre[1] (WeblogTheme getTheme(Weblog)): (soft) log != null
    //#pre[3] (WeblogTheme getTheme(Weblog)): (soft) this.roller != null
    //#pre[4] (WeblogTheme getTheme(Weblog)): (soft) this.roller.__Tag in {org/apache/roller/weblogger/business/Weblogger, org/apache/roller/weblogger/business/WebloggerImpl, org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl}
    //#pre[6] (WeblogTheme getTheme(Weblog)): (soft) this.themes != null
    //#presumption(WeblogTheme getTheme(Weblog)): java.util.Map:get(...).__Tag@144 in {org/apache/roller/weblogger/business/themes/SharedTheme, org/apache/roller/weblogger/business/themes/SharedThemeFromDir}
    //#post(WeblogTheme getTheme(Weblog)): return_value in Addr_Set{null,&new WeblogSharedTheme(getTheme#2),&new WeblogCustomTheme(getTheme#1)}
    //#post(WeblogTheme getTheme(Weblog)): new WeblogCustomTheme(getTheme#1) num objects <= 1
    //#post(WeblogTheme getTheme(Weblog)): new WeblogCustomTheme(getTheme#1).__Tag == org/apache/roller/weblogger/business/themes/WeblogCustomTheme
    //#post(WeblogTheme getTheme(Weblog)): new WeblogSharedTheme(getTheme#2) num objects <= 1
    //#post(WeblogTheme getTheme(Weblog)): new WeblogSharedTheme(getTheme#2).__Tag == org/apache/roller/weblogger/business/themes/WeblogSharedTheme
    //#post(WeblogTheme getTheme(Weblog)): new WeblogSharedTheme(getTheme#2).theme != null
    //#unanalyzed(WeblogTheme getTheme(Weblog)): Effects-of-calling:org.apache.roller.weblogger.pojos.WeblogTheme
    //#test_vector(WeblogTheme getTheme(Weblog)): weblog: Inverse{null}, Addr_Set{null}
    //#test_vector(WeblogTheme getTheme(Weblog)): java.lang.String:equals(...)@137: {0}, {1}
    //#test_vector(WeblogTheme getTheme(Weblog)): java.util.Map:get(...)@144: Addr_Set{null}, Inverse{null}
    //#test_vector(WeblogTheme getTheme(Weblog)): org.apache.roller.weblogger.pojos.Weblog:getEditorTheme(...)@137: Addr_Set{null}, Inverse{null}
            return null;
        
        WeblogTheme weblogTheme = null;
        
        // if theme is custom or null then return a WeblogCustomTheme
        if(weblog.getEditorTheme() == null || 
    //#ThemeManagerImpl.java:137: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.Weblog:getEditorTheme()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: WeblogTheme getTheme(Weblog)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.Weblog:getEditorTheme()
                WeblogTheme.CUSTOM.equals(weblog.getEditorTheme())) {
            weblogTheme = new WeblogCustomTheme(weblog);
            
        // otherwise we are returning a WeblogSharedTheme
        } else {
            ThemeManager themeMgr = roller.getThemeManager();
    //#ThemeManagerImpl.java:143: Warning: unused assignment
    //#    unused assignment into themeMgr
    //#    severity: LOW
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: WeblogTheme getTheme(Weblog)
            SharedTheme staticTheme =
    //#ThemeManagerImpl.java:144: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.Weblog:getEditorTheme()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: WeblogTheme getTheme(Weblog)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.Weblog:getEditorTheme()
                    (SharedTheme) this.themes.get(weblog.getEditorTheme());
            if(staticTheme != null) {
                weblogTheme = new WeblogSharedTheme(weblog, staticTheme);
            } else {
                log.warn("Unable to lookup theme "+weblog.getEditorTheme());
    //#ThemeManagerImpl.java:149: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.Weblog:getEditorTheme()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: WeblogTheme getTheme(Weblog)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.Weblog:getEditorTheme()
    //#ThemeManagerImpl.java:149: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:warn(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: WeblogTheme getTheme(Weblog)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:warn(Object)
            }
        }
        
        // TODO: if somehow the theme is still null should we provide some
        // kind of fallback option like a default theme?
        
        return weblogTheme;
    //#ThemeManagerImpl.java:156: end of method: WeblogTheme org.apache.roller.weblogger.business.themes.ThemeManagerImpl.getTheme(Weblog)
    }

    
    /**
     * @see org.apache.roller.weblogger.model.ThemeManager#getEnabledThemesList()
     *
     * TODO: reimplement enabled vs. disabled logic once we support it
     */
    public List getEnabledThemesList() {
        
        List all_themes = new ArrayList(this.themes.values());
    //#ThemeManagerImpl.java:167: method: List org.apache.roller.weblogger.business.themes.ThemeManagerImpl.getEnabledThemesList()
    //#input(List getEnabledThemesList()): this
    //#input(List getEnabledThemesList()): this.themes
    //#output(List getEnabledThemesList()): new ArrayList(getEnabledThemesList#1) num objects
    //#output(List getEnabledThemesList()): return_value
    //#new obj(List getEnabledThemesList()): new ArrayList(getEnabledThemesList#1)
    //#pre[2] (List getEnabledThemesList()): this.themes != null
    //#post(List getEnabledThemesList()): return_value == &new ArrayList(getEnabledThemesList#1)
    //#post(List getEnabledThemesList()): new ArrayList(getEnabledThemesList#1) num objects == 1
                
        // sort 'em ... default ordering for themes is by name
        Collections.sort(all_themes);
        
        return all_themes;
    //#ThemeManagerImpl.java:172: end of method: List org.apache.roller.weblogger.business.themes.ThemeManagerImpl.getEnabledThemesList()
    }
    
    
    /**
     * @see org.apache.roller.weblogger.model.ThemeManager#importTheme(website, theme)
     */
    public void importTheme(Weblog website, SharedTheme theme)
            throws WebloggerException {
        
        log.debug("Importing theme ["+theme.getName()+"] to weblog ["+website.getName()+"]");
    //#ThemeManagerImpl.java:182: method: void org.apache.roller.weblogger.business.themes.ThemeManagerImpl.importTheme(Weblog, SharedTheme)
    //#ThemeManagerImpl.java:182: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.Weblog:getName()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.Weblog:getName()
    //#ThemeManagerImpl.java:182: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
    //#ThemeManagerImpl.java:182: 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.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    suspicious precondition index: [4]
    //#    Attribs:  Soft
    //#ThemeManagerImpl.java:182: Warning: suspicious precondition
    //#    the precondition for theme.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    suspicious precondition index: [15]
    //#ThemeManagerImpl.java:182: Warning: suspicious precondition
    //#    the precondition for this.roller...__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    suspicious precondition index: [21]
    //#    Attribs:  Soft
    //#ThemeManagerImpl.java:182: Warning: suspicious precondition
    //#    the precondition for this.roller...userManager.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    suspicious precondition index: [23]
    //#    Attribs:  Soft
    //#ThemeManagerImpl.java:182: Warning: suspicious precondition
    //#    the precondition for this.roller.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    suspicious precondition index: [27]
    //#ThemeManagerImpl.java:182: Warning: suspicious precondition
    //#    the precondition for this.roller.fileManager.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    suspicious precondition index: [29]
    //#    Attribs:  Soft
    //#ThemeManagerImpl.java:182: Warning: suspicious precondition
    //#    the precondition for this.roller.userManager.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    suspicious precondition index: [33]
    //#input(void importTheme(Weblog, SharedTheme)): "="._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "Creating directory ["._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "Failed to create directory ["._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "Importing resource to "._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "Importing theme ["._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "Invalid path ["._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "Removing stale action template "._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "The file has been written to ["._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "Trouble accessing property: "._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "] automatically"._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "] to weblog ["._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "]"._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "], "._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "attempted save file size = "._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "cannot read from path."._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "directory doesn't exist."._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "fetched property ["._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "max allowed file size = "._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "probably doesn't have needed parent directories."._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "text.plain"._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "trying to get outside uploads dir."._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "trying to use nested directories."._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "uploads.dir.maxsize"._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "uploads.enabled"._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "uploads.file.maxsize"._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "uploads.types.allowed"._tainted
    //#input(void importTheme(Weblog, SharedTheme)): "uploads.types.forbid"._tainted
    //#input(void importTheme(Weblog, SharedTheme)): log
    //#input(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.WeblogTemplate.ACTIONS
    //#input(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.WeblogTemplate.ACTIONS.length
    //#input(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.WeblogTemplate.ACTIONS[0..4_294_967_295]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManager.__Descendant_Table[org/apache/roller/weblogger/business/FileManagerImpl]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManager.__Descendant_Table[org/apache/roller/weblogger/business/FileManager]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManager.__Descendant_Table[others]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManager.__Dispatch_Table.createDirectory(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManager.__Dispatch_Table.saveFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;Ljava/lang/String;JLjava/io/InputStream;Z)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManagerImpl.__Dispatch_Table.createDirectory(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManagerImpl.__Dispatch_Table.saveFile(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;Ljava/lang/String;JLjava/io/InputStream;Z)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManagerImpl.java.io.File.separator
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManagerImpl.java.io.File.separator._tainted
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManagerImpl.java.io.File.separatorChar
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/FileManagerImpl.log
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/GuiceWebloggerProvider.__Dispatch_Table.getWeblogger()Lorg/apache/roller/weblogger/business/Weblogger;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[org/apache/roller/weblogger/business/PropertiesManager]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAPropertiesManagerImpl]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/PropertiesManager.__Descendant_Table[others]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/PropertiesManager.__Dispatch_Table.getProperty(Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/RuntimeConfigProperty;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/UserManager.__Descendant_Table[org/apache/roller/weblogger/business/UserManager]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/UserManager.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/UserManager.__Descendant_Table[others]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/UserManager.__Dispatch_Table.getPageByAction(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/WeblogTemplate;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/UserManager.__Dispatch_Table.getPageByName(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/WeblogTemplate;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/UserManager.__Dispatch_Table.removePage(Lorg/apache/roller/weblogger/pojos/WeblogTemplate;)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/UserManager.__Dispatch_Table.savePage(Lorg/apache/roller/weblogger/pojos/WeblogTemplate;)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/UserManager.__Dispatch_Table.saveWebsite(Lorg/apache/roller/weblogger/pojos/Weblog;)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerImpl]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/Weblogger]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/Weblogger.__Descendant_Table[others]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/Weblogger.__Dispatch_Table.getFileManager()Lorg/apache/roller/weblogger/business/FileManager;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/Weblogger.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/Weblogger.__Dispatch_Table.getUserManager()Lorg/apache/roller/weblogger/business/UserManager;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance.propertiesManager.strategy.threadLocalEntityManager
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerImpl.__Dispatch_Table.getFileManager()Lorg/apache/roller/weblogger/business/FileManager;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerImpl.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerImpl.__Dispatch_Table.getUserManager()Lorg/apache/roller/weblogger/business/UserManager;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[org/apache/roller/weblogger/business/GuiceWebloggerProvider]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[org/apache/roller/weblogger/business/WebloggerProvider]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerProvider.__Descendant_Table[others]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/WebloggerProvider.__Dispatch_Table.getWeblogger()Lorg/apache/roller/weblogger/business/Weblogger;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Descendant_Table[org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Descendant_Table[others]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Dispatch_Table.getNamedQuery(Ljava/lang/String;)Ljavax/persistence/Query;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Dispatch_Table.load(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Object;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Dispatch_Table.remove(Ljava/lang/Object;)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.__Dispatch_Table.store(Ljava/lang/Object;)Ljava/lang/Object;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy.javax.persistence.FlushModeType.COMMIT
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAPropertiesManagerImpl.__Dispatch_Table.getProperty(Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/RuntimeConfigProperty;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.__Dispatch_Table.getPageByAction(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/WeblogTemplate;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.__Dispatch_Table.getPageByName(Lorg/apache/roller/weblogger/pojos/Weblog;Ljava/lang/String;)Lorg/apache/roller/weblogger/pojos/WeblogTemplate;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.__Dispatch_Table.removePage(Lorg/apache/roller/weblogger/pojos/WeblogTemplate;)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.__Dispatch_Table.savePage(Lorg/apache/roller/weblogger/pojos/WeblogTemplate;)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.__Dispatch_Table.saveWebsite(Lorg/apache/roller/weblogger/pojos/Weblog;)V
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl.__Dispatch_Table.getFileManager()Lorg/apache/roller/weblogger/business/FileManager;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl.__Dispatch_Table.getPropertiesManager()Lorg/apache/roller/weblogger/business/PropertiesManager;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl.__Dispatch_Table.getUserManager()Lorg/apache/roller/weblogger/business/UserManager;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/themes/SharedTheme.__Descendant_Table[org/apache/roller/weblogger/business/themes/SharedThemeFromDir]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/themes/SharedTheme.__Descendant_Table[org/apache/roller/weblogger/business/themes/SharedTheme]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/themes/SharedTheme.__Descendant_Table[others]
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/themes/SharedTheme.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/themes/SharedTheme.__Dispatch_Table.getResources()Ljava/util/List;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.getResources()Ljava/util/List;
    //#input(void importTheme(Weblog, SharedTheme)): org/apache/roller/weblogger/config/WebloggerRuntimeConfig.log
    //#input(void importTheme(Weblog, SharedTheme)): theme
    //#input(void importTheme(Weblog, SharedTheme)): theme.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): theme.name
    //#input(void importTheme(Weblog, SharedTheme)): theme.name._tainted
    //#input(void importTheme(Weblog, SharedTheme)): theme.resources
    //#input(void importTheme(Weblog, SharedTheme)): this
    //#input(void importTheme(Weblog, SharedTheme)): this.roller
    //#input(void importTheme(Weblog, SharedTheme)): this.roller...__Tag
    //#input(void importTheme(Weblog, SharedTheme)): this.roller...userManager
    //#input(void importTheme(Weblog, SharedTheme)): this.roller...userManager.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): this.roller...userManager.strategy
    //#input(void importTheme(Weblog, SharedTheme)): this.roller...userManager.strategy.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): this.roller...userManager.strategy.emf
    //#input(void importTheme(Weblog, SharedTheme)): this.roller...userManager.strategy.threadLocalEntityManager
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.fileManager
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.fileManager.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.fileManager.upload_dir
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.fileManager.upload_dir._tainted
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.userManager
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.userManager.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.userManager.roller
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.userManager.strategy
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.userManager.strategy.__Tag
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.userManager.strategy.emf
    //#input(void importTheme(Weblog, SharedTheme)): this.roller.userManager.strategy.threadLocalEntityManager
    //#input(void importTheme(Weblog, SharedTheme)): website
    //#pre[1] (void importTheme(Weblog, SharedTheme)): log != null
    //#pre[14] (void importTheme(Weblog, SharedTheme)): theme != null
    //#pre[15] (void importTheme(Weblog, SharedTheme)): theme.__Tag in {org/apache/roller/weblogger/business/themes/SharedTheme, org/apache/roller/weblogger/business/themes/SharedThemeFromDir}
    //#pre[16] (void importTheme(Weblog, SharedTheme)): init'ed(theme.name)
    //#pre[18] (void importTheme(Weblog, SharedTheme)): theme.resources != null
    //#pre[20] (void importTheme(Weblog, SharedTheme)): this.roller != null
    //#pre[27] (void importTheme(Weblog, SharedTheme)): this.roller.__Tag in {org/apache/roller/weblogger/business/Weblogger, org/apache/roller/weblogger/business/WebloggerImpl, org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl}
    //#pre[32] (void importTheme(Weblog, SharedTheme)): this.roller.userManager != null
    //#pre[33] (void importTheme(Weblog, SharedTheme)): this.roller.userManager.__Tag in {org/apache/roller/weblogger/business/UserManager, org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl}
    //#pre[35] (void importTheme(Weblog, SharedTheme)): this.roller.userManager.strategy != null
    //#pre[36] (void importTheme(Weblog, SharedTheme)): this.roller.userManager.strategy.__Tag == org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy
    //#pre[38] (void importTheme(Weblog, SharedTheme)): this.roller.userManager.strategy.threadLocalEntityManager != null
    //#pre[39] (void importTheme(Weblog, SharedTheme)): website != null
    //#pre[2] (void importTheme(Weblog, SharedTheme)): (soft) org/apache/roller/weblogger/business/FileManagerImpl.log != null
    //#pre[3] (void importTheme(Weblog, SharedTheme)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider != null
    //#pre[4] (void importTheme(Weblog, SharedTheme)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.__Tag in {org/apache/roller/weblogger/business/GuiceWebloggerProvider, org/apache/roller/weblogger/business/WebloggerProvider}
    //#pre[5] (void importTheme(Weblog, SharedTheme)): (soft) org/apache/roller/weblogger/business/WebloggerFactory.webloggerProvider.webloggerInstance != null
    //#pre[13] (void importTheme(Weblog, SharedTheme)): (soft) org/apache/roller/weblogger/config/WebloggerRuntimeConfig.log != null
    //#pre[21] (void importTheme(Weblog, SharedTheme)): (soft) this.roller...__Tag in {org/apache/roller/weblogger/business/Weblogger, org/apache/roller/weblogger/business/WebloggerImpl, org/apache/roller/weblogger/business/jpa/JPAWebloggerImpl}
    //#pre[22] (void importTheme(Weblog, SharedTheme)): (soft) this.roller...userManager != null
    //#pre[23] (void importTheme(Weblog, SharedTheme)): (soft) this.roller...userManager.__Tag in {org/apache/roller/weblogger/business/UserManager, org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl}
    //#pre[24] (void importTheme(Weblog, SharedTheme)): (soft) this.roller...userManager.strategy != null
    //#pre[25] (void importTheme(Weblog, SharedTheme)): (soft) this.roller...userManager.strategy.__Tag == org/apache/roller/weblogger/business/jpa/JPAPersistenceStrategy
    //#pre[26] (void importTheme(Weblog, SharedTheme)): (soft) this.roller...userManager.strategy.threadLocalEntityManager != null
    //#pre[28] (void importTheme(Weblog, SharedTheme)): (soft) this.roller.fileManager != null
    //#pre[29] (void importTheme(Weblog, SharedTheme)): (soft) this.roller.fileManager.__Tag in {org/apache/roller/weblogger/business/FileManager, org/apache/roller/weblogger/business/FileManagerImpl}
    //#pre[30] (void importTheme(Weblog, SharedTheme)): (soft) init'ed(this.roller.fileManager.upload_dir)
    //#pre[34] (void importTheme(Weblog, SharedTheme)): (soft) this.roller.userManager.roller != null
    //#pre[37] (void importTheme(Weblog, SharedTheme)): (soft) this.roller.userManager.strategy.emf != null
    //#presumption(void importTheme(Weblog, SharedTheme)): java.util.Iterator:next(...)@192 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): java.util.Iterator:next(...)@272 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): getUserManager(...)@185...strategy != userMgr.roller.userManager.strategy
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.business.themes.SharedTheme:getStylesheet(...)@260 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.business.themes.SharedTheme:getTemplates(...)@190 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.ThemeResource:getInputStream(...)@281 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.ThemeResource:getPath(...)@278 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.ThemeResource:getPath(...)@281 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.ThemeTemplate:getAction(...)@197 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.ThemeTemplate:getAction(...)@199 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.ThemeTemplate:getName(...)@206 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.WeblogTemplate.ACTIONS != null
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.WeblogTemplate.ACTIONS.length <= 4_294_967_295
    //#presumption(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.WeblogTemplate.ACTIONS[0..4_294_967_295] != null
    //#presumption(void importTheme(Weblog, SharedTheme)): this.roller.userManager.roller != getUserManager(...)@185.roller
    //#presumption(void importTheme(Weblog, SharedTheme)): userMgr.strategy.emf@199 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): userMgr.strategy.emf@206 != null
    //#presumption(void importTheme(Weblog, SharedTheme)): userMgr.strategy.emf@248 != null
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:getUserManager
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:saveWebsite
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.util.Map:values
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.util.Collections:sort
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.ThreadLocal:get
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.EntityManagerFactory:createEntityManager
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.ThreadLocal:set
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.EntityManager:getTransaction
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.EntityTransaction:isActive
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.EntityTransaction:begin
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.EntityManager:createNamedQuery
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.Query:setFlushMode
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.Query:setParameter
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.Query:getSingleResult
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.EntityManager:contains
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.EntityManager:persist
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.roller.weblogger.pojos.WeblogTemplate:getWebsite
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.util.Date
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:setLastModified
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.EntityManager:remove
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.String:replace
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.roller.weblogger.pojos.Weblog:getHandle
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.File
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.File:getAbsolutePath
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.File:getCanonicalPath
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.File:isDirectory
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.File:mkdir
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.String:endsWith
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.File:listFiles
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.File:length
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:getDirSize
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.String:split
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.String:toLowerCase
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:getBooleanProperty
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.roller.weblogger.util.RollerMessages:addError
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:getProperty
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.math.BigDecimal
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.math.BigDecimal:doubleValue
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.commons.logging.Log:debug
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.math.BigDecimal:toString
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.commons.lang.StringUtils:deleteWhitespace
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.commons.lang.StringUtils:split
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.RuntimeException
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.roller.weblogger.util.RollerMessages
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.roller.weblogger.util.RollerMessages:toString
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.FileOutputStream
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.InputStream:read
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.OutputStream:write
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.OutputStream:flush
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.io.OutputStream:close
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:getWeblogger
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:getPropertiesManager
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:javax.persistence.EntityManager:find
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.roller.weblogger.pojos.RuntimeConfigProperty:getValue
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:org.apache.commons.logging.Log:warn
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.Boolean
    //#unanalyzed(void importTheme(Weblog, SharedTheme)): Effects-of-calling:java.lang.Boolean:booleanValue
    //#test_vector(void importTheme(Weblog, SharedTheme)): java.lang.Object:equals(...)@223: {1}, {0}
    //#test_vector(void importTheme(Weblog, SharedTheme)): java.lang.String:equals(...)@197: {1}, {0}
    //#test_vector(void importTheme(Weblog, SharedTheme)): java.util.Iterator:hasNext(...)@191: {0}, {1}
    //#test_vector(void importTheme(Weblog, SharedTheme)): java.util.Iterator:hasNext(...)@271: {0}, {1}
    //#test_vector(void importTheme(Weblog, SharedTheme)): java.util.Set:contains(...)@247: {1}, {0}
    //#test_vector(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.business.themes.SharedTheme:getStylesheet(...)@259: Addr_Set{null}, Inverse{null}
    //#test_vector(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.ThemeResource:isDirectory(...)@277: {0}, {1}
    //#test_vector(void importTheme(Weblog, SharedTheme)): org.apache.roller.weblogger.pojos.ThemeTemplate:getAction(...)@197: Addr_Set{null}, Inverse{null}
        
        try {
            UserManager userMgr = roller.getUserManager();
            
            Set importedActionTemplates = new HashSet();
            ThemeTemplate themeTemplate = null;
    //#ThemeManagerImpl.java:188: Warning: unused assignment
    //#    unused assignment into themeTemplate
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    Attribs:  Uncertain
            ThemeTemplate stylesheetTemplate = theme.getStylesheet();
    //#ThemeManagerImpl.java:189: Warning: method not available
    //#    -- call on ThemeTemplate org.apache.roller.weblogger.business.themes.SharedTheme:getStylesheet()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: ThemeTemplate org.apache.roller.weblogger.business.themes.SharedTheme:getStylesheet()
            Iterator iter = theme.getTemplates().iterator();
    //#ThemeManagerImpl.java:190: Warning: method not available
    //#    -- call on List org.apache.roller.weblogger.business.themes.SharedTheme:getTemplates()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: List org.apache.roller.weblogger.business.themes.SharedTheme:getTemplates()
            while ( iter.hasNext() ) {
                themeTemplate = (ThemeTemplate) iter.next();
                
                WeblogTemplate template = null;
    //#ThemeManagerImpl.java:194: Warning: unused assignment
    //#    unused assignment into template
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    Attribs:  Uncertain
                
                // if template is an action, lookup by action
                if(themeTemplate.getAction() != null &&
    //#ThemeManagerImpl.java:197: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getAction()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getAction()
                        !themeTemplate.getAction().equals(WeblogTemplate.ACTION_CUSTOM)) {
                    template = userMgr.getPageByAction(website, themeTemplate.getAction());
    //#ThemeManagerImpl.java:199: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getAction()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getAction()
    //#ThemeManagerImpl.java:199: ?precondition failure
    //#    org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.getPageByAction: (soft) this.strategy.emf != null
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    basic block: bb_6
    //#    assertion: (soft) userMgr.strategy.emf != null
    //#    callee: WeblogTemplate org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.getPageByAction(Weblog, String)
    //#    callee assertion: (soft) this.strategy.emf != null
    //#    callee file: JPAUserManagerImpl.java
    //#    callee precondition index: [5]
    //#    callee srcpos: 916
    //#    VN: userMgr.strategy.emf
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad  Soft  Uncertain
                    if(template != null) {
                        importedActionTemplates.add(themeTemplate.getAction());
    //#ThemeManagerImpl.java:201: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getAction()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getAction()
                    }
                    
                // otherwise, lookup by name
                } else {
                    template = userMgr.getPageByName(website, themeTemplate.getName());
    //#ThemeManagerImpl.java:206: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getName()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getName()
    //#ThemeManagerImpl.java:206: ?precondition failure
    //#    org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.getPageByName: (soft) this.strategy.emf != null
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    basic block: bb_8
    //#    assertion: (soft) userMgr.strategy.emf != null
    //#    callee: WeblogTemplate org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.getPageByName(Weblog, String)
    //#    callee assertion: (soft) this.strategy.emf != null
    //#    callee file: JPAUserManagerImpl.java
    //#    callee precondition index: [5]
    //#    callee srcpos: 939
    //#    VN: userMgr.strategy.emf
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad  Soft  Uncertain
                }
                
                // Weblog does not have this template, so create it.
                boolean newTmpl = false;
                if (template == null) {
                    template = new WeblogTemplate();
    //#ThemeManagerImpl.java:212: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate()
                    template.setWebsite(website);
    //#ThemeManagerImpl.java:213: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setWebsite(Weblog)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setWebsite(Weblog)
                    newTmpl = true;
                }

                // TODO: fix conflict situation
                // it's possible that someone has defined a theme template which
                // matches 2 existing templates, 1 by action, the other by name
                
                // update template attributes
                // NOTE: we don't want to copy the template data for an existing stylesheet
                if(newTmpl || !themeTemplate.equals(stylesheetTemplate)) {
                    template.setAction(themeTemplate.getAction());
    //#ThemeManagerImpl.java:224: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getAction()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getAction()
    //#ThemeManagerImpl.java:224: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setAction(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setAction(String)
                    template.setName(themeTemplate.getName());
    //#ThemeManagerImpl.java:225: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getName()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getName()
    //#ThemeManagerImpl.java:225: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setName(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setName(String)
                    template.setDescription(themeTemplate.getDescription());
    //#ThemeManagerImpl.java:226: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getDescription()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getDescription()
    //#ThemeManagerImpl.java:226: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setDescription(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setDescription(String)
                    template.setLink(themeTemplate.getLink());
    //#ThemeManagerImpl.java:227: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getLink()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getLink()
    //#ThemeManagerImpl.java:227: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setLink(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setLink(String)
                    template.setContents(themeTemplate.getContents());
    //#ThemeManagerImpl.java:228: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getContents()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getContents()
    //#ThemeManagerImpl.java:228: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setContents(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setContents(String)
                    template.setHidden(themeTemplate.isHidden());
    //#ThemeManagerImpl.java:229: Warning: method not available
    //#    -- call on bool org.apache.roller.weblogger.pojos.ThemeTemplate:isHidden()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: bool org.apache.roller.weblogger.pojos.ThemeTemplate:isHidden()
    //#ThemeManagerImpl.java:229: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setHidden(bool)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setHidden(bool)
                    template.setNavbar(themeTemplate.isNavbar());
    //#ThemeManagerImpl.java:230: Warning: method not available
    //#    -- call on bool org.apache.roller.weblogger.pojos.ThemeTemplate:isNavbar()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: bool org.apache.roller.weblogger.pojos.ThemeTemplate:isNavbar()
    //#ThemeManagerImpl.java:230: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setNavbar(bool)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setNavbar(bool)
                    template.setTemplateLanguage(themeTemplate.getTemplateLanguage());
    //#ThemeManagerImpl.java:231: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getTemplateLanguage()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getTemplateLanguage()
    //#ThemeManagerImpl.java:231: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setTemplateLanguage(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setTemplateLanguage(String)
                    // NOTE: decorators are deprecated starting in 4.0
                    template.setDecoratorName(null);
    //#ThemeManagerImpl.java:233: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setDecoratorName(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setDecoratorName(String)
                    template.setLastModified(new Date());
    //#ThemeManagerImpl.java:234: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.WeblogTemplate:setLastModified(Date)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.WeblogTemplate:setLastModified(Date)
                    
                    // save it
                    userMgr.savePage( template );
    //#ThemeManagerImpl.java:237: ?precondition failure
    //#    org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.savePage: this.roller.userManager.__Tag in {org/apache/roller/weblogger/business/UserManager, org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl}
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    basic block: bb_13
    //#    assertion: userMgr.roller.userManager.__Tag in {org/apache/roller/weblogger/business/UserManager, org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl}
    //#    callee: void org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.savePage(WeblogTemplate)
    //#    callee assertion: this.roller.userManager.__Tag in {org/apache/roller/weblogger/business/UserManager, org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl}
    //#    callee file: JPAUserManagerImpl.java
    //#    callee precondition index: [6]
    //#    callee srcpos: 300
    //#    VN: userMgr.roller.userManager.__Tag
    //#    Expected: {333_056, 340_992}
    //#    Bad: {0, Invalid}
    //#    Attribs:  Int  Bad singleton  Bad overlaps +/-1000  Bad < Exp
                }
            }
            
            // now, see if the weblog has left over action templates that
            // need to be deleted because they aren't in their new theme
            for(int i=0; i < WeblogTemplate.ACTIONS.length; i++) {
                String action = WeblogTemplate.ACTIONS[i];
                
                // if we didn't import this action then see if it should be deleted
                if(!importedActionTemplates.contains(action)) {
                    WeblogTemplate toDelete = userMgr.getPageByAction(website, action);
    //#ThemeManagerImpl.java:248: ?precondition failure
    //#    org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.getPageByAction: (soft) this.strategy.emf != null
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    basic block: bb_18
    //#    assertion: (soft) userMgr.strategy.emf != null
    //#    callee: WeblogTemplate org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.getPageByAction(Weblog, String)
    //#    callee assertion: (soft) this.strategy.emf != null
    //#    callee file: JPAUserManagerImpl.java
    //#    callee precondition index: [5]
    //#    callee srcpos: 916
    //#    VN: userMgr.strategy.emf
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad  Soft  Uncertain
                    if(toDelete != null) {
                        log.debug("Removing stale action template "+toDelete.getId());
    //#ThemeManagerImpl.java:250: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.WeblogTemplate:getId()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.WeblogTemplate:getId()
    //#ThemeManagerImpl.java:250: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
                        userMgr.removePage(toDelete);
    //#ThemeManagerImpl.java:251: ?precondition failure
    //#    org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.removePage: this.roller.userManager.__Tag in {org/apache/roller/weblogger/business/UserManager, org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl}
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    basic block: bb_19
    //#    assertion: userMgr.roller.userManager.__Tag in {org/apache/roller/weblogger/business/UserManager, org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl}
    //#    callee: void org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.removePage(WeblogTemplate)
    //#    callee assertion: this.roller.userManager.__Tag in {org/apache/roller/weblogger/business/UserManager, org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl}
    //#    callee file: JPAUserManagerImpl.java
    //#    callee precondition index: [6]
    //#    callee srcpos: 308
    //#    VN: userMgr.roller.userManager.__Tag
    //#    Expected: {333_056, 340_992}
    //#    Bad: {0, Invalid}
    //#    Attribs:  Int  Bad singleton  Bad overlaps +/-1000  Bad < Exp
                    }
                }
            }
            
            
            // always update this weblog's theme and customStylesheet, then save
            website.setEditorTheme(WeblogTheme.CUSTOM);
    //#ThemeManagerImpl.java:258: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.Weblog:setEditorTheme(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.Weblog:setEditorTheme(String)
            if(theme.getStylesheet() != null) {
    //#ThemeManagerImpl.java:259: Warning: method not available
    //#    -- call on ThemeTemplate org.apache.roller.weblogger.business.themes.SharedTheme:getStylesheet()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: ThemeTemplate org.apache.roller.weblogger.business.themes.SharedTheme:getStylesheet()
                website.setCustomStylesheetPath(theme.getStylesheet().getLink());
    //#ThemeManagerImpl.java:260: Warning: method not available
    //#    -- call on ThemeTemplate org.apache.roller.weblogger.business.themes.SharedTheme:getStylesheet()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: ThemeTemplate org.apache.roller.weblogger.business.themes.SharedTheme:getStylesheet()
    //#ThemeManagerImpl.java:260: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeTemplate:getLink()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeTemplate:getLink()
    //#ThemeManagerImpl.java:260: Warning: method not available
    //#    -- call on void org.apache.roller.weblogger.pojos.Weblog:setCustomStylesheetPath(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.roller.weblogger.pojos.Weblog:setCustomStylesheetPath(String)
            }
            userMgr.saveWebsite(website);
    //#ThemeManagerImpl.java:262: ?precondition failure
    //#    org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.saveWebsite: (soft) this.strategy.emf != null
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    basic block: bb_23
    //#    assertion: (soft) userMgr.strategy.emf != null
    //#    callee: void org/apache/roller/weblogger/business/jpa/JPAUserManagerImpl.saveWebsite(Weblog)
    //#    callee assertion: (soft) this.strategy.emf != null
    //#    callee file: JPAUserManagerImpl.java
    //#    callee precondition index: [4]
    //#    callee srcpos: 87
    //#    VN: userMgr.strategy.emf
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad  Soft  Uncertain
            
            
            // now lets import all the theme resources
            FileManager fileMgr = roller.getFileManager();
            
            List resources = theme.getResources();
            Iterator iterat = resources.iterator();
            ThemeResource resource = null;
    //#ThemeManagerImpl.java:270: Warning: unused assignment
    //#    unused assignment into resource
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    Attribs:  Uncertain
            while ( iterat.hasNext() ) {
                resource = (ThemeResource) iterat.next();
                
                log.debug("Importing resource to "+resource.getPath());
    //#ThemeManagerImpl.java:274: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeResource:getPath()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeResource:getPath()
    //#ThemeManagerImpl.java:274: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
                
                try {
                    if(resource.isDirectory()) {
    //#ThemeManagerImpl.java:277: Warning: method not available
    //#    -- call on bool org.apache.roller.weblogger.pojos.ThemeResource:isDirectory()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: bool org.apache.roller.weblogger.pojos.ThemeResource:isDirectory()
                        fileMgr.createDirectory(website, resource.getPath());
    //#ThemeManagerImpl.java:278: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeResource:getPath()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeResource:getPath()
                    } else {
                        // save file without file-type, quota checks, etc.
                        fileMgr.saveFile(website, resource.getPath(), "text/plain", 
    //#ThemeManagerImpl.java:281: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeResource:getPath()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeResource:getPath()
    //#ThemeManagerImpl.java:281: Warning: method not available
    //#    -- call on long org.apache.roller.weblogger.pojos.ThemeResource:getLength()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: long org.apache.roller.weblogger.pojos.ThemeResource:getLength()
    //#ThemeManagerImpl.java:281: Warning: method not available
    //#    -- call on InputStream org.apache.roller.weblogger.pojos.ThemeResource:getInputStream()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: InputStream org.apache.roller.weblogger.pojos.ThemeResource:getInputStream()
                                resource.getLength(), resource.getInputStream(), false);
                    }
                } catch (Exception ex) {
                    log.info(ex);
    //#ThemeManagerImpl.java:285: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:info(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: void importTheme(Weblog, SharedTheme)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:info(Object)
                }
            }
            
        } catch (Exception e) {
            log.error("ERROR importing theme", e);
            throw new WebloggerException( e );
        }
    }
    //#ThemeManagerImpl.java:293: end of method: void org.apache.roller.weblogger.business.themes.ThemeManagerImpl.importTheme(Weblog, SharedTheme)
    
    
    /**
     * This is a convenience method which loads all the theme data from
     * themes stored on the filesystem in the roller webapp /themes/ directory.
     */
    private Map loadAllThemesFromDisk() {
        
        Map themes = new HashMap();
    //#ThemeManagerImpl.java:302: method: Map org.apache.roller.weblogger.business.themes.ThemeManagerImpl.loadAllThemesFromDisk()
    //#input(Map loadAllThemesFromDisk()): ":"._tainted
    //#input(Map loadAllThemesFromDisk()): "Couldn't load stylesheet theme ["._tainted
    //#input(Map loadAllThemesFromDisk()): "Couldn't load theme ["._tainted
    //#input(Map loadAllThemesFromDisk()): "Couldn't read  theme ["._tainted
    //#input(Map loadAllThemesFromDisk()): "Couldn't read theme ["._tainted
    //#input(Map loadAllThemesFromDisk()): "Exception reading theme ["._tainted
    //#input(Map loadAllThemesFromDisk()): "Loading Theme "._tainted
    //#input(Map loadAllThemesFromDisk()): "Parsing theme descriptor for "._tainted
    //#input(Map loadAllThemesFromDisk()): "Problem reading theme "._tainted
    //#input(Map loadAllThemesFromDisk()): "Unable to parse theme descriptor for theme "._tainted
    //#input(Map loadAllThemesFromDisk()): "] preview image file ["._tainted
    //#input(Map loadAllThemesFromDisk()): "] resource file ["._tainted
    //#input(Map loadAllThemesFromDisk()): "] template file ["._tainted
    //#input(Map loadAllThemesFromDisk()): "]"._tainted
    //#input(Map loadAllThemesFromDisk()): "theme.xml"._tainted
    //#input(Map loadAllThemesFromDisk()): java.io.File.separator
    //#input(Map loadAllThemesFromDisk()): java.io.File.separator._tainted
    //#input(Map loadAllThemesFromDisk()): log
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Descendant_Table[org/apache/roller/weblogger/business/themes/SharedThemeFromDir]
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Descendant_Table[others]
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setAuthor(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setDescription(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setEnabled(Z)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setLastModified(Ljava/util/Date;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.__Dispatch_Table.setName(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.java.io.File.separator
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.java.io.File.separator._tainted
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/SharedThemeFromDir.log
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeMetadata]
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.addResource(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.addTemplate(Lorg/apache/roller/weblogger/business/themes/ThemeMetadataTemplate;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getAuthor()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getId()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getPreviewImage()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getResources()Ljava/util/Set;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getStylesheet()Lorg/apache/roller/weblogger/business/themes/ThemeMetadataTemplate;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.getTemplates()Ljava/util/Set;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.setAuthor(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.setName(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.setPreviewImage(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadata.__Dispatch_Table.setStylesheet(Lorg/apache/roller/weblogger/business/themes/ThemeMetadataTemplate;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataParser.__Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeMetadataParser]
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataParser.__Dispatch_Table.unmarshall(Ljava/io/InputStream;)Lorg/apache/roller/weblogger/business/themes/ThemeMetadata;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate]
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Descendant_Table[others]
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getAction()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getContentsFile()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getDescription()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getLink()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.getTemplateLanguage()Ljava/lang/String;
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.isHidden()Z
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.isNavbar()Z
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setAction(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setContentType(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setContentsFile(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setDescription(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setHidden(Z)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setLink(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setName(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setNavbar(Z)V
    //#input(Map loadAllThemesFromDisk()): org/apache/roller/weblogger/business/themes/ThemeMetadataTemplate.__Dispatch_Table.setTemplateLanguage(Ljava/lang/String;)V
    //#input(Map loadAllThemesFromDisk()): this
    //#input(Map loadAllThemesFromDisk()): this.themeDir
    //#input(Map loadAllThemesFromDisk()): this.themeDir._tainted
    //#output(Map loadAllThemesFromDisk()): new HashMap(loadAllThemesFromDisk#1) num objects
    //#output(Map loadAllThemesFromDisk()): return_value
    //#new obj(Map loadAllThemesFromDisk()): new HashMap(loadAllThemesFromDisk#1)
    //#pre[4] (Map loadAllThemesFromDisk()): init'ed(this.themeDir)
    //#pre[1] (Map loadAllThemesFromDisk()): (soft) log != null
    //#pre[2] (Map loadAllThemesFromDisk()): (soft) org/apache/roller/weblogger/business/themes/SharedThemeFromDir.log != null
    //#presumption(Map loadAllThemesFromDisk()): init'ed(java.io.File.separator)
    //#presumption(Map loadAllThemesFromDisk()): themenames.length@313 <= 4_294_967_295
    //#post(Map loadAllThemesFromDisk()): return_value == &new HashMap(loadAllThemesFromDisk#1)
    //#post(Map loadAllThemesFromDisk()): new HashMap(loadAllThemesFromDisk#1) num objects == 1
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.commons.lang.StringUtils:replace
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.util.Map:put
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.roller.weblogger.pojos.ThemeTemplate:getName
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.roller.weblogger.pojos.ThemeTemplate:getLink
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.roller.weblogger.pojos.ThemeTemplate:getAction
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.io.File:exists
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.io.File:canRead
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.io.File:length
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.io.FileInputStream
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.io.InputStreamReader
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.io.InputStreamReader:read
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.lang.String
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:getName
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.commons.logging.Log:error
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.commons.logging.Log:isDebugEnabled
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.commons.logging.Log:debug
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.jdom.Element:getAttributeValue
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.jdom.Element:getChildText
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.lang.String:equalsIgnoreCase
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.commons.lang.StringUtils:isEmpty
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.util.HashSet
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.jdom.input.SAXBuilder
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.jdom.input.SAXBuilder:build
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.jdom.Document:getRootElement
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.jdom.Element:getChild
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.jdom.Element:getChildren
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.util.Set:add
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:setId
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:setName
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:setDescription
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:setAuthor
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.util.Date
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:setLastModified
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:setEnabled
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.io.File
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.commons.logging.Log:warn
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.io.File:lastModified
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.util.Set:iterator
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.roller.weblogger.WebloggerException
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.roller.RollerException
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:org.apache.roller.weblogger.business.themes.SharedTheme
    //#unanalyzed(Map loadAllThemesFromDisk()): Effects-of-calling:java.util.HashMap
    //#test_vector(Map loadAllThemesFromDisk()): java.io.File:list(...)@313: Inverse{null}, Addr_Set{null}
        
        // first, get a list of the themes available
        File themesdir = new File(this.themeDir);
        FilenameFilter filter = new FilenameFilter() {
    //#ThemeManagerImpl.java:306: method: void org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1.org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1(ThemeManagerImpl)
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1(ThemeManagerImpl)): Param_1
    //#input(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1(ThemeManagerImpl)): this
    //#output(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1(ThemeManagerImpl)): this.this$0
    //#post(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1(ThemeManagerImpl)): this.this$0 == Param_1
    //#post(void org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1(ThemeManagerImpl)): init'ed(this.this$0)
    //#ThemeManagerImpl.java:306: end of method: void org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1.org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1(ThemeManagerImpl)
            public boolean accept(File dir, String name) {
                File file =
    //#ThemeManagerImpl.java:308: method: bool org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1.accept(File, String)
    //#input(bool accept(File, String)): dir
    //#input(bool accept(File, String)): java.io.File.separator
    //#input(bool accept(File, String)): java.io.File.separator._tainted
    //#input(bool accept(File, String)): name
    //#input(bool accept(File, String)): name._tainted
    //#output(bool accept(File, String)): return_value
    //#pre[1] (bool accept(File, String)): dir != null
    //#presumption(bool accept(File, String)): init'ed(java.io.File.separator)
    //#post(bool accept(File, String)): init'ed(return_value)
                        new File(dir.getAbsolutePath() + File.separator + name);
                return file.isDirectory();
    //#ThemeManagerImpl.java:310: end of method: bool org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1.accept(File, String)
            }
        };
        String[] themenames = themesdir.list(filter);
        
        if(themenames == null) {
            log.warn("No themes loaded!  Perhaps you specified the wrong "+
    //#ThemeManagerImpl.java:316: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:warn(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: Map loadAllThemesFromDisk()
    //#    unanalyzed callee: void org.apache.commons.logging.Log:warn(Object)
                    "location for your themes directory?");
        }
        
        // now go through each theme and load it into a Theme object
        for(int i=0; i < themenames.length; i++) {
    //#ThemeManagerImpl.java:321: ?null dereference
    //#    themenames != null
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: Map loadAllThemesFromDisk()
    //#    basic block: bb_4
    //#    assertion: themenames != null
    //#    VN: java.io.File:list(...)@313
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad  Uncertain
            try {
                Theme theme = new SharedThemeFromDir(this.themeDir + File.separator + themenames[i]);
    //#ThemeManagerImpl.java:323: ?use of default init
    //#    init'ed(themenames[i])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: Map loadAllThemesFromDisk()
    //#    basic block: bb_6
    //#    assertion: init'ed(themenames[i])
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
                if(theme != null) {
    //#ThemeManagerImpl.java:324: Warning: test always goes same way
    //#    test predetermined because theme != null
    //#    severity: LOW
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: Map loadAllThemesFromDisk()
    //#    from bb: bb_6
    //#    live edge: bb_6-->bb_7
    //#    tested vn: 0
    //#    tested vn values: {0}
                    themes.put(theme.getId(), theme);
    //#ThemeManagerImpl.java:325: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.Theme:getId()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: Map loadAllThemesFromDisk()
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.Theme:getId()
                }
            } catch (Throwable unexpected) {
                // shouldn't happen, so let's learn why it did
                log.error("Problem reading theme " + themenames[i], unexpected);
    //#ThemeManagerImpl.java:329: ?use of default init
    //#    init'ed(themenames[i])
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: Map loadAllThemesFromDisk()
    //#    basic block: bb_9
    //#    assertion: init'ed(themenames[i])
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    //#ThemeManagerImpl.java:329: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:error(Object, Throwable)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
    //#    method: Map loadAllThemesFromDisk()
    //#    unanalyzed callee: void org.apache.commons.logging.Log:error(Object, Throwable)
            }
        }
        
        return themes;
    //#ThemeManagerImpl.java:333: end of method: Map org.apache.roller.weblogger.business.themes.ThemeManagerImpl.loadAllThemesFromDisk()
    }
    
}
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1__static_init): __Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeManagerImpl$1]
    //#output(org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1__static_init): __Dispatch_Table.accept(Ljava/io/File;Ljava/lang/String;)Z
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1__static_init): __Descendant_Table[org/apache/roller/weblogger/business/themes/ThemeManagerImpl$1] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1__static_init): __Dispatch_Table.accept(Ljava/io/File;Ljava/lang/String;)Z == &accept
    //#ThemeManagerImpl.java:: end of method: org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1.org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1__static_init
    //#ThemeManagerImpl.java:: end of class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl$1
    //#ThemeManagerImpl.java:: end of class: org.apache.roller.weblogger.business.themes.ThemeManagerImpl
