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	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.. 2³²-1}, {0}
test_vector	java.util.Map:get(...)@81: Addr_Set{null}, Inverse{null}

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