Failure in GradeCount loop test

[Stephen Siegel]

I added a JUnit test for GradeCount. The loop technique is supposed to find the error after 19 states. Instead it gets a null pointer exception when trying to get the label of a "for" loop that does not have a label. It should execute that loop normally. It is the next "while" loop that corresponds to the loop in the spec and requires the loop technique.

Why did this example work before, and now now?

Yi---not sure if you have time to look into this but you could probably figure it out quickly.

[Stephen Siegel]

In the example on our web page http://vsl.cis.udel.edu/tass/examples/gradeCount.html
the arrays for grades and "for" loops do not exist. That is why it works there.
I am wondering if after this change to for loops was made, if it ever worked.
The problem is the loop technique is expecting the next loop it finds in the impl
to be the corresponding loop, but it isn't. It should however just execute this loop normally.

[ywei]

I have modified the Enabler class in loop package and I will check the hourly test results to see if it works. (Haven't set up the environment for TASS on my new computer so I can't run it locally.)

[ywei]

The example now proceeds normally, but the hourly test returned some error related to Java VM which I don't understand. (Forked Java VM exited abnormally)

[Stephen Siegel]

Test still fails; the JUnit report indicates that it timed out after 5 minutes. The problem appears to be in StateManager.nextState. In executing a loop transition, the values of all writevars must be reset to symbolic constants. However, this is not happening for arrays, because they are not included in the set of writevars, but rather in the set writerefs, obtained by method writerefs() in loop location.

[Stephen Siegel]

Fixed. Added writerefs to set of variables that get reset, and commented out an exit instruction when unlabeled loop is found in impl.