//# 2 errors, 740 messages
//#
package net.sourceforge.pebble.security;
    //#defaultsecurityrealm.java:1:1: class: net.sourceforge.pebble.security.DefaultSecurityRealm$1
    //#defaultsecurityrealm.java:1:1: method: net.sourceforge.pebble.security.DefaultSecurityRealm$1.net.sourceforge.pebble.security.DefaultSecurityRealm$1__static_init
    //#defaultsecurityrealm.java:1:1: class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#defaultsecurityrealm.java:1: method: void net.sourceforge.pebble.security.DefaultSecurityRealm$1.net.sourceforge.pebble.security.DefaultSecurityRealm$1(DefaultSecurityRealm)
    //#input(void net.sourceforge.pebble.security.DefaultSecurityRealm$1(DefaultSecurityRealm)): Param_1
    //#input(void net.sourceforge.pebble.security.DefaultSecurityRealm$1(DefaultSecurityRealm)): this
    //#output(void net.sourceforge.pebble.security.DefaultSecurityRealm$1(DefaultSecurityRealm)): this.this$0
    //#post(void net.sourceforge.pebble.security.DefaultSecurityRealm$1(DefaultSecurityRealm)): this.this$0 == Param_1
    //#post(void net.sourceforge.pebble.security.DefaultSecurityRealm$1(DefaultSecurityRealm)): init'ed(this.this$0)

import net.sourceforge.pebble.Configuration;
import net.sourceforge.pebble.Constants;
import net.sourceforge.pebble.comparator.PebbleUserDetailsComparator;
import org.acegisecurity.providers.dao.SaltSource;
import org.acegisecurity.providers.encoding.PasswordEncoder;
import org.apache.commons.logging.Log;
import org.apache.commons.logging.LogFactory;

import java.io.*;
import java.util.*;

/**
 * Implementation of the SecurityRealm that gets authentication
 * credentials from the blog directory.
 *
 * @author    Simon Brown
 */
public class DefaultSecurityRealm implements SecurityRealm {
    //#defaultsecurityrealm.java:20: method: void net.sourceforge.pebble.security.DefaultSecurityRealm.net.sourceforge.pebble.security.DefaultSecurityRealm()
    //#defaultsecurityrealm.java:20: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm.net.sourceforge.pebble.security.DefaultSecurityRealm()

