[Javapathfinder-user] ArrayStoreException on a standard JPF run

[Anthony A. <aa...@cs...>]

Hello all,

I do hope this is the appropriate forum for sending out a question. If  
not, please accept my sincerest apologies. I have posted in the  
SourceForge forum but it looks quite tranquil there.

When running JPF against a set of dynamically spawning Thread  
subclasses, I receive a java.lang.ArrayStoreException assigning a  
variable declared as int to an initialized object-level array of ints.  
I'm not sure how this is possible. When I run the code outside of JPF  
I never receive this exception. Even stranger, under JPF the line  
executes several times successfully and then fails with this  
exception. All of this is sequential, taking place in a single thread.

Is there anything anyone is aware of that JPF might be doing to  
conceivably attempt to assign a non-integer value here, when the  
variable on the right of the assignment is explicitly (and locally)  
declared int? I'm utterly at a loss about this.

I would heartily appreciate any insight anyone has on this. The code  
in question is as follows:

public int[] fire(int[] m, int e) {
int[] n = m.clone();
for(int z: n) System.out.println("[ -> " + z);
System.out.println("------");
int i;
int t = getTransition(e);
if(t == -1) return null;
for(i = 0; i < arcs[t][0].length; i++) {
n[arcs[t][0][i][0]] -= arcs[t][0][i][1]; // *** ArrayStoreException  
occurs *here* ***
if(n[arcs[t][0][i][0]] < 0)
return null;
}
for(i = 0; i < arcs[t][1].length; i++)
n[arcs[t][1][i][0]] += arcs[t][1][i][1];
return n;
}