//# 0 errors, 132 messages
//#
package net.sourceforge.pebble.trackback;
    //#trackbacktokenmanager.java:1:1: class: net.sourceforge.pebble.trackback.TrackBackTokenManager$1
    //#trackbacktokenmanager.java:1:1: method: net.sourceforge.pebble.trackback.TrackBackTokenManager$1.net.sourceforge.pebble.trackback.TrackBackTokenManager$1__static_init
    //#trackbacktokenmanager.java:1:1: class: net.sourceforge.pebble.trackback.TrackBackTokenManager
    //#trackbacktokenmanager.java:1: method: void net.sourceforge.pebble.trackback.TrackBackTokenManager$1.net.sourceforge.pebble.trackback.TrackBackTokenManager$1(TrackBackTokenManager)
    //#input(void net.sourceforge.pebble.trackback.TrackBackTokenManager$1(TrackBackTokenManager)): Param_1
    //#input(void net.sourceforge.pebble.trackback.TrackBackTokenManager$1(TrackBackTokenManager)): this
    //#output(void net.sourceforge.pebble.trackback.TrackBackTokenManager$1(TrackBackTokenManager)): this.this$0
    //#post(void net.sourceforge.pebble.trackback.TrackBackTokenManager$1(TrackBackTokenManager)): this.this$0 == Param_1
    //#post(void net.sourceforge.pebble.trackback.TrackBackTokenManager$1(TrackBackTokenManager)): init'ed(this.this$0)

import org.apache.commons.logging.Log;
import org.apache.commons.logging.LogFactory;

import java.util.*;

/**
 * Manages tokens for generating TrackBack links.
 *
 * @author    Simon Brown
 */
public class TrackBackTokenManager {

