Messages

method | net.sourceforge.pebble.trackback.TrackBackTokenMan ager$1__static_init

method | void net.sourceforge.pebble.trackback. TrackBackTokenManager$1(TrackBackTokenManager)

method | net.sourceforge.pebble.trackback.TrackBackTokenMan ager__static_init
post | instance == &new TrackBackTokenManager(TrackBac kTokenManager__static_init#1)
post | init'ed(log)
post | new HashMap(TrackBackTokenManager#2) num objects == 1
post | new Random(TrackBackTokenManager#1) num objects == 1
post | new TrackBackTokenManager(TrackBackTokenManager__ static_init#1) num objects == 1
post | instance.random == &new Random(TrackBackTokenMa nager#1)
post | instance.tokens == &new HashMap(TrackBackTokenM anager#2)
unanalyzed | call on java.util.Random
unanalyzed | call on java.util.HashMap
unanalyzed | call on java.util.TimerTask
unanalyzed | call on java.util.Timer
unanalyzed | call on java.util.Timer:schedule

method | Log access$0()
post | init'ed(return_value)

| info | method not available | -- call on Log org.apache.commons.logging. LogFactory:getLog(Class)

method | Map access$1(TrackBackTokenManager)
pre | Param_0 != null
pre | init'ed(Param_0.tokens)
post | return_value == Param_0.tokens
post | init'ed(return_value)

method | void net.sourceforge.pebble.trackback. TrackBackTokenManager()
post | this.random == &new Random(TrackBackTokenManage r#1)
post | this.tokens == &new HashMap(TrackBackTokenManag er#2)
post | new HashMap(TrackBackTokenManager#2) num objects == 1
post | new Random(TrackBackTokenManager#1) num objects == 1
unanalyzed | call on java.util.TimerTask

method | void run()
pre | this.tokens != null
presumption | java.util.Map:keySet(...)@36 != null
presumption | org.apache.commons.logging.LogFactory:getLog(... )@15 != null
unanalyzed | call on java.util.Date
unanalyzed | call on java.lang.String:length
unanalyzed | call on java.util.Map:get
unanalyzed | call on java.util.Date:getTime
test_vector | java.util.Iterator:hasNext(...)@37: {1}, {0}

| info | method not available | -- call on void org.apache.commons.logging. Log:debug(Object)

method | TrackBackTokenManager getInstance()
post | return_value == &new TrackBackTokenManager(Trac kBackTokenManager__static_init#1)

method | String generateToken()
pre | this.random != null
pre | this.tokens != null
post | return_value != null

method | bool isValid(String)
pre | (soft) this.tokens != null
post | init'ed(return_value)
test_vector | token: Addr_Set{null}, Inverse{null}
test_vector | java.lang.String:length(...)@78: {1.. 232-1}, {0}
test_vector | java.util.Map:get(...)@81: Addr_Set{null}, Inverse{null}

method | void expire(String)
pre | this.tokens != null