Class cast exception in matmat-par_2_2_2.mmp

[ywei]

the command is:
tass verify matmat-par_2_2_2.mmp -np 2

and I got this exception
java.lang.ClassCastException: edu.udel.cis.vsl.minimp.value.impl.SymbolicValue

at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.referenceValue(Evaluator.java:79)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.executeInvocation(Executor.java:170)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.executeInvocation(Executor.java:185)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.execute(Executor.java:73)
at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:74)
at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:19)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:141)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:102)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:90)
at edu.udel.cis.vsl.minimp.Minimp.verify(Minimp.java:441)
at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:535)

It looks like the program was trying to cast a symbolic value to a reference value.

[Stephen Siegel]

When message is received, instead of being stored into cell pointed to by recv buffer arg, it is being stuck in recv buffer arg (which is an array variable in this case). Fixing...

[Stephen Siegel]

I think I have fixed the problem, but it only revealed a new problem which is that it is possible to try to assign a value to a variable of incompatible type. This can happen for arrays, because the dimensions are determined dynamically. It can actually happen with just about any type, because of sends and receives: there is no static checking. The solution is to introduce a method compatible() in the value factory which will check that a given symbolic value is compatible with a given variable (can be assigned to that variable). This sill have to go into the symbolic value and the type of the value. Should not be too difficult.