Multiple_errors = true stopped to the first one

[Adri]

Hello,

I would like to submit a potentiel problem with the variable search.multiple_errors = true, the program is stopped after the first error.

According to the following example

public static void main(String args[]) {

    String a = args[0];

    String b = args[1];

    String c = args[2];

}

Output

...

search.multiple_error=true

...

====================================================== error 1

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty

java.lang.ArrayIndexOutOfBoundsException: 0

        at tutorial.MyClient.main(tutorial/MyClient.java:6)

====================================================== snapshot #1

thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}

  call stack:

        at tutorial.MyClient.main(MyClient.java:6)

====================================================== results

error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArrayIndexOutOfBoundsException: 0  at tu..."

The expected output woulb be to have 3 errors displayed. One for each args[n]

Best regards

[Cyrille Artho]

Hi Adri,

Thank you for finding this. I think this option is rarely used so there might have been a regression long ago that stopped this from working. Can you please createa a unit test case for this?

[Cyrille Artho]

Hi again,

As Darko remarked, this is not a bug, because all errors happen on the same execution path. So JPF works as expected here.

If you had three threads, each of which accessing an array element that is out of bounds, then the default would be that JPF finds an error with one thread, and with multiple_errors=true, JPF reports an error for each thread.

[Adri]

Hi cyrill,

Thanks for the answer.
Nevertheless, is it an option to detect all bugs in the program? In the previous example, if I correct the first line (String a = args[0]) JPF will detect the next error (String b = args[1]).
But it would be interesting to detect all the errors at the same time and to have a "long" report with all the errors.