id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
314	ArrayIndexOutOfBoundsException in morph (via state)	zirkel	Stephen Siegel	"When running TASS with the Clang frontend on example.xml, there is an exception when trying to access a variable in a local (block) scope.

{{{
Exception in thread ""main"" java.lang.ArrayIndexOutOfBoundsException: Array index out of range: 1
	at edu.udel.cis.vsl.tass.morph.MorphicVector.get(MorphicVector.java:53)
	at edu.udel.cis.vsl.tass.state.impl.ModelEnvironment.setValueLocal(ModelEnvironment.java:297)
	at edu.udel.cis.vsl.tass.state.impl.ModelEnvironment.setValue(ModelEnvironment.java:219)
	at edu.udel.cis.vsl.tass.state.impl.Environment.setValue(Environment.java:455)
	at edu.udel.cis.vsl.tass.semantics.impl.Executor.assignValue(Executor.java:361)
	at edu.udel.cis.vsl.tass.semantics.impl.Executor.assignValue(Executor.java:440)
	at edu.udel.cis.vsl.tass.semantics.impl.Executor.executeReturnStatement(Executor.java:553)
	at edu.udel.cis.vsl.tass.semantics.impl.Executor.execute(Executor.java:196)
	at edu.udel.cis.vsl.tass.kripke.impl.StateManager.nextStateSimple(StateManager.java:1195)
	at edu.udel.cis.vsl.tass.kripke.impl.StateManager.immediateNextState(StateManager.java:605)
	at edu.udel.cis.vsl.tass.kripke.impl.StateManager.nextState(StateManager.java:527)
	at edu.udel.cis.vsl.tass.kripke.impl.StateManager.nextState(StateManager.java:1)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.proceedToNewState(DfsSearcher.java:204)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:156)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:137)
	at edu.udel.cis.vsl.tass.verify.impl.CollectiveVerifier.searchGeneric(CollectiveVerifier.java:242)
	at edu.udel.cis.vsl.tass.verify.impl.CollectiveVerifier.search(CollectiveVerifier.java:217)
	at edu.udel.cis.vsl.tass.verify.Verify.verify(Verify.java:30)
	at edu.udel.cis.vsl.tass.ui.Runner.run(Runner.java:175)
	at edu.udel.cis.vsl.tass.TASS.main(TASS.java:28)
}}}"	defect	closed	major	1.1	state	1.1	fixed	example.xml, clang, scope, local, block, morphic, model environment