Messages

method	net.sourceforge.pebble.PebbleContext__static_init
presumption	org.apache.commons.logging.LogFactory:getLog(... )@52 != null
post	instance == &new PebbleContext(PebbleContext__ static_init#1)
post	(soft) log != null
post	new Date(PebbleContext#1) num objects == 1
post	new PebbleContext(PebbleContext__static_init#1) num objects == 1
post	possibly_updated(instance.buildVersion)
post	instance.startTime == &new Date(PebbleContext#1 )
unanalyzed	call on java.util.Date
unanalyzed	call on java.util.Properties
unanalyzed	call on java.lang.Object:getClass
unanalyzed	call on java.lang.Class:getClassLoader
unanalyzed	call on java.lang.ClassLoader:getResourceAsStream
unanalyzed	call on java.util.Properties:load
unanalyzed	call on java.util.Properties:getProperty
unanalyzed	call on java.io.InputStream:close
unanalyzed	call on org.apache.commons.logging.Log:warn
unanalyzed	call on java.io.IOException:getMessage
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on java.io.IOException:printStackTrace

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

method	PebbleContext getInstance()
post	return_value == &new PebbleContext(PebbleContex t__static_init#1)

method	void net.sourceforge.pebble.PebbleContext()
pre	(soft) log != null
presumption	java.lang.Class:getClassLoader(...)@80 != null
presumption	java.lang.Object:getClass(...)@80 != null
post	possibly_updated(this.buildVersion)
post	this.startTime == &new Date(PebbleContext#1)
post	new Date(PebbleContext#1) num objects == 1
test_vector	java.lang.ClassLoader:getResourceAsStream(...)@80: Addr_Set{null}, Inverse{null}

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

info method not available -- call on void org.apache.commons.logging. Log:error(Object, Throwable)

method	String getBuildVersion()
pre	init'ed(this.buildVersion)
post	return_value == this.buildVersion
post	init'ed(return_value)

method	RelativeDate getUptime()
pre	this.startTime != null
presumption	java.util.Date:getTime(...)@121 - java.util. Date:getTime(...)@121 in -18_446_744_073_709_551_61 5..2⁶³
post	return_value == &new RelativeDate(getUptime#1)
post	new RelativeDate(getUptime#1) num objects == 1
post	(soft) init'ed(return_value.time)

method	long getMemoryUsageInKB()
presumption	(-(java.lang.Runtime:freeMemory(...)@125 - java.lang.Runtime:totalMemory(...)@125))/1_024 in -27_021_597_764_222_975..27_021_597_764_222_975
presumption	java.lang.Runtime:getRuntime(...)@125 != null
post	return_value in -27_021_597_764_222_975.. 27_021_597_764_222_975

method	long getTotalMemoryInKB()
presumption	java.lang.Runtime:getRuntime(...)@129 != null
presumption	java.lang.Runtime:totalMemory(...)@129/1_024 in -9_007_199_254_740_992..18_014_398_509_481_983
post	return_value in -9_007_199_254_740_992.. 18_014_398_509_481_983

method	Configuration getConfiguration()
pre	init'ed(this.configuration)
post	return_value == this.configuration
post	init'ed(return_value)

method	void setConfiguration(Configuration)
post	this.configuration == configuration
post	init'ed(this.configuration)

method	void setWebApplicationRoot(String)
post	this.webApplicationRoot == webApplicationRoot
post	init'ed(this.webApplicationRoot)

method	String getWebApplicationRoot()
pre	init'ed(this.webApplicationRoot)
post	return_value == this.webApplicationRoot
post	init'ed(return_value)