Opened 15 years ago

Closed 15 years ago

#314 closed defect (fixed)

ArrayIndexOutOfBoundsException in morph (via state)

Reported by: zirkel Owned by: Stephen Siegel
Priority: major Milestone: 1.1
Component: state Version: 1.1
Keywords: example.xml, clang, scope, local, block, morphic, model environment Cc:

Description

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)

Change History (2)

comment:1 by Stephen Siegel, 15 years ago

Owner: set to Stephen Siegel
Status: new → accepted

comment:2 by Stephen Siegel, 15 years ago

Resolution: → fixed
Status: accepted → closed

Was assuming that the start location had to be in outermost scope.
Got rid of that assumption and fixed a number of other bugs related to scopes.
Local variables are initialized when entering a scope.
Example now verifies successfully.

Note: See TracTickets for help on using tickets.