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;
}
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Hello all,
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;
}