  private static final Log log = LogFactory.getLog(TrackBackTokenManager.class);
    //#trackbacktokenmanager.java:15: method: net.sourceforge.pebble.trackback.TrackBackTokenManager.net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init
    //#trackbacktokenmanager.java:15: Warning: method not available
    //#    -- call on Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.trackback.TrackBackTokenManager
    //#    method: net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init
    //#    unanalyzed callee: Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): __Descendant_Table[net/sourceforge/pebble/trackback/TrackBackTokenManager]
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): __Dispatch_Table.expire(Ljava/lang/String;)V
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): __Dispatch_Table.generateToken()Ljava/lang/String;
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): __Dispatch_Table.isValid(Ljava/lang/String;)Z
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): instance
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): log
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): new HashMap(TrackBackTokenManager#2) num objects
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): new Random(TrackBackTokenManager#1) num objects
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): new TrackBackTokenManager(TrackBackTokenManager__static_init#1) num objects
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): instance.__Tag
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): instance.random
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): instance.tokens
    //#new obj(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): new HashMap(TrackBackTokenManager#2)
    //#new obj(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): new Random(TrackBackTokenManager#1)
    //#new obj(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): new TrackBackTokenManager(TrackBackTokenManager__static_init#1)
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): __Descendant_Table[net/sourceforge/pebble/trackback/TrackBackTokenManager] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): __Dispatch_Table.expire(Ljava/lang/String;)V == &expire
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): __Dispatch_Table.generateToken()Ljava/lang/String; == &generateToken
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): __Dispatch_Table.isValid(Ljava/lang/String;)Z == &isValid
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): instance == &new TrackBackTokenManager(TrackBackTokenManager__static_init#1)
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): init'ed(log)
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): new HashMap(TrackBackTokenManager#2) num objects == 1
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): new Random(TrackBackTokenManager#1) num objects == 1
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): new TrackBackTokenManager(TrackBackTokenManager__static_init#1) num objects == 1
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): instance.__Tag == net/sourceforge/pebble/trackback/TrackBackTokenManager
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): instance.random == &new Random(TrackBackTokenManager#1)
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): instance.tokens == &new HashMap(TrackBackTokenManager#2)
    //#unanalyzed(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): Effects-of-calling:java.util.Random
    //#unanalyzed(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): Effects-of-calling:java.util.HashMap
    //#unanalyzed(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): Effects-of-calling:java.util.TimerTask
    //#unanalyzed(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): Effects-of-calling:java.util.Timer
    //#unanalyzed(net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init): Effects-of-calling:java.util.Timer:schedule
    //#trackbacktokenmanager.java:15: method: Log net.sourceforge.pebble.trackback.TrackBackTokenManager.access$0()
    //#input(Log access$0()): log
    //#output(Log access$0()): return_value
    //#post(Log access$0()): init'ed(return_value)
    //#trackbacktokenmanager.java:15: end of method: Log net.sourceforge.pebble.trackback.TrackBackTokenManager.access$0()

  private static final TrackBackTokenManager instance = new TrackBackTokenManager();
    //#trackbacktokenmanager.java:17: end of method: net.sourceforge.pebble.trackback.TrackBackTokenManager.net.sourceforge.pebble.trackback.TrackBackTokenManager__static_init

  /** the time to live for new tokens */
  private static final long TIME_TO_LIVE = 1000 * 60 * 10; // 10 minutes

  private Random random = new Random();

  /** the map of tokens */
  private Map<String,Date> tokens = new HashMap<String,Date>();
    //#trackbacktokenmanager.java:25: method: Map net.sourceforge.pebble.trackback.TrackBackTokenManager.access$1(TrackBackTokenManager)
    //#input(Map access$1(TrackBackTokenManager)): Param_0
    //#input(Map access$1(TrackBackTokenManager)): Param_0.tokens
    //#output(Map access$1(TrackBackTokenManager)): return_value
    //#pre[1] (Map access$1(TrackBackTokenManager)): Param_0 != null
    //#pre[2] (Map access$1(TrackBackTokenManager)): init'ed(Param_0.tokens)
    //#post(Map access$1(TrackBackTokenManager)): return_value == Param_0.tokens
    //#post(Map access$1(TrackBackTokenManager)): init'ed(return_value)
    //#trackbacktokenmanager.java:25: end of method: Map net.sourceforge.pebble.trackback.TrackBackTokenManager.access$1(TrackBackTokenManager)

  /**
   * Private constructor for the singleton pattern.
   */
  private TrackBackTokenManager() {
    //#trackbacktokenmanager.java:30: method: void net.sourceforge.pebble.trackback.TrackBackTokenManager.net.sourceforge.pebble.trackback.TrackBackTokenManager()
    //#input(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): this
    //#output(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): new HashMap(TrackBackTokenManager#2) num objects
    //#output(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): new Random(TrackBackTokenManager#1) num objects
    //#output(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): this.random
    //#output(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): this.tokens
    //#new obj(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): new HashMap(TrackBackTokenManager#2)
    //#new obj(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): new Random(TrackBackTokenManager#1)
    //#post(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): this.random == &new Random(TrackBackTokenManager#1)
    //#post(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): this.tokens == &new HashMap(TrackBackTokenManager#2)
    //#post(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): new HashMap(TrackBackTokenManager#2) num objects == 1
    //#post(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): new Random(TrackBackTokenManager#1) num objects == 1
    //#unanalyzed(void net.sourceforge.pebble.trackback.TrackBackTokenManager()): Effects-of-calling:java.util.TimerTask
    // create a new TimerTask that will purge invalid tokens
    TimerTask task = new TimerTask() {
    //#trackbacktokenmanager.java:32: end of method: void net.sourceforge.pebble.trackback.TrackBackTokenManager$1.net.sourceforge.pebble.trackback.TrackBackTokenManager$1(TrackBackTokenManager)
      public void run() {
        synchronized (TrackBackTokenManager.this) {
    //#trackbacktokenmanager.java:34: method: void net.sourceforge.pebble.trackback.TrackBackTokenManager$1.run()
    //#input(void run()): net/sourceforge/pebble/trackback/TrackBackTokenManager.__Descendant_Table[net/sourceforge/pebble/trackback/TrackBackTokenManager]
    //#input(void run()): net/sourceforge/pebble/trackback/TrackBackTokenManager.__Descendant_Table[others]
    //#input(void run()): net/sourceforge/pebble/trackback/TrackBackTokenManager.__Dispatch_Table.isValid(Ljava/lang/String;)Z
    //#input(void run()): net/sourceforge/pebble/trackback/TrackBackTokenManager.log
    //#input(void run()): this
    //#input(void run()): this.this$0
    //#input(void run()): this.this$0.__Tag
    //#input(void run()): this.this$0.tokens
    //#pre[4] (void run()): this.tokens != null
    //#pre[2] (void run()): (soft) this.this$0 != null
    //#pre[3] (void run()): (soft) this.__Tag == net/sourceforge/pebble/trackback/TrackBackTokenManager
    //#presumption(void run()): java.util.Map:keySet(...)@36 != null
    //#presumption(void run()): org.apache.commons.logging.LogFactory:getLog(...)@15 != null
    //#unanalyzed(void run()): Effects-of-calling:java.util.Date
    //#unanalyzed(void run()): Effects-of-calling:java.lang.String:length
    //#unanalyzed(void run()): Effects-of-calling:java.util.Map:get
    //#unanalyzed(void run()): Effects-of-calling:java.util.Date:getTime
    //#test_vector(void run()): java.util.Iterator:hasNext(...)@37: {1}, {0}
          log.debug("Purging expired tokens");
    //#trackbacktokenmanager.java:35: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.trackback.TrackBackTokenManager$1
    //#    method: void run()
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
          Iterator it = tokens.keySet().iterator();
          while (it.hasNext()) {
            String token = (String)it.next();
            if (!isValid(token)) {
              it.remove();
            }
          }
        }
      }
    //#trackbacktokenmanager.java:44: end of method: void net.sourceforge.pebble.trackback.TrackBackTokenManager$1.run()
    };

    Timer timer = new Timer();
    timer.schedule(task, 2 * TIME_TO_LIVE);
  }
    //#trackbacktokenmanager.java:49: end of method: void net.sourceforge.pebble.trackback.TrackBackTokenManager.net.sourceforge.pebble.trackback.TrackBackTokenManager()

  /**
   * Gets the singleton instance of this class.
   *
   * @return    a TrackBackTokenManager instance
   */
  public static TrackBackTokenManager getInstance() {
    return instance;
    //#trackbacktokenmanager.java:57: method: TrackBackTokenManager net.sourceforge.pebble.trackback.TrackBackTokenManager.getInstance()
    //#input(TrackBackTokenManager getInstance()): instance
    //#output(TrackBackTokenManager getInstance()): return_value
    //#post(TrackBackTokenManager getInstance()): return_value == &new TrackBackTokenManager(TrackBackTokenManager__static_init#1)
    //#trackbacktokenmanager.java:57: end of method: TrackBackTokenManager net.sourceforge.pebble.trackback.TrackBackTokenManager.getInstance()
  }

  /**
   * Generates a new token with a fixed time to live.
   *
   * @return  a new token
   */
  public synchronized String generateToken() {
    String token = "" + random.nextLong();
    //#trackbacktokenmanager.java:66: method: String net.sourceforge.pebble.trackback.TrackBackTokenManager.generateToken()
    //#input(String generateToken()): this
    //#input(String generateToken()): this.random
    //#input(String generateToken()): this.tokens
    //#output(String generateToken()): return_value
    //#pre[2] (String generateToken()): this.random != null
    //#pre[3] (String generateToken()): this.tokens != null
    //#post(String generateToken()): return_value != null
    tokens.put(token, new Date());
    return token;
    //#trackbacktokenmanager.java:68: end of method: String net.sourceforge.pebble.trackback.TrackBackTokenManager.generateToken()
  }

  /**
   * Determines whether a given token is valid.
   *
   * @param token   the token to test
   * @return  true if the token is valid and hasn't expired, false otherwise
   */
  public synchronized boolean isValid(String token) {
    if (token == null || token.length() == 0) {
    //#trackbacktokenmanager.java:78: method: bool net.sourceforge.pebble.trackback.TrackBackTokenManager.isValid(String)
    //#input(bool isValid(String)): this
    //#input(bool isValid(String)): this.tokens
    //#input(bool isValid(String)): token
    //#output(bool isValid(String)): return_value
    //#pre[2] (bool isValid(String)): (soft) this.tokens != null
    //#post(bool isValid(String)): init'ed(return_value)
    //#test_vector(bool isValid(String)): token: Addr_Set{null}, Inverse{null}
    //#test_vector(bool isValid(String)): java.lang.String:length(...)@78: {1..4_294_967_295}, {0}
    //#test_vector(bool isValid(String)): java.util.Map:get(...)@81: Addr_Set{null}, Inverse{null}
      return false;
    } else {
      Date date = tokens.get(token);
      return (date != null) && (new Date().getTime() - date.getTime() <= TIME_TO_LIVE);
    //#trackbacktokenmanager.java:82: end of method: bool net.sourceforge.pebble.trackback.TrackBackTokenManager.isValid(String)
    }
  }

  /**
   * Expires a given token.
   *
   * @param token   the token to be expired
   */
  public synchronized void expire(String token) {
    tokens.remove(token);
    //#trackbacktokenmanager.java:92: method: void net.sourceforge.pebble.trackback.TrackBackTokenManager.expire(String)
    //#input(void expire(String)): this
    //#input(void expire(String)): this.tokens
    //#input(void expire(String)): token
    //#pre[2] (void expire(String)): this.tokens != null
  }
    //#trackbacktokenmanager.java:93: end of method: void net.sourceforge.pebble.trackback.TrackBackTokenManager.expire(String)

}    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager$1__static_init): __Descendant_Table[net/sourceforge/pebble/trackback/TrackBackTokenManager$1]
    //#output(net.sourceforge.pebble.trackback.TrackBackTokenManager$1__static_init): __Dispatch_Table.run()V
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager$1__static_init): __Descendant_Table[net/sourceforge/pebble/trackback/TrackBackTokenManager$1] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.trackback.TrackBackTokenManager$1__static_init): __Dispatch_Table.run()V == &run
    //#trackbacktokenmanager.java:: end of method: net.sourceforge.pebble.trackback.TrackBackTokenManager$1.net.sourceforge.pebble.trackback.TrackBackTokenManager$1__static_init
    //#trackbacktokenmanager.java:: end of class: net.sourceforge.pebble.trackback.TrackBackTokenManager$1
    //#trackbacktokenmanager.java:: end of class: net.sourceforge.pebble.trackback.TrackBackTokenManager