  private static final Log log = LogFactory.getLog(DefaultSecurityRealm.class);
    //#defaultsecurityrealm.java:22: method: net.sourceforge.pebble.security.DefaultSecurityRealm.net.sourceforge.pebble.security.DefaultSecurityRealm__static_init
    //#defaultsecurityrealm.java:22: Warning: method not available
    //#    -- call on Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#    method: net.sourceforge.pebble.security.DefaultSecurityRealm__static_init
    //#    unanalyzed callee: Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.changePassword(Ljava/lang/String;Ljava/lang/String;)V
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.createUser(Lnet/sourceforge/pebble/security/PebbleUserDetails;)V
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getConfiguration()Lnet/sourceforge/pebble/Configuration;
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getFileForRealm()Ljava/io/File;
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getFileForUser(Ljava/lang/String;)Ljava/io/File;
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getPasswordEncoder()Lorg/acegisecurity/providers/encoding/PasswordEncoder;
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getSaltSource()Lorg/acegisecurity/providers/dao/SaltSource;
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getUser(Ljava/lang/String;)Lnet/sourceforge/pebble/security/PebbleUserDetails;
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getUsers()Ljava/util/Collection;
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.init()V
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.removeUser(Ljava/lang/String;)V
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.setConfiguration(Lnet/sourceforge/pebble/Configuration;)V
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.setPasswordEncoder(Lorg/acegisecurity/providers/encoding/PasswordEncoder;)V
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.setSaltSource(Lorg/acegisecurity/providers/dao/SaltSource;)V
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.updateUser(Lnet/sourceforge/pebble/security/PebbleUserDetails;)V
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.updateUser(Lnet/sourceforge/pebble/security/PebbleUserDetails;Z)V
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): log
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): net/sourceforge/pebble/security/SecurityRealm.__Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): net/sourceforge/pebble/security/SecurityRealm.__Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.changePassword(Ljava/lang/String;Ljava/lang/String;)V == &changePassword
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.createUser(Lnet/sourceforge/pebble/security/PebbleUserDetails;)V == &createUser
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getConfiguration()Lnet/sourceforge/pebble/Configuration; == &getConfiguration
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getFileForRealm()Ljava/io/File; == &getFileForRealm
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getFileForUser(Ljava/lang/String;)Ljava/io/File; == &getFileForUser
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getPasswordEncoder()Lorg/acegisecurity/providers/encoding/PasswordEncoder; == &getPasswordEncoder
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getSaltSource()Lorg/acegisecurity/providers/dao/SaltSource; == &getSaltSource
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getUser(Ljava/lang/String;)Lnet/sourceforge/pebble/security/PebbleUserDetails; == &getUser
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.getUsers()Ljava/util/Collection; == &getUsers
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.init()V == &init
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.removeUser(Ljava/lang/String;)V == &removeUser
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.setConfiguration(Lnet/sourceforge/pebble/Configuration;)V == &setConfiguration
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.setPasswordEncoder(Lorg/acegisecurity/providers/encoding/PasswordEncoder;)V == &setPasswordEncoder
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.setSaltSource(Lorg/acegisecurity/providers/dao/SaltSource;)V == &setSaltSource
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.updateUser(Lnet/sourceforge/pebble/security/PebbleUserDetails;)V == &updateUser
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): __Dispatch_Table.updateUser(Lnet/sourceforge/pebble/security/PebbleUserDetails;Z)V == &updateUser
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm__static_init): init'ed(log)
    //#defaultsecurityrealm.java:22: end of method: net.sourceforge.pebble.security.DefaultSecurityRealm.net.sourceforge.pebble.security.DefaultSecurityRealm__static_init

  private static final String REALM_DIRECTORY_NAME = "realm";

  protected static final String PASSWORD = "password";
  protected static final String ROLES = "roles";
  protected static final String NAME = "name";
  protected static final String EMAIL_ADDRESS = "emailAddress";
  protected static final String WEBSITE = "website";
  protected static final String PROFILE = "profile";
  protected static final String DETAILS_UPDATEABLE = "detailsUpdateable";
  protected static final String PREFERENCE = "preference.";

  private Configuration configuration;

  private PasswordEncoder passwordEncoder;

  private SaltSource saltSource;

  /**
   * Creates the underlying security realm upon creation, if necessary.
   */
  public void init() {
    try {
      File realm = getFileForRealm();
    //#defaultsecurityrealm.java:46: method: void net.sourceforge.pebble.security.DefaultSecurityRealm.init()
    //#input(void init()): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#input(void init()): __Descendant_Table[others]
    //#input(void init()): __Dispatch_Table.createUser(Lnet/sourceforge/pebble/security/PebbleUserDetails;)V
    //#input(void init()): __Dispatch_Table.getFileForRealm()Ljava/io/File;
    //#input(void init()): __Dispatch_Table.getFileForUser(Ljava/lang/String;)Ljava/io/File;
    //#input(void init()): __Dispatch_Table.getUser(Ljava/lang/String;)Lnet/sourceforge/pebble/security/PebbleUserDetails;
    //#input(void init()): log
    //#input(void init()): net.sourceforge.pebble.Constants.BLOG_ADMIN_ROLE
    //#input(void init()): net.sourceforge.pebble.Constants.BLOG_CONTRIBUTOR_ROLE
    //#input(void init()): net.sourceforge.pebble.Constants.BLOG_OWNER_ROLE
    //#input(void init()): net.sourceforge.pebble.Constants.BLOG_PUBLISHER_ROLE
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Descendant_Table[others]
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getEmailAddress()Ljava/lang/String;
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getPassword()Ljava/lang/String;
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getPreferences()Ljava/util/Map;
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getProfile()Ljava/lang/String;
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getRolesAsString()Ljava/lang/String;
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getUsername()Ljava/lang/String;
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getWebsite()Ljava/lang/String;
    //#input(void init()): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.isDetailsUpdateable()Z
    //#input(void init()): this
    //#input(void init()): this.__Tag
    //#input(void init()): this.configuration
    //#input(void init()): this.passwordEncoder
    //#input(void init()): this.saltSource
    //#pre[2] (void init()): (soft) this.__Tag == net/sourceforge/pebble/security/DefaultSecurityRealm
    //#pre[3] (void init()): (soft) this.configuration != null
    //#pre[4] (void init()): (soft) this.passwordEncoder != null
    //#pre[5] (void init()): (soft) this.saltSource != null
    //#presumption(void init()): defaultUser.grantedAuthories.length <= 4_294_967_295
    //#presumption(void init()): defaultUser.grantedAuthories[0..4_294_967_295] != null
    //#presumption(void init()): java.util.Set:toArray(...)@194 != null
    //#presumption(void init()): net.sourceforge.pebble.Constants.BLOG_ADMIN_ROLE != null
    //#presumption(void init()): net.sourceforge.pebble.Constants.BLOG_CONTRIBUTOR_ROLE != null
    //#presumption(void init()): net.sourceforge.pebble.Constants.BLOG_OWNER_ROLE != null
    //#presumption(void init()): net.sourceforge.pebble.Constants.BLOG_PUBLISHER_ROLE != null
    //#presumption(void init()): org.apache.commons.logging.LogFactory:getLog(...)@22 != null
    //#unanalyzed(void init()): Effects-of-calling:net.sourceforge.pebble.Configuration:getDataDirectory
    //#unanalyzed(void init()): Effects-of-calling:java.io.File
    //#unanalyzed(void init()): Effects-of-calling:getUser
    //#unanalyzed(void init()): Effects-of-calling:updateUser
    //#unanalyzed(void init()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void init()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void init()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void init()): Effects-of-calling:net.sourceforge.pebble.PebbleException
    //#unanalyzed(void init()): Effects-of-calling:getFileForUser
    //#unanalyzed(void init()): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void init()): Effects-of-calling:java.io.FileInputStream
    //#unanalyzed(void init()): Effects-of-calling:java.util.Properties
    //#unanalyzed(void init()): Effects-of-calling:java.util.Properties:load
    //#unanalyzed(void init()): Effects-of-calling:java.io.FileInputStream:close
    //#unanalyzed(void init()): Effects-of-calling:java.util.Properties:getProperty
    //#unanalyzed(void init()): Effects-of-calling:java.lang.String:split
    //#unanalyzed(void init()): Effects-of-calling:java.lang.String:equalsIgnoreCase
    //#unanalyzed(void init()): Effects-of-calling:java.util.HashMap
    //#unanalyzed(void init()): Effects-of-calling:java.util.Properties:keySet
    //#unanalyzed(void init()): Effects-of-calling:java.util.Set:iterator
    //#unanalyzed(void init()): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void init()): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void init()): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void init()): Effects-of-calling:java.lang.String:length
    //#unanalyzed(void init()): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void init()): Effects-of-calling:java.util.Map:put
    //#unanalyzed(void init()): Effects-of-calling:java.util.HashSet
    //#unanalyzed(void init()): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(void init()): Effects-of-calling:org.acegisecurity.GrantedAuthorityImpl
    //#unanalyzed(void init()): Effects-of-calling:java.util.Set:add
    //#unanalyzed(void init()): Effects-of-calling:java.util.Set:toArray
    //#unanalyzed(void init()): Effects-of-calling:java.lang.String:valueOf
    //#unanalyzed(void init()): Effects-of-calling:org.acegisecurity.providers.dao.SaltSource:getSalt
    //#unanalyzed(void init()): Effects-of-calling:org.acegisecurity.providers.encoding.PasswordEncoder:encodePassword
    //#unanalyzed(void init()): Effects-of-calling:java.util.Properties:setProperty
    //#unanalyzed(void init()): Effects-of-calling:java.lang.StringBuffer
    //#unanalyzed(void init()): Effects-of-calling:org.acegisecurity.GrantedAuthority:getAuthority
    //#unanalyzed(void init()): Effects-of-calling:java.lang.StringBuffer:append
    //#unanalyzed(void init()): Effects-of-calling:java.lang.StringBuffer:toString
    //#unanalyzed(void init()): Effects-of-calling:java.util.Map:keySet
    //#unanalyzed(void init()): Effects-of-calling:java.util.Map:get
    //#unanalyzed(void init()): Effects-of-calling:java.io.FileOutputStream
    //#unanalyzed(void init()): Effects-of-calling:java.util.Properties:store
    //#unanalyzed(void init()): Effects-of-calling:java.io.FileOutputStream:flush
    //#unanalyzed(void init()): Effects-of-calling:java.io.FileOutputStream:close
    //#test_vector(void init()): java.io.File:exists(...)@47: {1}, {0}
      if (!realm.exists()) {
        realm.mkdirs();
        log.warn("*** Creating default user (username/password)");
    //#defaultsecurityrealm.java:49: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:warn(Object)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#    method: void init()
    //#    unanalyzed callee: void org.apache.commons.logging.Log:warn(Object)
        log.warn("*** Don't forget to delete this user in a production deployment!");
    //#defaultsecurityrealm.java:50: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:warn(Object)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#    method: void init()
    //#    unanalyzed callee: void org.apache.commons.logging.Log:warn(Object)
        PebbleUserDetails defaultUser = new PebbleUserDetails("username", "password", "Default User", "username@domain.com", "http://www.domain.com", "Default User...", new String[] {Constants.BLOG_OWNER_ROLE, Constants.BLOG_PUBLISHER_ROLE, Constants.BLOG_CONTRIBUTOR_ROLE, Constants.BLOG_ADMIN_ROLE}, new HashMap<String,String>(), true);
    //#defaultsecurityrealm.java:51: ?precondition failure
    //#    net/sourceforge/pebble/security/PebbleUserDetails.net.sourceforge.pebble.security.PebbleUserDetails: (soft) roles[0..4_294_967_295] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#    method: void init()
    //#    basic block: bb_3
    //#    assertion: (soft) net.sourceforge.pebble.security.PebbleUserDetails.Param_7[0..4_294_967_295] != null
    //#    callee: void net/sourceforge/pebble/security/PebbleUserDetails.net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)
    //#    callee assertion: (soft) roles[0..4_294_967_295] != null
    //#    callee file: pebbleuserdetails.java
    //#    callee precondition index: [9]
    //#    callee srcpos: 57
    //#    VN: net.sourceforge.pebble.security.PebbleUserDetails.Param_7[0..4_294_967_295]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null, Invalid}
    //#    Attribs:  Ptr  null in Bad  Soft  Uncertain
        createUser(defaultUser);
      }
    } catch (SecurityRealmException e) {
      log.error("Error while creating security realm", e);
    //#defaultsecurityrealm.java:55: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:error(Object, Throwable)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#    method: void init()
    //#    unanalyzed callee: void org.apache.commons.logging.Log:error(Object, Throwable)
    }

  }
    //#defaultsecurityrealm.java:58: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm.init()

  /**
   * Looks up and returns a collection of all users.
   *
   * @return  a Collection of PebbleUserDetails objects
   */
  public synchronized Collection<PebbleUserDetails> getUsers() throws SecurityRealmException {
    LinkedList<PebbleUserDetails> users = new LinkedList<PebbleUserDetails>();
    //#defaultsecurityrealm.java:66: method: Collection net.sourceforge.pebble.security.DefaultSecurityRealm.getUsers()
    //#input(Collection getUsers()): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#input(Collection getUsers()): __Descendant_Table[others]
    //#input(Collection getUsers()): __Dispatch_Table.getFileForRealm()Ljava/io/File;
    //#input(Collection getUsers()): __Dispatch_Table.getFileForUser(Ljava/lang/String;)Ljava/io/File;
    //#input(Collection getUsers()): __Dispatch_Table.getUser(Ljava/lang/String;)Lnet/sourceforge/pebble/security/PebbleUserDetails;
    //#input(Collection getUsers()): this
    //#input(Collection getUsers()): this.__Tag
    //#input(Collection getUsers()): this.configuration
    //#output(Collection getUsers()): new LinkedList(getUsers#1) num objects
    //#output(Collection getUsers()): return_value
    //#new obj(Collection getUsers()): new LinkedList(getUsers#1)
    //#pre[2] (Collection getUsers()): this.__Tag == net/sourceforge/pebble/security/DefaultSecurityRealm
    //#pre[3] (Collection getUsers()): this.configuration != null
    //#presumption(Collection getUsers()): Local_7[Local_5]@68 != null
    //#presumption(Collection getUsers()): files.length@68 <= 4_294_967_295
    //#presumption(Collection getUsers()): java.io.File:getName(...)@83 != null
    //#presumption(Collection getUsers()): java.io.File:getName(...)@83 != null
    //#presumption(Collection getUsers()): java.io.File:listFiles(...)@68 != null
    //#post(Collection getUsers()): return_value == &new LinkedList(getUsers#1)
    //#post(Collection getUsers()): new LinkedList(getUsers#1) num objects == 1
    //#unanalyzed(Collection getUsers()): Effects-of-calling:net.sourceforge.pebble.Configuration:getDataDirectory
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.io.File
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(Collection getUsers()): Effects-of-calling:getFileForUser
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.io.File:exists
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.io.FileInputStream
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.Properties
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.Properties:load
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.io.FileInputStream:close
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.Properties:getProperty
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.lang.String:split
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.lang.String:equalsIgnoreCase
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.HashMap
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.Properties:keySet
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.Set:iterator
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.lang.String:length
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.Map:put
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.HashSet
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(Collection getUsers()): Effects-of-calling:org.acegisecurity.GrantedAuthorityImpl
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.Set:add
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.util.Set:toArray
    //#unanalyzed(Collection getUsers()): Effects-of-calling:net.sourceforge.pebble.PebbleException
    //#unanalyzed(Collection getUsers()): Effects-of-calling:java.lang.String:valueOf
    File realm = getFileForRealm();
    File files[] = realm.listFiles(new FilenameFilter() {
    //#defaultsecurityrealm.java:68: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm$1.net.sourceforge.pebble.security.DefaultSecurityRealm$1(DefaultSecurityRealm)
      /**
       * Tests if a specified file should be included in a file list.
       *
       * @param dir  the directory in which the file was found.
       * @param name the name of the file.
       * @return <code>true</code> if and only if the name should be
       *         included in the file list; <code>false</code> otherwise.
       */
      public boolean accept(File dir, String name) {
        return name.endsWith(".properties");
    //#defaultsecurityrealm.java:78: method: bool net.sourceforge.pebble.security.DefaultSecurityRealm$1.accept(File, String)
    //#input(bool accept(File, String)): name
    //#output(bool accept(File, String)): return_value
    //#pre[1] (bool accept(File, String)): name != null
    //#post(bool accept(File, String)): init'ed(return_value)
    //#defaultsecurityrealm.java:78: end of method: bool net.sourceforge.pebble.security.DefaultSecurityRealm$1.accept(File, String)
      }
    });

    for (File file : files) {
      PebbleUserDetails pud = getUser(file.getName().substring(0, file.getName().lastIndexOf(".")));
      if (pud != null) {
        users.add(pud);
      }
    }

    Collections.sort(users, new PebbleUserDetailsComparator());
    //#defaultsecurityrealm.java:89: Warning: method not available
    //#    -- call on void net.sourceforge.pebble.comparator.PebbleUserDetailsComparator()
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#    method: Collection getUsers()
    //#    unanalyzed callee: void net.sourceforge.pebble.comparator.PebbleUserDetailsComparator()

    return users;
    //#defaultsecurityrealm.java:91: end of method: Collection net.sourceforge.pebble.security.DefaultSecurityRealm.getUsers()
  }

  /**
   * Looks up and returns user details for the given username.
   *
   * @param username the username to find details for
   * @return a PebbleUserDetails instance
   *
   */
  public synchronized PebbleUserDetails getUser(String username) throws SecurityRealmException {
    File user = getFileForUser(username);
    //#defaultsecurityrealm.java:102: method: PebbleUserDetails net.sourceforge.pebble.security.DefaultSecurityRealm.getUser(String)
    //#input(PebbleUserDetails getUser(String)): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#input(PebbleUserDetails getUser(String)): __Descendant_Table[others]
    //#input(PebbleUserDetails getUser(String)): __Dispatch_Table.getFileForRealm()Ljava/io/File;
    //#input(PebbleUserDetails getUser(String)): __Dispatch_Table.getFileForUser(Ljava/lang/String;)Ljava/io/File;
    //#input(PebbleUserDetails getUser(String)): this
    //#input(PebbleUserDetails getUser(String)): this.__Tag
    //#input(PebbleUserDetails getUser(String)): this.configuration
    //#input(PebbleUserDetails getUser(String)): username
    //#output(PebbleUserDetails getUser(String)): new HashMap(PebbleUserDetails#1) num objects
    //#output(PebbleUserDetails getUser(String)): new HashMap(getUser#3) num objects
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4) num objects
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).__Tag
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).detailsUpdateable
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).emailAddress
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).grantedAuthories
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).name
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).password
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).preferences
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).profile
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).username
    //#output(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).website
    //#output(PebbleUserDetails getUser(String)): return_value
    //#new obj(PebbleUserDetails getUser(String)): new HashMap(PebbleUserDetails#1)
    //#new obj(PebbleUserDetails getUser(String)): new HashMap(getUser#3)
    //#new obj(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4)
    //#pre[2] (PebbleUserDetails getUser(String)): this.__Tag == net/sourceforge/pebble/security/DefaultSecurityRealm
    //#pre[3] (PebbleUserDetails getUser(String)): this.configuration != null
    //#presumption(PebbleUserDetails getUser(String)): java.util.Iterator:next(...)@126 != null
    //#presumption(PebbleUserDetails getUser(String)): java.util.Properties:getProperty(...)@114 != null
    //#presumption(PebbleUserDetails getUser(String)): java.util.Properties:keySet(...)@126 != null
    //#presumption(PebbleUserDetails getUser(String)): roles.length@114 <= 4_294_967_295
    //#presumption(PebbleUserDetails getUser(String)): roles[0..4_294_967_295]@114 != null
    //#post(PebbleUserDetails getUser(String)): return_value in Addr_Set{null,&new PebbleUserDetails(getUser#4)}
    //#post(PebbleUserDetails getUser(String)): new HashMap(PebbleUserDetails#1) num objects <= 1
    //#post(PebbleUserDetails getUser(String)): new HashMap(getUser#3) num objects <= 1
    //#post(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4) num objects <= 1
    //#post(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#post(PebbleUserDetails getUser(String)): init'ed(new PebbleUserDetails(getUser#4).detailsUpdateable)
    //#post(PebbleUserDetails getUser(String)): init'ed(new PebbleUserDetails(getUser#4).emailAddress)
    //#post(PebbleUserDetails getUser(String)): init'ed(new PebbleUserDetails(getUser#4).grantedAuthories)
    //#post(PebbleUserDetails getUser(String)): init'ed(new PebbleUserDetails(getUser#4).name)
    //#post(PebbleUserDetails getUser(String)): init'ed(new PebbleUserDetails(getUser#4).password)
    //#post(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).preferences == &new HashMap(getUser#3)
    //#post(PebbleUserDetails getUser(String)): init'ed(new PebbleUserDetails(getUser#4).profile)
    //#post(PebbleUserDetails getUser(String)): new PebbleUserDetails(getUser#4).username == username
    //#post(PebbleUserDetails getUser(String)): init'ed(new PebbleUserDetails(getUser#4).username)
    //#post(PebbleUserDetails getUser(String)): init'ed(new PebbleUserDetails(getUser#4).website)
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:net.sourceforge.pebble.Configuration:getDataDirectory
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:java.io.File
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:java.util.HashMap
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:java.util.HashSet
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:org.acegisecurity.GrantedAuthorityImpl
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:java.util.Set:add
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:java.util.Set:toArray
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:net.sourceforge.pebble.PebbleException
    //#unanalyzed(PebbleUserDetails getUser(String)): Effects-of-calling:java.lang.String:valueOf
    //#test_vector(PebbleUserDetails getUser(String)): java.io.File:exists(...)@103: {1}, {0}
    //#test_vector(PebbleUserDetails getUser(String)): java.lang.String:startsWith(...)@128: {0}, {1}
    //#test_vector(PebbleUserDetails getUser(String)): java.util.Iterator:hasNext(...)@126: {1}, {0}
    //#test_vector(PebbleUserDetails getUser(String)): java.util.Properties:getProperty(...)@119: Addr_Set{null}, Inverse{null}
    if (!user.exists()) {
      return null;
    }

    try {
      FileInputStream in = new FileInputStream(user);
      Properties props = new Properties();
      props.load(in);
      in.close();

      String password = props.getProperty(PASSWORD);
      String[] roles = props.getProperty(ROLES).split(",");
      String name = props.getProperty(NAME);
      String emailAddress = props.getProperty(EMAIL_ADDRESS);
      String website = props.getProperty(WEBSITE);
      String profile = props.getProperty(PROFILE);
      String detailsUpdateableAsString = props.getProperty(DETAILS_UPDATEABLE);
      boolean detailsUpdateable = true;
      if (detailsUpdateableAsString != null) {
        detailsUpdateable = detailsUpdateableAsString.equalsIgnoreCase("true");
      }

      Map<String,String> preferences = new HashMap<String,String>();
      for (Object key : props.keySet()) {
        String propertyName = (String)key;
        if (propertyName.startsWith(PREFERENCE)) {
          preferences.put(propertyName.substring(PREFERENCE.length()), props.getProperty(propertyName));          
        }
      }

      return new PebbleUserDetails(username, password, name, emailAddress, website, profile, roles, preferences, detailsUpdateable);
    } catch (IOException ioe) {
      throw new SecurityRealmException(ioe);
    //#defaultsecurityrealm.java:135: end of method: PebbleUserDetails net.sourceforge.pebble.security.DefaultSecurityRealm.getUser(String)
    }
  }

  /**
   * Creates a new user.
   *
   * @param pud   a PebbleUserDetails instance
   */
  public synchronized void createUser(PebbleUserDetails pud) throws SecurityRealmException {
    if (getUser(pud.getUsername()) == null) {
    //#defaultsecurityrealm.java:145: method: void net.sourceforge.pebble.security.DefaultSecurityRealm.createUser(PebbleUserDetails)
    //#input(void createUser(PebbleUserDetails)): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#input(void createUser(PebbleUserDetails)): __Descendant_Table[others]
    //#input(void createUser(PebbleUserDetails)): __Dispatch_Table.getFileForRealm()Ljava/io/File;
    //#input(void createUser(PebbleUserDetails)): __Dispatch_Table.getFileForUser(Ljava/lang/String;)Ljava/io/File;
    //#input(void createUser(PebbleUserDetails)): __Dispatch_Table.getUser(Ljava/lang/String;)Lnet/sourceforge/pebble/security/PebbleUserDetails;
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Descendant_Table[others]
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getEmailAddress()Ljava/lang/String;
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getPassword()Ljava/lang/String;
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getPreferences()Ljava/util/Map;
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getProfile()Ljava/lang/String;
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getRolesAsString()Ljava/lang/String;
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getUsername()Ljava/lang/String;
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getWebsite()Ljava/lang/String;
    //#input(void createUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.isDetailsUpdateable()Z
    //#input(void createUser(PebbleUserDetails)): pud
    //#input(void createUser(PebbleUserDetails)): pud.__Tag
    //#input(void createUser(PebbleUserDetails)): pud.detailsUpdateable
    //#input(void createUser(PebbleUserDetails)): pud.emailAddress
    //#input(void createUser(PebbleUserDetails)): pud.grantedAuthories
    //#input(void createUser(PebbleUserDetails)): pud.grantedAuthories.length
    //#input(void createUser(PebbleUserDetails)): pud.grantedAuthories[0..4_294_967_295]
    //#input(void createUser(PebbleUserDetails)): pud.name
    //#input(void createUser(PebbleUserDetails)): pud.password
    //#input(void createUser(PebbleUserDetails)): pud.preferences
    //#input(void createUser(PebbleUserDetails)): pud.profile
    //#input(void createUser(PebbleUserDetails)): pud.username
    //#input(void createUser(PebbleUserDetails)): pud.website
    //#input(void createUser(PebbleUserDetails)): this
    //#input(void createUser(PebbleUserDetails)): this.__Tag
    //#input(void createUser(PebbleUserDetails)): this.configuration
    //#input(void createUser(PebbleUserDetails)): this.passwordEncoder
    //#input(void createUser(PebbleUserDetails)): this.saltSource
    //#pre[1] (void createUser(PebbleUserDetails)): pud != null
    //#pre[2] (void createUser(PebbleUserDetails)): pud.__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#pre[3] (void createUser(PebbleUserDetails)): init'ed(pud.detailsUpdateable)
    //#pre[4] (void createUser(PebbleUserDetails)): init'ed(pud.emailAddress)
    //#pre[5] (void createUser(PebbleUserDetails)): pud.grantedAuthories != null
    //#pre[6] (void createUser(PebbleUserDetails)): pud.grantedAuthories.length <= 4_294_967_295
    //#pre[8] (void createUser(PebbleUserDetails)): init'ed(pud.name)
    //#pre[10] (void createUser(PebbleUserDetails)): init'ed(pud.preferences)
    //#pre[11] (void createUser(PebbleUserDetails)): init'ed(pud.profile)
    //#pre[12] (void createUser(PebbleUserDetails)): init'ed(pud.username)
    //#pre[13] (void createUser(PebbleUserDetails)): init'ed(pud.website)
    //#pre[15] (void createUser(PebbleUserDetails)): this.__Tag == net/sourceforge/pebble/security/DefaultSecurityRealm
    //#pre[16] (void createUser(PebbleUserDetails)): this.configuration != null
    //#pre[7] (void createUser(PebbleUserDetails)): (soft) pud.grantedAuthories[0..4_294_967_295] != null
    //#pre[9] (void createUser(PebbleUserDetails)): (soft) init'ed(pud.password)
    //#pre[17] (void createUser(PebbleUserDetails)): (soft) this.passwordEncoder != null
    //#pre[18] (void createUser(PebbleUserDetails)): (soft) this.saltSource != null
    //#presumption(void createUser(PebbleUserDetails)): java.io.File:exists(...)@103 == 0
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:net.sourceforge.pebble.Configuration:getDataDirectory
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.io.File
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:net.sourceforge.pebble.PebbleException
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:getFileForUser
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.io.FileInputStream
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties:load
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.io.FileInputStream:close
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties:getProperty
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:split
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:equalsIgnoreCase
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.HashMap
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties:keySet
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Set:iterator
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Map:put
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.HashSet
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:org.acegisecurity.GrantedAuthorityImpl
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Set:add
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Set:toArray
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:valueOf
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:org.acegisecurity.providers.dao.SaltSource:getSalt
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:org.acegisecurity.providers.encoding.PasswordEncoder:encodePassword
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties:setProperty
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuffer
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:org.acegisecurity.GrantedAuthority:getAuthority
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuffer:append
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuffer:toString
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Map:keySet
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Map:get
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.io.FileOutputStream
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties:store
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.io.FileOutputStream:flush
    //#unanalyzed(void createUser(PebbleUserDetails)): Effects-of-calling:java.io.FileOutputStream:close
      updateUser(pud, true);
    } else {
      throw new SecurityRealmException("User " + pud.getUsername() + " already exists");
    }
  }
    //#defaultsecurityrealm.java:150: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm.createUser(PebbleUserDetails)

  /**
   * Updates user details.
   *
   * @param pud   a PebbleUserDetails instance
   */
  public synchronized void updateUser(PebbleUserDetails pud) throws SecurityRealmException {
    updateUser(pud, false);
    //#defaultsecurityrealm.java:158: method: void net.sourceforge.pebble.security.DefaultSecurityRealm.updateUser(PebbleUserDetails)
    //#input(void updateUser(PebbleUserDetails)): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#input(void updateUser(PebbleUserDetails)): __Descendant_Table[others]
    //#input(void updateUser(PebbleUserDetails)): __Dispatch_Table.getFileForRealm()Ljava/io/File;
    //#input(void updateUser(PebbleUserDetails)): __Dispatch_Table.getFileForUser(Ljava/lang/String;)Ljava/io/File;
    //#input(void updateUser(PebbleUserDetails)): __Dispatch_Table.getUser(Ljava/lang/String;)Lnet/sourceforge/pebble/security/PebbleUserDetails;
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Descendant_Table[others]
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getEmailAddress()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getPassword()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getPreferences()Ljava/util/Map;
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getProfile()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getRolesAsString()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getUsername()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getWebsite()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.isDetailsUpdateable()Z
    //#input(void updateUser(PebbleUserDetails)): pud
    //#input(void updateUser(PebbleUserDetails)): pud.__Tag
    //#input(void updateUser(PebbleUserDetails)): pud.detailsUpdateable
    //#input(void updateUser(PebbleUserDetails)): pud.emailAddress
    //#input(void updateUser(PebbleUserDetails)): pud.grantedAuthories
    //#input(void updateUser(PebbleUserDetails)): pud.grantedAuthories.length
    //#input(void updateUser(PebbleUserDetails)): pud.grantedAuthories[0..4_294_967_295]
    //#input(void updateUser(PebbleUserDetails)): pud.name
    //#input(void updateUser(PebbleUserDetails)): pud.password
    //#input(void updateUser(PebbleUserDetails)): pud.preferences
    //#input(void updateUser(PebbleUserDetails)): pud.profile
    //#input(void updateUser(PebbleUserDetails)): pud.username
    //#input(void updateUser(PebbleUserDetails)): pud.website
    //#input(void updateUser(PebbleUserDetails)): this
    //#input(void updateUser(PebbleUserDetails)): this.__Tag
    //#input(void updateUser(PebbleUserDetails)): this.configuration
    //#input(void updateUser(PebbleUserDetails)): this.passwordEncoder
    //#input(void updateUser(PebbleUserDetails)): this.saltSource
    //#pre[1] (void updateUser(PebbleUserDetails)): pud != null
    //#pre[2] (void updateUser(PebbleUserDetails)): pud.__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#pre[3] (void updateUser(PebbleUserDetails)): init'ed(pud.detailsUpdateable)
    //#pre[4] (void updateUser(PebbleUserDetails)): init'ed(pud.emailAddress)
    //#pre[5] (void updateUser(PebbleUserDetails)): pud.grantedAuthories != null
    //#pre[6] (void updateUser(PebbleUserDetails)): pud.grantedAuthories.length <= 4_294_967_295
    //#pre[8] (void updateUser(PebbleUserDetails)): init'ed(pud.name)
    //#pre[10] (void updateUser(PebbleUserDetails)): init'ed(pud.preferences)
    //#pre[11] (void updateUser(PebbleUserDetails)): init'ed(pud.profile)
    //#pre[12] (void updateUser(PebbleUserDetails)): init'ed(pud.username)
    //#pre[13] (void updateUser(PebbleUserDetails)): init'ed(pud.website)
    //#pre[15] (void updateUser(PebbleUserDetails)): this.__Tag == net/sourceforge/pebble/security/DefaultSecurityRealm
    //#pre[16] (void updateUser(PebbleUserDetails)): this.configuration != null
    //#pre[7] (void updateUser(PebbleUserDetails)): (soft) pud.grantedAuthories[0..4_294_967_295] != null
    //#pre[9] (void updateUser(PebbleUserDetails)): (soft) init'ed(pud.password)
    //#pre[17] (void updateUser(PebbleUserDetails)): (soft) this.passwordEncoder != null
    //#pre[18] (void updateUser(PebbleUserDetails)): (soft) this.saltSource != null
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:net.sourceforge.pebble.Configuration:getDataDirectory
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.io.File
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:getFileForUser
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.io.FileInputStream
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties:load
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.io.FileInputStream:close
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties:getProperty
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:split
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:equalsIgnoreCase
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.HashMap
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties:keySet
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Set:iterator
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Map:put
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.HashSet
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:org.acegisecurity.GrantedAuthorityImpl
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Set:add
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Set:toArray
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:net.sourceforge.pebble.PebbleException
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.String:valueOf
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:org.acegisecurity.providers.dao.SaltSource:getSalt
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:org.acegisecurity.providers.encoding.PasswordEncoder:encodePassword
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties:setProperty
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuffer
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:org.acegisecurity.GrantedAuthority:getAuthority
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuffer:append
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.lang.StringBuffer:toString
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Map:keySet
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Map:get
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.io.FileOutputStream
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.util.Properties:store
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.io.FileOutputStream:flush
    //#unanalyzed(void updateUser(PebbleUserDetails)): Effects-of-calling:java.io.FileOutputStream:close
  }
    //#defaultsecurityrealm.java:159: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm.updateUser(PebbleUserDetails)

  /**
   * Updates user details, except for the password
   *
   * @param pud   a PebbleUserDetails instance
   */
  private void updateUser(PebbleUserDetails pud, boolean updatePassword) throws SecurityRealmException {
    File user = getFileForUser(pud.getUsername());
    //#defaultsecurityrealm.java:167: method: void net.sourceforge.pebble.security.DefaultSecurityRealm.updateUser(PebbleUserDetails, bool)
    //#input(void updateUser(PebbleUserDetails, bool)): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#input(void updateUser(PebbleUserDetails, bool)): __Descendant_Table[others]
    //#input(void updateUser(PebbleUserDetails, bool)): __Dispatch_Table.getFileForRealm()Ljava/io/File;
    //#input(void updateUser(PebbleUserDetails, bool)): __Dispatch_Table.getFileForUser(Ljava/lang/String;)Ljava/io/File;
    //#input(void updateUser(PebbleUserDetails, bool)): __Dispatch_Table.getUser(Ljava/lang/String;)Lnet/sourceforge/pebble/security/PebbleUserDetails;
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Descendant_Table[others]
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getEmailAddress()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getPassword()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getPreferences()Ljava/util/Map;
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getProfile()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getRolesAsString()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getUsername()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getWebsite()Ljava/lang/String;
    //#input(void updateUser(PebbleUserDetails, bool)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.isDetailsUpdateable()Z
    //#input(void updateUser(PebbleUserDetails, bool)): pud
    //#input(void updateUser(PebbleUserDetails, bool)): pud.__Tag
    //#input(void updateUser(PebbleUserDetails, bool)): pud.detailsUpdateable
    //#input(void updateUser(PebbleUserDetails, bool)): pud.emailAddress
    //#input(void updateUser(PebbleUserDetails, bool)): pud.grantedAuthories
    //#input(void updateUser(PebbleUserDetails, bool)): pud.grantedAuthories.length
    //#input(void updateUser(PebbleUserDetails, bool)): pud.grantedAuthories[0..4_294_967_295]
    //#input(void updateUser(PebbleUserDetails, bool)): pud.name
    //#input(void updateUser(PebbleUserDetails, bool)): pud.password
    //#input(void updateUser(PebbleUserDetails, bool)): pud.preferences
    //#input(void updateUser(PebbleUserDetails, bool)): pud.profile
    //#input(void updateUser(PebbleUserDetails, bool)): pud.username
    //#input(void updateUser(PebbleUserDetails, bool)): pud.website
    //#input(void updateUser(PebbleUserDetails, bool)): this
    //#input(void updateUser(PebbleUserDetails, bool)): this.__Tag
    //#input(void updateUser(PebbleUserDetails, bool)): this.configuration
    //#input(void updateUser(PebbleUserDetails, bool)): this.passwordEncoder
    //#input(void updateUser(PebbleUserDetails, bool)): this.saltSource
    //#input(void updateUser(PebbleUserDetails, bool)): updatePassword
    //#pre[1] (void updateUser(PebbleUserDetails, bool)): pud != null
    //#pre[2] (void updateUser(PebbleUserDetails, bool)): pud.__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#pre[3] (void updateUser(PebbleUserDetails, bool)): init'ed(pud.detailsUpdateable)
    //#pre[4] (void updateUser(PebbleUserDetails, bool)): init'ed(pud.emailAddress)
    //#pre[5] (void updateUser(PebbleUserDetails, bool)): pud.grantedAuthories != null
    //#pre[6] (void updateUser(PebbleUserDetails, bool)): pud.grantedAuthories.length <= 4_294_967_295
    //#pre[8] (void updateUser(PebbleUserDetails, bool)): init'ed(pud.name)
    //#pre[10] (void updateUser(PebbleUserDetails, bool)): init'ed(pud.preferences)
    //#pre[11] (void updateUser(PebbleUserDetails, bool)): init'ed(pud.profile)
    //#pre[12] (void updateUser(PebbleUserDetails, bool)): init'ed(pud.username)
    //#pre[13] (void updateUser(PebbleUserDetails, bool)): init'ed(pud.website)
    //#pre[15] (void updateUser(PebbleUserDetails, bool)): this.__Tag == net/sourceforge/pebble/security/DefaultSecurityRealm
    //#pre[16] (void updateUser(PebbleUserDetails, bool)): this.configuration != null
    //#pre[7] (void updateUser(PebbleUserDetails, bool)): (soft) pud.grantedAuthories[0..4_294_967_295] != null
    //#pre[9] (void updateUser(PebbleUserDetails, bool)): (soft) init'ed(pud.password)
    //#pre[17] (void updateUser(PebbleUserDetails, bool)): (soft) this.passwordEncoder != null
    //#pre[18] (void updateUser(PebbleUserDetails, bool)): (soft) this.saltSource != null
    //#presumption(void updateUser(PebbleUserDetails, bool)): java.io.File:exists(...)@103 == 1
    //#presumption(void updateUser(PebbleUserDetails, bool)): java.util.Iterator:hasNext(...)@126 == 0
    //#presumption(void updateUser(PebbleUserDetails, bool)): java.util.Map:keySet(...)@184 != null
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:net.sourceforge.pebble.Configuration:getDataDirectory
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.io.File
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:getFileForUser
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.io.FileInputStream
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.Properties
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.Properties:load
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.io.FileInputStream:close
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.Properties:getProperty
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.String:split
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.String:equalsIgnoreCase
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.HashMap
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.Properties:keySet
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.Set:iterator
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.Map:put
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.HashSet
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:org.acegisecurity.GrantedAuthorityImpl
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.Set:add
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.util.Set:toArray
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:net.sourceforge.pebble.PebbleException
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.String:valueOf
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.StringBuffer
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:org.acegisecurity.GrantedAuthority:getAuthority
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.StringBuffer:append
    //#unanalyzed(void updateUser(PebbleUserDetails, bool)): Effects-of-calling:java.lang.StringBuffer:toString
    //#test_vector(void updateUser(PebbleUserDetails, bool)): updatePassword: {0}, {1}
    //#test_vector(void updateUser(PebbleUserDetails, bool)): java.util.Iterator:hasNext(...)@184: {1}, {0}
    PebbleUserDetails currentDetails = getUser(pud.getUsername());

    Properties props = new Properties();
    if (updatePassword) {
      props.setProperty(DefaultSecurityRealm.PASSWORD, passwordEncoder.encodePassword(pud.getPassword(), saltSource.getSalt(pud)));
    //#defaultsecurityrealm.java:172: Warning: method not available
    //#    -- call on Object org.acegisecurity.providers.dao.SaltSource:getSalt(UserDetails)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#    method: void updateUser(PebbleUserDetails, bool)
    //#    unanalyzed callee: Object org.acegisecurity.providers.dao.SaltSource:getSalt(UserDetails)
    //#defaultsecurityrealm.java:172: Warning: method not available
    //#    -- call on String org.acegisecurity.providers.encoding.PasswordEncoder:encodePassword(String, Object)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#    method: void updateUser(PebbleUserDetails, bool)
    //#    unanalyzed callee: String org.acegisecurity.providers.encoding.PasswordEncoder:encodePassword(String, Object)
    } else {
      props.setProperty(DefaultSecurityRealm.PASSWORD, currentDetails.getPassword());
    }
    props.setProperty(DefaultSecurityRealm.ROLES, pud.getRolesAsString());
    props.setProperty(DefaultSecurityRealm.NAME, pud.getName());
    props.setProperty(DefaultSecurityRealm.EMAIL_ADDRESS, pud.getEmailAddress());
    props.setProperty(DefaultSecurityRealm.WEBSITE, pud.getWebsite());
    props.setProperty(DefaultSecurityRealm.PROFILE, pud.getProfile());
    props.setProperty(DefaultSecurityRealm.DETAILS_UPDATEABLE, "" + pud.isDetailsUpdateable());

    Map<String,String> preferences = pud.getPreferences();
    for (String preference : preferences.keySet()) {
      props.setProperty(DefaultSecurityRealm.PREFERENCE + preference, preferences.get(preference));
    }

    try {
      FileOutputStream out = new FileOutputStream(user);
      props.store(out, "User : " + pud.getUsername());
      out.flush();
      out.close();
    } catch (IOException ioe) {
      throw new SecurityRealmException(ioe);
    }
  }
    //#defaultsecurityrealm.java:196: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm.updateUser(PebbleUserDetails, bool)

  /**
   * Changes a user's password.
   *
   * @param username    the username of the user
   * @param password    the new password
   * @throws SecurityRealmException
   */
  public synchronized void changePassword(String username, String password) throws SecurityRealmException {
    PebbleUserDetails pud = getUser(username);
    //#defaultsecurityrealm.java:206: method: void net.sourceforge.pebble.security.DefaultSecurityRealm.changePassword(String, String)
    //#input(void changePassword(String, String)): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#input(void changePassword(String, String)): __Descendant_Table[others]
    //#input(void changePassword(String, String)): __Dispatch_Table.getFileForRealm()Ljava/io/File;
    //#input(void changePassword(String, String)): __Dispatch_Table.getFileForUser(Ljava/lang/String;)Ljava/io/File;
    //#input(void changePassword(String, String)): __Dispatch_Table.getUser(Ljava/lang/String;)Lnet/sourceforge/pebble/security/PebbleUserDetails;
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Descendant_Table[others]
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getEmailAddress()Ljava/lang/String;
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getPassword()Ljava/lang/String;
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getPreferences()Ljava/util/Map;
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getProfile()Ljava/lang/String;
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getRolesAsString()Ljava/lang/String;
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getUsername()Ljava/lang/String;
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.getWebsite()Ljava/lang/String;
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.isDetailsUpdateable()Z
    //#input(void changePassword(String, String)): net/sourceforge/pebble/security/PebbleUserDetails.__Dispatch_Table.setPassword(Ljava/lang/String;)V
    //#input(void changePassword(String, String)): password
    //#input(void changePassword(String, String)): this
    //#input(void changePassword(String, String)): this.__Tag
    //#input(void changePassword(String, String)): this.configuration
    //#input(void changePassword(String, String)): this.passwordEncoder
    //#input(void changePassword(String, String)): this.saltSource
    //#input(void changePassword(String, String)): username
    //#pre[3] (void changePassword(String, String)): this.__Tag == net/sourceforge/pebble/security/DefaultSecurityRealm
    //#pre[4] (void changePassword(String, String)): (soft) this.configuration != null
    //#pre[5] (void changePassword(String, String)): (soft) this.passwordEncoder != null
    //#pre[6] (void changePassword(String, String)): (soft) this.saltSource != null
    //#presumption(void changePassword(String, String)): pud.grantedAuthories.length@206 <= 4_294_967_295
    //#presumption(void changePassword(String, String)): pud.grantedAuthories[0..4_294_967_295]@206 != null
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:net.sourceforge.pebble.Configuration:getDataDirectory
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.io.File
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:getFileForUser
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.io.FileInputStream
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Properties
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Properties:load
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.io.FileInputStream:close
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Properties:getProperty
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.String:split
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.String:equalsIgnoreCase
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.HashMap
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Properties:keySet
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Set:iterator
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Map:put
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.HashSet
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:org.acegisecurity.GrantedAuthorityImpl
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Set:add
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Set:toArray
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:net.sourceforge.pebble.PebbleException
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.String:valueOf
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:org.acegisecurity.providers.dao.SaltSource:getSalt
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:org.acegisecurity.providers.encoding.PasswordEncoder:encodePassword
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Properties:setProperty
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.StringBuffer
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:org.acegisecurity.GrantedAuthority:getAuthority
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.StringBuffer:append
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.lang.StringBuffer:toString
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Map:keySet
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Map:get
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.io.FileOutputStream
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.util.Properties:store
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.io.FileOutputStream:flush
    //#unanalyzed(void changePassword(String, String)): Effects-of-calling:java.io.FileOutputStream:close
    if (pud != null) {
      pud.setPassword(password);
      updateUser(pud, true);
    //#defaultsecurityrealm.java:209: ?precondition failure
    //#    net/sourceforge/pebble/security/DefaultSecurityRealm.updateUser: pud.grantedAuthories != null
    //#    severity: MEDIUM
    //#    class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#    method: void changePassword(String, String)
    //#    basic block: bb_2
    //#    assertion: new PebbleUserDetails(getUser#4).grantedAuthories != null
    //#    callee: void net/sourceforge/pebble/security/DefaultSecurityRealm.updateUser(PebbleUserDetails, bool)
    //#    callee assertion: pud.grantedAuthories != null
    //#    callee file: defaultsecurityrealm.java
    //#    callee precondition index: [5]
    //#    callee srcpos: 167
    //#    VN: new PebbleUserDetails(getUser#4).grantedAuthories
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    }
  }
    //#defaultsecurityrealm.java:211: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm.changePassword(String, String)

  /**
   * Removes user details for the given username.
   *
   * @param username    the username of the user to remove
   */
  public synchronized void removeUser(String username) throws SecurityRealmException {
    File user = getFileForUser(username);
    //#defaultsecurityrealm.java:219: method: void net.sourceforge.pebble.security.DefaultSecurityRealm.removeUser(String)
    //#input(void removeUser(String)): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#input(void removeUser(String)): __Descendant_Table[others]
    //#input(void removeUser(String)): __Dispatch_Table.getFileForRealm()Ljava/io/File;
    //#input(void removeUser(String)): __Dispatch_Table.getFileForUser(Ljava/lang/String;)Ljava/io/File;
    //#input(void removeUser(String)): this
    //#input(void removeUser(String)): this.__Tag
    //#input(void removeUser(String)): this.configuration
    //#input(void removeUser(String)): username
    //#pre[2] (void removeUser(String)): this.__Tag == net/sourceforge/pebble/security/DefaultSecurityRealm
    //#pre[3] (void removeUser(String)): this.configuration != null
    //#presumption(void removeUser(String)): java.io.File:exists(...)@224 == 0
    //#unanalyzed(void removeUser(String)): Effects-of-calling:net.sourceforge.pebble.Configuration:getDataDirectory
    //#unanalyzed(void removeUser(String)): Effects-of-calling:java.io.File
    //#unanalyzed(void removeUser(String)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void removeUser(String)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void removeUser(String)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void removeUser(String)): Effects-of-calling:net.sourceforge.pebble.PebbleException
    //#unanalyzed(void removeUser(String)): Effects-of-calling:java.lang.String:valueOf
    //#test_vector(void removeUser(String)): java.io.File:exists(...)@220: {0}, {1}
    if (user.exists()) {
      user.delete();
    }

    if (user.exists()) {
      throw new SecurityRealmException("User " + username + " could not be deleted");
    }
  }
    //#defaultsecurityrealm.java:227: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm.removeUser(String)

  protected File getFileForRealm() throws SecurityRealmException {
    // find the directory and file corresponding to the user, of the form
    // ${pebbleContext.dataDirectory}/realm/${username}.properties
    return new File(configuration.getDataDirectory(), DefaultSecurityRealm.REALM_DIRECTORY_NAME);
    //#defaultsecurityrealm.java:232: method: File net.sourceforge.pebble.security.DefaultSecurityRealm.getFileForRealm()
    //#defaultsecurityrealm.java:232: Warning: method not available
    //#    -- call on String net.sourceforge.pebble.Configuration:getDataDirectory()
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.DefaultSecurityRealm
    //#    method: File getFileForRealm()
    //#    unanalyzed callee: String net.sourceforge.pebble.Configuration:getDataDirectory()
    //#input(File getFileForRealm()): this
    //#input(File getFileForRealm()): this.configuration
    //#output(File getFileForRealm()): new File(getFileForRealm#1) num objects
    //#output(File getFileForRealm()): return_value
    //#new obj(File getFileForRealm()): new File(getFileForRealm#1)
    //#pre[2] (File getFileForRealm()): this.configuration != null
    //#post(File getFileForRealm()): return_value == &new File(getFileForRealm#1)
    //#post(File getFileForRealm()): new File(getFileForRealm#1) num objects == 1
    //#defaultsecurityrealm.java:232: end of method: File net.sourceforge.pebble.security.DefaultSecurityRealm.getFileForRealm()
  }

  protected File getFileForUser(String username) throws SecurityRealmException {
    // find the directory and file corresponding to the user, of the form
    // ${pebbleContext.dataDirectory}/realm/${username}.properties
    return new File(getFileForRealm(), username + ".properties");
    //#defaultsecurityrealm.java:238: method: File net.sourceforge.pebble.security.DefaultSecurityRealm.getFileForUser(String)
    //#input(File getFileForUser(String)): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm]
    //#input(File getFileForUser(String)): __Descendant_Table[others]
    //#input(File getFileForUser(String)): __Dispatch_Table.getFileForRealm()Ljava/io/File;
    //#input(File getFileForUser(String)): this
    //#input(File getFileForUser(String)): this.__Tag
    //#input(File getFileForUser(String)): this.configuration
    //#input(File getFileForUser(String)): username
    //#output(File getFileForUser(String)): new File(getFileForUser#1) num objects
    //#output(File getFileForUser(String)): return_value
    //#new obj(File getFileForUser(String)): new File(getFileForUser#1)
    //#pre[2] (File getFileForUser(String)): this.__Tag == net/sourceforge/pebble/security/DefaultSecurityRealm
    //#pre[3] (File getFileForUser(String)): this.configuration != null
    //#post(File getFileForUser(String)): return_value == &new File(getFileForUser#1)
    //#post(File getFileForUser(String)): new File(getFileForUser#1) num objects == 1
    //#unanalyzed(File getFileForUser(String)): Effects-of-calling:net.sourceforge.pebble.Configuration:getDataDirectory
    //#unanalyzed(File getFileForUser(String)): Effects-of-calling:java.io.File
    //#defaultsecurityrealm.java:238: end of method: File net.sourceforge.pebble.security.DefaultSecurityRealm.getFileForUser(String)
  }

  public Configuration getConfiguration() {
    return configuration;
    //#defaultsecurityrealm.java:242: method: Configuration net.sourceforge.pebble.security.DefaultSecurityRealm.getConfiguration()
    //#input(Configuration getConfiguration()): this
    //#input(Configuration getConfiguration()): this.configuration
    //#output(Configuration getConfiguration()): return_value
    //#pre[2] (Configuration getConfiguration()): init'ed(this.configuration)
    //#post(Configuration getConfiguration()): return_value == this.configuration
    //#post(Configuration getConfiguration()): init'ed(return_value)
    //#defaultsecurityrealm.java:242: end of method: Configuration net.sourceforge.pebble.security.DefaultSecurityRealm.getConfiguration()
  }

  public void setConfiguration(Configuration configuration) {
    this.configuration = configuration;
    //#defaultsecurityrealm.java:246: method: void net.sourceforge.pebble.security.DefaultSecurityRealm.setConfiguration(Configuration)
    //#input(void setConfiguration(Configuration)): configuration
    //#input(void setConfiguration(Configuration)): this
    //#output(void setConfiguration(Configuration)): this.configuration
    //#post(void setConfiguration(Configuration)): this.configuration == configuration
    //#post(void setConfiguration(Configuration)): init'ed(this.configuration)
  }
    //#defaultsecurityrealm.java:247: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm.setConfiguration(Configuration)

  public PasswordEncoder getPasswordEncoder() {
    return passwordEncoder;
    //#defaultsecurityrealm.java:250: method: PasswordEncoder net.sourceforge.pebble.security.DefaultSecurityRealm.getPasswordEncoder()
    //#input(PasswordEncoder getPasswordEncoder()): this
    //#input(PasswordEncoder getPasswordEncoder()): this.passwordEncoder
    //#output(PasswordEncoder getPasswordEncoder()): return_value
    //#pre[2] (PasswordEncoder getPasswordEncoder()): init'ed(this.passwordEncoder)
    //#post(PasswordEncoder getPasswordEncoder()): return_value == this.passwordEncoder
    //#post(PasswordEncoder getPasswordEncoder()): init'ed(return_value)
    //#defaultsecurityrealm.java:250: end of method: PasswordEncoder net.sourceforge.pebble.security.DefaultSecurityRealm.getPasswordEncoder()
  }

  public void setPasswordEncoder(PasswordEncoder passwordEncoder) {
    this.passwordEncoder = passwordEncoder;
    //#defaultsecurityrealm.java:254: method: void net.sourceforge.pebble.security.DefaultSecurityRealm.setPasswordEncoder(PasswordEncoder)
    //#input(void setPasswordEncoder(PasswordEncoder)): passwordEncoder
    //#input(void setPasswordEncoder(PasswordEncoder)): this
    //#output(void setPasswordEncoder(PasswordEncoder)): this.passwordEncoder
    //#post(void setPasswordEncoder(PasswordEncoder)): this.passwordEncoder == passwordEncoder
    //#post(void setPasswordEncoder(PasswordEncoder)): init'ed(this.passwordEncoder)
  }
    //#defaultsecurityrealm.java:255: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm.setPasswordEncoder(PasswordEncoder)

  public SaltSource getSaltSource() {
    return saltSource;
    //#defaultsecurityrealm.java:258: method: SaltSource net.sourceforge.pebble.security.DefaultSecurityRealm.getSaltSource()
    //#input(SaltSource getSaltSource()): this
    //#input(SaltSource getSaltSource()): this.saltSource
    //#output(SaltSource getSaltSource()): return_value
    //#pre[2] (SaltSource getSaltSource()): init'ed(this.saltSource)
    //#post(SaltSource getSaltSource()): return_value == this.saltSource
    //#post(SaltSource getSaltSource()): init'ed(return_value)
    //#defaultsecurityrealm.java:258: end of method: SaltSource net.sourceforge.pebble.security.DefaultSecurityRealm.getSaltSource()
  }

  public void setSaltSource(SaltSource saltSource) {
    this.saltSource = saltSource;
    //#defaultsecurityrealm.java:262: method: void net.sourceforge.pebble.security.DefaultSecurityRealm.setSaltSource(SaltSource)
    //#input(void setSaltSource(SaltSource)): saltSource
    //#input(void setSaltSource(SaltSource)): this
    //#output(void setSaltSource(SaltSource)): this.saltSource
    //#post(void setSaltSource(SaltSource)): this.saltSource == saltSource
    //#post(void setSaltSource(SaltSource)): init'ed(this.saltSource)
  }
    //#defaultsecurityrealm.java:263: end of method: void net.sourceforge.pebble.security.DefaultSecurityRealm.setSaltSource(SaltSource)

}    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm$1__static_init): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm$1]
    //#output(net.sourceforge.pebble.security.DefaultSecurityRealm$1__static_init): __Dispatch_Table.accept(Ljava/io/File;Ljava/lang/String;)Z
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm$1__static_init): __Descendant_Table[net/sourceforge/pebble/security/DefaultSecurityRealm$1] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.security.DefaultSecurityRealm$1__static_init): __Dispatch_Table.accept(Ljava/io/File;Ljava/lang/String;)Z == &accept
    //#defaultsecurityrealm.java:: end of method: net.sourceforge.pebble.security.DefaultSecurityRealm$1.net.sourceforge.pebble.security.DefaultSecurityRealm$1__static_init
    //#defaultsecurityrealm.java:: end of class: net.sourceforge.pebble.security.DefaultSecurityRealm$1
    //#defaultsecurityrealm.java:: end of class: net.sourceforge.pebble.security.DefaultSecurityRealm
