id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
277	NullPointerException in ModelEnvironment	zirkel		"Running IntegrateTest gives a NullPointerException.

{{{
java.lang.NullPointerException
	at edu.udel.cis.vsl.tass.state.impl.ModelEnvironment.computeReachableHeap(ModelEnvironment.java:976)
	at edu.udel.cis.vsl.tass.state.impl.ModelEnvironment.canonicalizeHeap(ModelEnvironment.java:841)
	at edu.udel.cis.vsl.tass.state.impl.Environment.canonicalizeHeap(Environment.java:548)
	at edu.udel.cis.vsl.tass.semantics.impl.Executor.executeReturnStatement(Executor.java:439)
	at edu.udel.cis.vsl.tass.semantics.impl.Executor.execute(Executor.java:150)
	at edu.udel.cis.vsl.tass.kripke.impl.StateManager.nextStateSimple(StateManager.java:1119)
	at edu.udel.cis.vsl.tass.kripke.impl.StateManager.immediateNextState(StateManager.java:550)
	at edu.udel.cis.vsl.tass.kripke.impl.StateManager.nextState(StateManager.java:476)
	at edu.udel.cis.vsl.tass.kripke.impl.StateManager.nextState(StateManager.java:1)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.proceedToNewState(DfsSearcher.java:197)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:149)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:130)
	at edu.udel.cis.vsl.tass.verify.impl.CollectiveVerifier.searchGeneric(CollectiveVerifier.java:231)
	at edu.udel.cis.vsl.tass.verify.impl.CollectiveVerifier.search(CollectiveVerifier.java:206)
	at edu.udel.cis.vsl.tass.verify.Verify.verify(Verify.java:30)
	at integrate.IntegrateTest.testVerifySpec(IntegrateTest.java:37)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:44)
	at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:15)
	at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:41)
	at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:20)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:76)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:50)
	at org.junit.runners.ParentRunner$3.run(ParentRunner.java:193)
	at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:52)
	at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:191)
	at org.junit.runners.ParentRunner.access$000(ParentRunner.java:42)
	at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:184)
	at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
	at org.junit.runners.ParentRunner.run(ParentRunner.java:236)
	at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:49)
	at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:467)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:683)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:390)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:197)


}}}"	defect	closed	major		state		fixed