Bug for \old initializations

[JonasKlamroth]

`//@ ensures (\forall int i; 0 <= i < \old(table.length); i % 2 == 0 ==> \old(table[i + 1]) == 0);

`

This is an example for which JJBMC will create a false positive index out of bounds warning. The problem here is that the quantified variable i is further restricted by the implication. However when initializing the old value this restriction is not considered and thus the out of bounds exception occurs.

[JonasKlamroth]

public static void main(String args[]) {
    int[] a = new int[2];
    try {
      a[3] = 0;
    } catch (IndexOutOfBoundsException e) {

    }
  }

this example shows that just adding a catch claus does not help since jbmc still complains (which i consider to be a bug)

[mattulbrich]

There might be a switch to jbmc where you can allow/disallow implicit runtime exceptions (NPE, IOOBE etc)

[mattulbrich]

Can you paste the translation of the above ensures, esp. with the initialisation used to store \old(table).

[JonasKlamroth]

yes there is a switch however it does not work as i would expect (see the example which still resuts in an "uncaught" exception). Here is the translation:

int old0 = table.length;
int[] old1 = new int[4];
for (int i = 0; i <= old0 - 1; ++i) {
    try {
        old1[i % 4] = table[i + 1];
    } catch (java.lang.RuntimeException e) {
    }
}