//# 0 errors, 497 messages
//#
package net.sourceforge.pebble.security;
    //#pebbleuserdetails.java:1:1: class: net.sourceforge.pebble.security.PebbleUserDetails
    //#pebbleuserdetails.java:1:1: method: net.sourceforge.pebble.security.PebbleUserDetails.net.sourceforge.pebble.security.PebbleUserDetails__static_init

import net.sourceforge.pebble.Constants;
import org.acegisecurity.GrantedAuthority;
import org.acegisecurity.GrantedAuthorityImpl;
import org.acegisecurity.userdetails.UserDetails;

import java.util.HashSet;
import java.util.Set;
import java.util.HashMap;
import java.util.Map;

/**
 * Extension of the Acegi User class that adds additional information
 * such as the user's e-mail address.
 *
 * @author    Simon Brown
 */
public class PebbleUserDetails implements UserDetails {

  private String username;
  private String password;

  /** the name */
  private String name;

  /** the e-mail address */
  private String emailAddress;

  /** the website */
  private String website;

  /** the profile */
  private String profile;

  /** the user's preferences */
  private Map<String,String> preferences = new HashMap<String,String>();

  private GrantedAuthority grantedAuthories[];

  private boolean detailsUpdateable = true;

  public PebbleUserDetails() {
    //#pebbleuserdetails.java:43: method: void net.sourceforge.pebble.security.PebbleUserDetails.net.sourceforge.pebble.security.PebbleUserDetails()
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails()): this
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails()): new HashMap(PebbleUserDetails#1) num objects
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails()): this.detailsUpdateable
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails()): this.preferences
    //#new obj(void net.sourceforge.pebble.security.PebbleUserDetails()): new HashMap(PebbleUserDetails#1)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails()): this.detailsUpdateable == 1
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails()): new HashMap(PebbleUserDetails#1) num objects == 1
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails()): this.preferences == &new HashMap(PebbleUserDetails#1)
  }
    //#pebbleuserdetails.java:44: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.net.sourceforge.pebble.security.PebbleUserDetails()

  public PebbleUserDetails(String username, String name, String emailAddress, String website, String profile, String roles[], Map<String,String> preferences, boolean detailsUpdateable) {
    //#pebbleuserdetails.java:46: method: void net.sourceforge.pebble.security.PebbleUserDetails.net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): detailsUpdateable
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): emailAddress
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): name
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): preferences
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): profile
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): roles
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): roles.length
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): roles[0..4_294_967_295]
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): username
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): website
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): new HashMap(PebbleUserDetails#1) num objects
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.detailsUpdateable
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.emailAddress
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.grantedAuthories
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.name
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.preferences
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.profile
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.username
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.website
    //#new obj(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): new HashMap(PebbleUserDetails#1)
    //#pre[7] (void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): (soft) roles.length <= 4_294_967_295
    //#pre[8] (void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): (soft) roles[0..4_294_967_295] != null
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.detailsUpdateable == detailsUpdateable
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): init'ed(this.detailsUpdateable)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.emailAddress == emailAddress
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): init'ed(this.emailAddress)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): init'ed(this.grantedAuthories)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.name == name
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): init'ed(this.name)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.preferences == preferences
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): init'ed(this.preferences)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.profile == profile
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): init'ed(this.profile)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.username == username
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): init'ed(this.username)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): this.website == website
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): init'ed(this.website)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): new HashMap(PebbleUserDetails#1) num objects == 1
    //#unanalyzed(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): Effects-of-calling:java.util.HashSet
    //#unanalyzed(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): Effects-of-calling:org.acegisecurity.GrantedAuthorityImpl
    //#unanalyzed(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): Effects-of-calling:java.util.Set:add
    //#unanalyzed(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)): Effects-of-calling:java.util.Set:toArray
    this.username = username;
    this.name = name;
    this.emailAddress = emailAddress;
    this.website = website;
    this.profile = profile;
    this.grantedAuthories = createGrantedAuthorities(roles);
    this.preferences = preferences;
    this.detailsUpdateable = detailsUpdateable;
  }
    //#pebbleuserdetails.java:55: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String[], Map, bool)

  public PebbleUserDetails(String username, String password, String name, String emailAddress, String website, String profile, String roles[], Map<String,String> preferences, boolean detailsUpdateable) {
    //#pebbleuserdetails.java:57: method: void net.sourceforge.pebble.security.PebbleUserDetails.net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): detailsUpdateable
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): emailAddress
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): name
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): password
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): preferences
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): profile
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): roles
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): roles.length
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): roles[0..4_294_967_295]
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): username
    //#input(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): website
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): new HashMap(PebbleUserDetails#1) num objects
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.detailsUpdateable
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.emailAddress
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.grantedAuthories
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.name
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.password
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.preferences
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.profile
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.username
    //#output(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.website
    //#new obj(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): new HashMap(PebbleUserDetails#1)
    //#pre[8] (void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): (soft) roles.length <= 4_294_967_295
    //#pre[9] (void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): (soft) roles[0..4_294_967_295] != null
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.detailsUpdateable == detailsUpdateable
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): init'ed(this.detailsUpdateable)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.emailAddress == emailAddress
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): init'ed(this.emailAddress)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): init'ed(this.grantedAuthories)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.name == name
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): init'ed(this.name)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.password == password
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): init'ed(this.password)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.preferences == preferences
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): init'ed(this.preferences)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.profile == profile
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): init'ed(this.profile)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.username == username
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): init'ed(this.username)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): this.website == website
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): init'ed(this.website)
    //#post(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): new HashMap(PebbleUserDetails#1) num objects == 1
    //#unanalyzed(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): Effects-of-calling:java.util.HashSet
    //#unanalyzed(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): Effects-of-calling:org.acegisecurity.GrantedAuthorityImpl
    //#unanalyzed(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): Effects-of-calling:java.util.Set:add
    //#unanalyzed(void net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)): Effects-of-calling:java.util.Set:toArray
    this.username = username;
    this.password = password;
    this.name = name;
    this.emailAddress = emailAddress;
    this.website = website;
    this.profile = profile;
    this.grantedAuthories = createGrantedAuthorities(roles);
    this.preferences = preferences;
    this.detailsUpdateable = detailsUpdateable;
  }
    //#pebbleuserdetails.java:67: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.net.sourceforge.pebble.security.PebbleUserDetails(String, String, String, String, String, String, String[], Map, bool)

  public String getUsername() {
    return this.username;
    //#pebbleuserdetails.java:70: method: String net.sourceforge.pebble.security.PebbleUserDetails.getUsername()
    //#input(String getUsername()): this
    //#input(String getUsername()): this.username
    //#output(String getUsername()): return_value
    //#pre[2] (String getUsername()): init'ed(this.username)
    //#post(String getUsername()): return_value == this.username
    //#post(String getUsername()): init'ed(return_value)
    //#pebbleuserdetails.java:70: end of method: String net.sourceforge.pebble.security.PebbleUserDetails.getUsername()
  }

  public String getPassword() {
    return this.password;
    //#pebbleuserdetails.java:74: method: String net.sourceforge.pebble.security.PebbleUserDetails.getPassword()
    //#input(String getPassword()): this
    //#input(String getPassword()): this.password
    //#output(String getPassword()): return_value
    //#pre[2] (String getPassword()): init'ed(this.password)
    //#post(String getPassword()): return_value == this.password
    //#post(String getPassword()): init'ed(return_value)
    //#pebbleuserdetails.java:74: end of method: String net.sourceforge.pebble.security.PebbleUserDetails.getPassword()
  }

  public boolean isAccountNonExpired() {
    return true;
    //#pebbleuserdetails.java:78: method: bool net.sourceforge.pebble.security.PebbleUserDetails.isAccountNonExpired()
    //#output(bool isAccountNonExpired()): return_value
    //#post(bool isAccountNonExpired()): return_value == 1
    //#pebbleuserdetails.java:78: end of method: bool net.sourceforge.pebble.security.PebbleUserDetails.isAccountNonExpired()
  }

  public boolean isAccountNonLocked() {
    return true;
    //#pebbleuserdetails.java:82: method: bool net.sourceforge.pebble.security.PebbleUserDetails.isAccountNonLocked()
    //#output(bool isAccountNonLocked()): return_value
    //#post(bool isAccountNonLocked()): return_value == 1
    //#pebbleuserdetails.java:82: end of method: bool net.sourceforge.pebble.security.PebbleUserDetails.isAccountNonLocked()
  }

  public boolean isCredentialsNonExpired() {
    return true;
    //#pebbleuserdetails.java:86: method: bool net.sourceforge.pebble.security.PebbleUserDetails.isCredentialsNonExpired()
    //#output(bool isCredentialsNonExpired()): return_value
    //#post(bool isCredentialsNonExpired()): return_value == 1
    //#pebbleuserdetails.java:86: end of method: bool net.sourceforge.pebble.security.PebbleUserDetails.isCredentialsNonExpired()
  }

  public boolean isEnabled() {
    return true;
    //#pebbleuserdetails.java:90: method: bool net.sourceforge.pebble.security.PebbleUserDetails.isEnabled()
    //#output(bool isEnabled()): return_value
    //#post(bool isEnabled()): return_value == 1
    //#pebbleuserdetails.java:90: end of method: bool net.sourceforge.pebble.security.PebbleUserDetails.isEnabled()
  }

  /**
   * Gets the name.
   *
   * @return  a String
   */
  public String getName() {
    return name;
    //#pebbleuserdetails.java:99: method: String net.sourceforge.pebble.security.PebbleUserDetails.getName()
    //#input(String getName()): this
    //#input(String getName()): this.name
    //#output(String getName()): return_value
    //#pre[2] (String getName()): init'ed(this.name)
    //#post(String getName()): return_value == this.name
    //#post(String getName()): init'ed(return_value)
    //#pebbleuserdetails.java:99: end of method: String net.sourceforge.pebble.security.PebbleUserDetails.getName()
  }

  /**
   * Gets the e-mail address.
   *
   * @return  a String
   */
  public String getEmailAddress() {
    return emailAddress;
    //#pebbleuserdetails.java:108: method: String net.sourceforge.pebble.security.PebbleUserDetails.getEmailAddress()
    //#input(String getEmailAddress()): this
    //#input(String getEmailAddress()): this.emailAddress
    //#output(String getEmailAddress()): return_value
    //#pre[2] (String getEmailAddress()): init'ed(this.emailAddress)
    //#post(String getEmailAddress()): return_value == this.emailAddress
    //#post(String getEmailAddress()): init'ed(return_value)
    //#pebbleuserdetails.java:108: end of method: String net.sourceforge.pebble.security.PebbleUserDetails.getEmailAddress()
  }

  /**
   * Gets the website.
   *
   * @return  a String
   */
  public String getWebsite() {
    return website;
    //#pebbleuserdetails.java:117: method: String net.sourceforge.pebble.security.PebbleUserDetails.getWebsite()
    //#input(String getWebsite()): this
    //#input(String getWebsite()): this.website
    //#output(String getWebsite()): return_value
    //#pre[2] (String getWebsite()): init'ed(this.website)
    //#post(String getWebsite()): return_value == this.website
    //#post(String getWebsite()): init'ed(return_value)
    //#pebbleuserdetails.java:117: end of method: String net.sourceforge.pebble.security.PebbleUserDetails.getWebsite()
  }

  /**
   * Gets the user's profile.
   *
   * @return  a String
   */
  public String getProfile() {
    return this.profile;
    //#pebbleuserdetails.java:126: method: String net.sourceforge.pebble.security.PebbleUserDetails.getProfile()
    //#input(String getProfile()): this
    //#input(String getProfile()): this.profile
    //#output(String getProfile()): return_value
    //#pre[2] (String getProfile()): init'ed(this.profile)
    //#post(String getProfile()): return_value == this.profile
    //#post(String getProfile()): init'ed(return_value)
    //#pebbleuserdetails.java:126: end of method: String net.sourceforge.pebble.security.PebbleUserDetails.getProfile()
  }

  public GrantedAuthority[] getAuthorities() {
    return this.grantedAuthories;
    //#pebbleuserdetails.java:130: method: GrantedAuthority[] net.sourceforge.pebble.security.PebbleUserDetails.getAuthorities()
    //#input(GrantedAuthority[] getAuthorities()): this
    //#input(GrantedAuthority[] getAuthorities()): this.grantedAuthories
    //#output(GrantedAuthority[] getAuthorities()): return_value
    //#pre[2] (GrantedAuthority[] getAuthorities()): init'ed(this.grantedAuthories)
    //#post(GrantedAuthority[] getAuthorities()): return_value == this.grantedAuthories
    //#post(GrantedAuthority[] getAuthorities()): init'ed(return_value)
    //#pebbleuserdetails.java:130: end of method: GrantedAuthority[] net.sourceforge.pebble.security.PebbleUserDetails.getAuthorities()
  }

  public String[] getRoles() {
    GrantedAuthority[] authorities = getAuthorities();
    //#pebbleuserdetails.java:134: method: String[] net.sourceforge.pebble.security.PebbleUserDetails.getRoles()
    //#input(String[] getRoles()): __Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(String[] getRoles()): __Descendant_Table[others]
    //#input(String[] getRoles()): __Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(String[] getRoles()): this
    //#input(String[] getRoles()): this.__Tag
    //#input(String[] getRoles()): this.grantedAuthories
    //#input(String[] getRoles()): this.grantedAuthories.length
    //#input(String[] getRoles()): this.grantedAuthories[0..4_294_967_294]
    //#output(String[] getRoles()): new String[](getRoles#1) num objects
    //#output(String[] getRoles()): return_value.length
    //#output(String[] getRoles()): return_value[0..4_294_967_295]
    //#output(String[] getRoles()): return_value
    //#new obj(String[] getRoles()): new String[](getRoles#1)
    //#pre[2] (String[] getRoles()): this.__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#pre[3] (String[] getRoles()): this.grantedAuthories != null
    //#pre[4] (String[] getRoles()): this.grantedAuthories.length <= 4_294_967_295
    //#pre[5] (String[] getRoles()): (soft) this.grantedAuthories[0..4_294_967_294] != null
    //#post(String[] getRoles()): return_value == &new String[](getRoles#1)
    //#post(String[] getRoles()): new String[](getRoles#1) num objects == 1
    //#post(String[] getRoles()): return_value.length == this.grantedAuthories.length
    //#post(String[] getRoles()): return_value.length <= 4_294_967_295
    //#post(String[] getRoles()): possibly_updated(return_value[0..4_294_967_295])
    String[] roles = new String[authorities.length];
    for (int i = 0; i < authorities.length; i++) {
      roles[i] = authorities[i].getAuthority();
    //#pebbleuserdetails.java:137: Warning: method not available
    //#    -- call on String org.acegisecurity.GrantedAuthority:getAuthority()
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.PebbleUserDetails
    //#    method: String[] getRoles()
    //#    unanalyzed callee: String org.acegisecurity.GrantedAuthority:getAuthority()
    }

    return roles;
    //#pebbleuserdetails.java:140: end of method: String[] net.sourceforge.pebble.security.PebbleUserDetails.getRoles()
  }

  public String getRolesAsString() {
    StringBuffer buf = new StringBuffer();
    //#pebbleuserdetails.java:144: method: String net.sourceforge.pebble.security.PebbleUserDetails.getRolesAsString()
    //#input(String getRolesAsString()): __Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(String getRolesAsString()): __Descendant_Table[others]
    //#input(String getRolesAsString()): __Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(String getRolesAsString()): this
    //#input(String getRolesAsString()): this.__Tag
    //#input(String getRolesAsString()): this.grantedAuthories
    //#input(String getRolesAsString()): this.grantedAuthories.length
    //#input(String getRolesAsString()): this.grantedAuthories[0..4_294_967_294]
    //#output(String getRolesAsString()): return_value
    //#pre[2] (String getRolesAsString()): this.__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#pre[3] (String getRolesAsString()): this.grantedAuthories != null
    //#pre[4] (String getRolesAsString()): this.grantedAuthories.length <= 4_294_967_295
    //#pre[5] (String getRolesAsString()): (soft) this.grantedAuthories[0..4_294_967_294] != null
    //#post(String getRolesAsString()): return_value != null

    GrantedAuthority[] authorities = getAuthorities();
    for (int i = 0; i < authorities.length; i++) {
      buf.append(authorities[i].getAuthority());
    //#pebbleuserdetails.java:148: Warning: method not available
    //#    -- call on String org.acegisecurity.GrantedAuthority:getAuthority()
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.PebbleUserDetails
    //#    method: String getRolesAsString()
    //#    unanalyzed callee: String org.acegisecurity.GrantedAuthority:getAuthority()
      if (i < authorities.length) {
    //#pebbleuserdetails.java:149: Warning: test always goes same way
    //#    test predetermined because i - authorities.length in -4_294_967_295..-1
    //#    severity: LOW
    //#    class: net.sourceforge.pebble.security.PebbleUserDetails
    //#    method: String getRolesAsString()
    //#    from bb: bb_2
    //#    live edge: bb_2-->bb_3
    //#    tested vn: i - this.grantedAuthories.length
    //#    tested vn values: {-4_294_967_295..-1}
        buf.append(",");
      }
    }

    return buf.toString();
    //#pebbleuserdetails.java:154: end of method: String net.sourceforge.pebble.security.PebbleUserDetails.getRolesAsString()
  }

  public boolean isUserInRole(String role) {
    GrantedAuthority[] authorities = getAuthorities();
    //#pebbleuserdetails.java:158: method: bool net.sourceforge.pebble.security.PebbleUserDetails.isUserInRole(String)
    //#input(bool isUserInRole(String)): __Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(bool isUserInRole(String)): __Descendant_Table[others]
    //#input(bool isUserInRole(String)): __Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(bool isUserInRole(String)): role
    //#input(bool isUserInRole(String)): this
    //#input(bool isUserInRole(String)): this.__Tag
    //#input(bool isUserInRole(String)): this.grantedAuthories
    //#input(bool isUserInRole(String)): this.grantedAuthories.length
    //#input(bool isUserInRole(String)): this.grantedAuthories[0..4_294_967_294]
    //#output(bool isUserInRole(String)): return_value
    //#pre[3] (bool isUserInRole(String)): this.__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#pre[4] (bool isUserInRole(String)): init'ed(this.grantedAuthories)
    //#pre[5] (bool isUserInRole(String)): (soft) this.grantedAuthories.length <= 4_294_967_295
    //#pre[6] (bool isUserInRole(String)): (soft) this.grantedAuthories[0..4_294_967_294] != null
    //#presumption(bool isUserInRole(String)): org.acegisecurity.GrantedAuthority:getAuthority(...)@161 != null
    //#post(bool isUserInRole(String)): init'ed(return_value)
    //#test_vector(bool isUserInRole(String)): this.grantedAuthories: Addr_Set{null}, Inverse{null}
    //#test_vector(bool isUserInRole(String)): java.lang.String:equals(...)@161: {0}, {1}
    if (authorities != null) {
      for (GrantedAuthority authority : authorities) {
        if (authority.getAuthority().equals(role)) {
    //#pebbleuserdetails.java:161: Warning: method not available
    //#    -- call on String org.acegisecurity.GrantedAuthority:getAuthority()
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.PebbleUserDetails
    //#    method: bool isUserInRole(String)
    //#    unanalyzed callee: String org.acegisecurity.GrantedAuthority:getAuthority()
          return true;
        }
      }
    }
    return false;
    //#pebbleuserdetails.java:166: end of method: bool net.sourceforge.pebble.security.PebbleUserDetails.isUserInRole(String)
  }

  public boolean isBlogAdmin() {
    return isUserInRole(Constants.BLOG_ADMIN_ROLE);
    //#pebbleuserdetails.java:170: method: bool net.sourceforge.pebble.security.PebbleUserDetails.isBlogAdmin()
    //#input(bool isBlogAdmin()): __Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(bool isBlogAdmin()): __Descendant_Table[others]
    //#input(bool isBlogAdmin()): __Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(bool isBlogAdmin()): __Dispatch_Table.isUserInRole(Ljava/lang/String;)Z
    //#input(bool isBlogAdmin()): net.sourceforge.pebble.Constants.BLOG_ADMIN_ROLE
    //#input(bool isBlogAdmin()): this
    //#input(bool isBlogAdmin()): this.__Tag
    //#input(bool isBlogAdmin()): this.grantedAuthories
    //#input(bool isBlogAdmin()): this.grantedAuthories.length
    //#input(bool isBlogAdmin()): this.grantedAuthories[0..4_294_967_295]
    //#output(bool isBlogAdmin()): return_value
    //#pre[2] (bool isBlogAdmin()): this.__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#pre[3] (bool isBlogAdmin()): init'ed(this.grantedAuthories)
    //#pre[4] (bool isBlogAdmin()): (soft) this.grantedAuthories.length <= 4_294_967_295
    //#pre[5] (bool isBlogAdmin()): (soft) this.grantedAuthories[0..4_294_967_295] != null
    //#presumption(bool isBlogAdmin()): init'ed(net.sourceforge.pebble.Constants.BLOG_ADMIN_ROLE)
    //#post(bool isBlogAdmin()): init'ed(return_value)
    //#unanalyzed(bool isBlogAdmin()): Effects-of-calling:org.acegisecurity.GrantedAuthority:getAuthority
    //#unanalyzed(bool isBlogAdmin()): Effects-of-calling:java.lang.String:equals
    //#pebbleuserdetails.java:170: end of method: bool net.sourceforge.pebble.security.PebbleUserDetails.isBlogAdmin()
  }

  public boolean isBlogOwner() {
    return isUserInRole(Constants.BLOG_OWNER_ROLE);
    //#pebbleuserdetails.java:174: method: bool net.sourceforge.pebble.security.PebbleUserDetails.isBlogOwner()
    //#input(bool isBlogOwner()): __Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(bool isBlogOwner()): __Descendant_Table[others]
    //#input(bool isBlogOwner()): __Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(bool isBlogOwner()): __Dispatch_Table.isUserInRole(Ljava/lang/String;)Z
    //#input(bool isBlogOwner()): net.sourceforge.pebble.Constants.BLOG_OWNER_ROLE
    //#input(bool isBlogOwner()): this
    //#input(bool isBlogOwner()): this.__Tag
    //#input(bool isBlogOwner()): this.grantedAuthories
    //#input(bool isBlogOwner()): this.grantedAuthories.length
    //#input(bool isBlogOwner()): this.grantedAuthories[0..4_294_967_295]
    //#output(bool isBlogOwner()): return_value
    //#pre[2] (bool isBlogOwner()): this.__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#pre[3] (bool isBlogOwner()): init'ed(this.grantedAuthories)
    //#pre[4] (bool isBlogOwner()): (soft) this.grantedAuthories.length <= 4_294_967_295
    //#pre[5] (bool isBlogOwner()): (soft) this.grantedAuthories[0..4_294_967_295] != null
    //#presumption(bool isBlogOwner()): init'ed(net.sourceforge.pebble.Constants.BLOG_OWNER_ROLE)
    //#post(bool isBlogOwner()): init'ed(return_value)
    //#unanalyzed(bool isBlogOwner()): Effects-of-calling:org.acegisecurity.GrantedAuthority:getAuthority
    //#unanalyzed(bool isBlogOwner()): Effects-of-calling:java.lang.String:equals
    //#pebbleuserdetails.java:174: end of method: bool net.sourceforge.pebble.security.PebbleUserDetails.isBlogOwner()
  }

  public boolean isBlogPublisher() {
    return isUserInRole(Constants.BLOG_PUBLISHER_ROLE);
    //#pebbleuserdetails.java:178: method: bool net.sourceforge.pebble.security.PebbleUserDetails.isBlogPublisher()
    //#input(bool isBlogPublisher()): __Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(bool isBlogPublisher()): __Descendant_Table[others]
    //#input(bool isBlogPublisher()): __Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(bool isBlogPublisher()): __Dispatch_Table.isUserInRole(Ljava/lang/String;)Z
    //#input(bool isBlogPublisher()): net.sourceforge.pebble.Constants.BLOG_PUBLISHER_ROLE
    //#input(bool isBlogPublisher()): this
    //#input(bool isBlogPublisher()): this.__Tag
    //#input(bool isBlogPublisher()): this.grantedAuthories
    //#input(bool isBlogPublisher()): this.grantedAuthories.length
    //#input(bool isBlogPublisher()): this.grantedAuthories[0..4_294_967_295]
    //#output(bool isBlogPublisher()): return_value
    //#pre[2] (bool isBlogPublisher()): this.__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#pre[3] (bool isBlogPublisher()): init'ed(this.grantedAuthories)
    //#pre[4] (bool isBlogPublisher()): (soft) this.grantedAuthories.length <= 4_294_967_295
    //#pre[5] (bool isBlogPublisher()): (soft) this.grantedAuthories[0..4_294_967_295] != null
    //#presumption(bool isBlogPublisher()): init'ed(net.sourceforge.pebble.Constants.BLOG_PUBLISHER_ROLE)
    //#post(bool isBlogPublisher()): init'ed(return_value)
    //#unanalyzed(bool isBlogPublisher()): Effects-of-calling:org.acegisecurity.GrantedAuthority:getAuthority
    //#unanalyzed(bool isBlogPublisher()): Effects-of-calling:java.lang.String:equals
    //#pebbleuserdetails.java:178: end of method: bool net.sourceforge.pebble.security.PebbleUserDetails.isBlogPublisher()
  }

  public boolean isBlogContributor() {
    return isUserInRole(Constants.BLOG_CONTRIBUTOR_ROLE);
    //#pebbleuserdetails.java:182: method: bool net.sourceforge.pebble.security.PebbleUserDetails.isBlogContributor()
    //#input(bool isBlogContributor()): __Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#input(bool isBlogContributor()): __Descendant_Table[others]
    //#input(bool isBlogContributor()): __Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#input(bool isBlogContributor()): __Dispatch_Table.isUserInRole(Ljava/lang/String;)Z
    //#input(bool isBlogContributor()): net.sourceforge.pebble.Constants.BLOG_CONTRIBUTOR_ROLE
    //#input(bool isBlogContributor()): this
    //#input(bool isBlogContributor()): this.__Tag
    //#input(bool isBlogContributor()): this.grantedAuthories
    //#input(bool isBlogContributor()): this.grantedAuthories.length
    //#input(bool isBlogContributor()): this.grantedAuthories[0..4_294_967_295]
    //#output(bool isBlogContributor()): return_value
    //#pre[2] (bool isBlogContributor()): this.__Tag == net/sourceforge/pebble/security/PebbleUserDetails
    //#pre[3] (bool isBlogContributor()): init'ed(this.grantedAuthories)
    //#pre[4] (bool isBlogContributor()): (soft) this.grantedAuthories.length <= 4_294_967_295
    //#pre[5] (bool isBlogContributor()): (soft) this.grantedAuthories[0..4_294_967_295] != null
    //#presumption(bool isBlogContributor()): init'ed(net.sourceforge.pebble.Constants.BLOG_CONTRIBUTOR_ROLE)
    //#post(bool isBlogContributor()): init'ed(return_value)
    //#unanalyzed(bool isBlogContributor()): Effects-of-calling:org.acegisecurity.GrantedAuthority:getAuthority
    //#unanalyzed(bool isBlogContributor()): Effects-of-calling:java.lang.String:equals
    //#pebbleuserdetails.java:182: end of method: bool net.sourceforge.pebble.security.PebbleUserDetails.isBlogContributor()
  }

  private static GrantedAuthority[] createGrantedAuthorities(String roles[]) {
    Set<GrantedAuthority> authorities = new HashSet<GrantedAuthority>();
    //#pebbleuserdetails.java:186: method: GrantedAuthority[] net.sourceforge.pebble.security.PebbleUserDetails.createGrantedAuthorities(String[])
    //#input(GrantedAuthority[] createGrantedAuthorities(String[])): net.sourceforge.pebble.Constants.BLOG_READER_ROLE
    //#input(GrantedAuthority[] createGrantedAuthorities(String[])): roles
    //#input(GrantedAuthority[] createGrantedAuthorities(String[])): roles.length
    //#input(GrantedAuthority[] createGrantedAuthorities(String[])): roles[0..4_294_967_294]
    //#output(GrantedAuthority[] createGrantedAuthorities(String[])): return_value
    //#pre[2] (GrantedAuthority[] createGrantedAuthorities(String[])): (soft) roles.length <= 4_294_967_295
    //#pre[3] (GrantedAuthority[] createGrantedAuthorities(String[])): (soft) roles[0..4_294_967_294] != null
    //#presumption(GrantedAuthority[] createGrantedAuthorities(String[])): init'ed(net.sourceforge.pebble.Constants.BLOG_READER_ROLE)
    //#post(GrantedAuthority[] createGrantedAuthorities(String[])): init'ed(return_value)
    //#test_vector(GrantedAuthority[] createGrantedAuthorities(String[])): roles: Addr_Set{null}, Inverse{null}
    if (roles != null) {
      for (String role : roles) {
        authorities.add(new GrantedAuthorityImpl(role.trim()));
    //#pebbleuserdetails.java:189: Warning: method not available
    //#    -- call on void org.acegisecurity.GrantedAuthorityImpl(String)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.PebbleUserDetails
    //#    method: GrantedAuthority[] createGrantedAuthorities(String[])
    //#    unanalyzed callee: void org.acegisecurity.GrantedAuthorityImpl(String)
      }
    }
    authorities.add(new GrantedAuthorityImpl(Constants.BLOG_READER_ROLE));
    //#pebbleuserdetails.java:192: Warning: method not available
    //#    -- call on void org.acegisecurity.GrantedAuthorityImpl(String)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.security.PebbleUserDetails
    //#    method: GrantedAuthority[] createGrantedAuthorities(String[])
    //#    unanalyzed callee: void org.acegisecurity.GrantedAuthorityImpl(String)

    return authorities.toArray(new GrantedAuthority[]{});
    //#pebbleuserdetails.java:194: end of method: GrantedAuthority[] net.sourceforge.pebble.security.PebbleUserDetails.createGrantedAuthorities(String[])
  }

  public void setUsername(String username) {
    this.username = username;
    //#pebbleuserdetails.java:198: method: void net.sourceforge.pebble.security.PebbleUserDetails.setUsername(String)
    //#input(void setUsername(String)): this
    //#input(void setUsername(String)): username
    //#output(void setUsername(String)): this.username
    //#post(void setUsername(String)): this.username == username
    //#post(void setUsername(String)): init'ed(this.username)
  }
    //#pebbleuserdetails.java:199: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.setUsername(String)

  public void setPassword(String password) {
    this.password = password;
    //#pebbleuserdetails.java:202: method: void net.sourceforge.pebble.security.PebbleUserDetails.setPassword(String)
    //#input(void setPassword(String)): password
    //#input(void setPassword(String)): this
    //#output(void setPassword(String)): this.password
    //#post(void setPassword(String)): this.password == password
    //#post(void setPassword(String)): init'ed(this.password)
  }
    //#pebbleuserdetails.java:203: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.setPassword(String)

  public void setName(String name) {
    this.name = name;
    //#pebbleuserdetails.java:206: method: void net.sourceforge.pebble.security.PebbleUserDetails.setName(String)
    //#input(void setName(String)): name
    //#input(void setName(String)): this
    //#output(void setName(String)): this.name
    //#post(void setName(String)): this.name == name
    //#post(void setName(String)): init'ed(this.name)
  }
    //#pebbleuserdetails.java:207: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.setName(String)

  public void setEmailAddress(String emailAddress) {
    this.emailAddress = emailAddress;
    //#pebbleuserdetails.java:210: method: void net.sourceforge.pebble.security.PebbleUserDetails.setEmailAddress(String)
    //#input(void setEmailAddress(String)): emailAddress
    //#input(void setEmailAddress(String)): this
    //#output(void setEmailAddress(String)): this.emailAddress
    //#post(void setEmailAddress(String)): this.emailAddress == emailAddress
    //#post(void setEmailAddress(String)): init'ed(this.emailAddress)
  }
    //#pebbleuserdetails.java:211: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.setEmailAddress(String)

  public void setWebsite(String website) {
    this.website = website;
    //#pebbleuserdetails.java:214: method: void net.sourceforge.pebble.security.PebbleUserDetails.setWebsite(String)
    //#input(void setWebsite(String)): this
    //#input(void setWebsite(String)): website
    //#output(void setWebsite(String)): this.website
    //#post(void setWebsite(String)): this.website == website
    //#post(void setWebsite(String)): init'ed(this.website)
  }
    //#pebbleuserdetails.java:215: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.setWebsite(String)

  public void setProfile(String profile) {
    this.profile = profile;
    //#pebbleuserdetails.java:218: method: void net.sourceforge.pebble.security.PebbleUserDetails.setProfile(String)
    //#input(void setProfile(String)): profile
    //#input(void setProfile(String)): this
    //#output(void setProfile(String)): this.profile
    //#post(void setProfile(String)): this.profile == profile
    //#post(void setProfile(String)): init'ed(this.profile)
  }
    //#pebbleuserdetails.java:219: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.setProfile(String)

  public void setGrantedAuthories(GrantedAuthority[] grantedAuthories) {
    this.grantedAuthories = grantedAuthories;
    //#pebbleuserdetails.java:222: method: void net.sourceforge.pebble.security.PebbleUserDetails.setGrantedAuthories(GrantedAuthority[])
    //#input(void setGrantedAuthories(GrantedAuthority[])): grantedAuthories
    //#input(void setGrantedAuthories(GrantedAuthority[])): this
    //#output(void setGrantedAuthories(GrantedAuthority[])): this.grantedAuthories
    //#post(void setGrantedAuthories(GrantedAuthority[])): this.grantedAuthories == grantedAuthories
    //#post(void setGrantedAuthories(GrantedAuthority[])): init'ed(this.grantedAuthories)
  }
    //#pebbleuserdetails.java:223: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.setGrantedAuthories(GrantedAuthority[])

  public boolean isDetailsUpdateable() {
    return detailsUpdateable;
    //#pebbleuserdetails.java:226: method: bool net.sourceforge.pebble.security.PebbleUserDetails.isDetailsUpdateable()
    //#input(bool isDetailsUpdateable()): this
    //#input(bool isDetailsUpdateable()): this.detailsUpdateable
    //#output(bool isDetailsUpdateable()): return_value
    //#pre[2] (bool isDetailsUpdateable()): init'ed(this.detailsUpdateable)
    //#post(bool isDetailsUpdateable()): return_value == this.detailsUpdateable
    //#post(bool isDetailsUpdateable()): init'ed(return_value)
    //#pebbleuserdetails.java:226: end of method: bool net.sourceforge.pebble.security.PebbleUserDetails.isDetailsUpdateable()
  }

  public void setDetailsUpdateable(boolean detailsUpdateable) {
    this.detailsUpdateable = detailsUpdateable;
    //#pebbleuserdetails.java:230: method: void net.sourceforge.pebble.security.PebbleUserDetails.setDetailsUpdateable(bool)
    //#input(void setDetailsUpdateable(bool)): detailsUpdateable
    //#input(void setDetailsUpdateable(bool)): this
    //#output(void setDetailsUpdateable(bool)): this.detailsUpdateable
    //#post(void setDetailsUpdateable(bool)): this.detailsUpdateable == detailsUpdateable
    //#post(void setDetailsUpdateable(bool)): init'ed(this.detailsUpdateable)
  }
    //#pebbleuserdetails.java:231: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.setDetailsUpdateable(bool)

  public Map<String,String> getPreferences() {
    return new HashMap<String,String>(preferences);
    //#pebbleuserdetails.java:234: method: Map net.sourceforge.pebble.security.PebbleUserDetails.getPreferences()
    //#input(Map getPreferences()): this
    //#input(Map getPreferences()): this.preferences
    //#output(Map getPreferences()): new HashMap(getPreferences#1) num objects
    //#output(Map getPreferences()): return_value
    //#new obj(Map getPreferences()): new HashMap(getPreferences#1)
    //#pre[2] (Map getPreferences()): init'ed(this.preferences)
    //#post(Map getPreferences()): return_value == &new HashMap(getPreferences#1)
    //#post(Map getPreferences()): new HashMap(getPreferences#1) num objects == 1
    //#pebbleuserdetails.java:234: end of method: Map net.sourceforge.pebble.security.PebbleUserDetails.getPreferences()
  }

  public String getPreference(String key) {
    return preferences.get(key);
    //#pebbleuserdetails.java:238: method: String net.sourceforge.pebble.security.PebbleUserDetails.getPreference(String)
    //#input(String getPreference(String)): key
    //#input(String getPreference(String)): this
    //#input(String getPreference(String)): this.preferences
    //#output(String getPreference(String)): return_value
    //#pre[3] (String getPreference(String)): this.preferences != null
    //#post(String getPreference(String)): init'ed(return_value)
    //#pebbleuserdetails.java:238: end of method: String net.sourceforge.pebble.security.PebbleUserDetails.getPreference(String)
  }

  public void setPreferences(Map<String,String> preferences) {
    this.preferences = new HashMap<String,String>(preferences);
    //#pebbleuserdetails.java:242: method: void net.sourceforge.pebble.security.PebbleUserDetails.setPreferences(Map)
    //#input(void setPreferences(Map)): preferences
    //#input(void setPreferences(Map)): this
    //#output(void setPreferences(Map)): new HashMap(setPreferences#1) num objects
    //#output(void setPreferences(Map)): this.preferences
    //#new obj(void setPreferences(Map)): new HashMap(setPreferences#1)
    //#post(void setPreferences(Map)): this.preferences == &new HashMap(setPreferences#1)
    //#post(void setPreferences(Map)): new HashMap(setPreferences#1) num objects == 1
  }
    //#pebbleuserdetails.java:243: end of method: void net.sourceforge.pebble.security.PebbleUserDetails.setPreferences(Map)
  
}    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails]
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getEmailAddress()Ljava/lang/String;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getName()Ljava/lang/String;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getPassword()Ljava/lang/String;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getPreference(Ljava/lang/String;)Ljava/lang/String;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getPreferences()Ljava/util/Map;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getProfile()Ljava/lang/String;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getRoles()[Ljava/lang/String;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getRolesAsString()Ljava/lang/String;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getUsername()Ljava/lang/String;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getWebsite()Ljava/lang/String;
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isAccountNonExpired()Z
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isAccountNonLocked()Z
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isBlogAdmin()Z
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isBlogContributor()Z
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isBlogOwner()Z
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isBlogPublisher()Z
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isCredentialsNonExpired()Z
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isDetailsUpdateable()Z
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isEnabled()Z
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isUserInRole(Ljava/lang/String;)Z
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setDetailsUpdateable(Z)V
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setEmailAddress(Ljava/lang/String;)V
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setGrantedAuthories([Lorg/acegisecurity/GrantedAuthority;)V
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setName(Ljava/lang/String;)V
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setPassword(Ljava/lang/String;)V
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setPreferences(Ljava/util/Map;)V
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setProfile(Ljava/lang/String;)V
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setUsername(Ljava/lang/String;)V
    //#output(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setWebsite(Ljava/lang/String;)V
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Descendant_Table[net/sourceforge/pebble/security/PebbleUserDetails] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getAuthorities()[Lorg/acegisecurity/GrantedAuthority; == &getAuthorities
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getEmailAddress()Ljava/lang/String; == &getEmailAddress
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getName()Ljava/lang/String; == &getName
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getPassword()Ljava/lang/String; == &getPassword
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getPreference(Ljava/lang/String;)Ljava/lang/String; == &getPreference
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getPreferences()Ljava/util/Map; == &getPreferences
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getProfile()Ljava/lang/String; == &getProfile
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getRoles()[Ljava/lang/String; == &getRoles
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getRolesAsString()Ljava/lang/String; == &getRolesAsString
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getUsername()Ljava/lang/String; == &getUsername
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.getWebsite()Ljava/lang/String; == &getWebsite
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isAccountNonExpired()Z == &isAccountNonExpired
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isAccountNonLocked()Z == &isAccountNonLocked
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isBlogAdmin()Z == &isBlogAdmin
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isBlogContributor()Z == &isBlogContributor
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isBlogOwner()Z == &isBlogOwner
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isBlogPublisher()Z == &isBlogPublisher
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isCredentialsNonExpired()Z == &isCredentialsNonExpired
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isDetailsUpdateable()Z == &isDetailsUpdateable
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isEnabled()Z == &isEnabled
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.isUserInRole(Ljava/lang/String;)Z == &isUserInRole
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setDetailsUpdateable(Z)V == &setDetailsUpdateable
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setEmailAddress(Ljava/lang/String;)V == &setEmailAddress
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setGrantedAuthories([Lorg/acegisecurity/GrantedAuthority;)V == &setGrantedAuthories
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setName(Ljava/lang/String;)V == &setName
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setPassword(Ljava/lang/String;)V == &setPassword
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setPreferences(Ljava/util/Map;)V == &setPreferences
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setProfile(Ljava/lang/String;)V == &setProfile
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setUsername(Ljava/lang/String;)V == &setUsername
    //#post(net.sourceforge.pebble.security.PebbleUserDetails__static_init): __Dispatch_Table.setWebsite(Ljava/lang/String;)V == &setWebsite
    //#pebbleuserdetails.java:: end of method: net.sourceforge.pebble.security.PebbleUserDetails.net.sourceforge.pebble.security.PebbleUserDetails__static_init
    //#pebbleuserdetails.java:: end of class: net.sourceforge.pebble.security.PebbleUserDetails
