Mysterious Java symbolic execution

[vladrich]

In the following (distilled) program, xx is assigned only once. In the trace that CBMC generates, xx is assigned multiple times with different values. I suspect this causes problems in the full benchmark.

public final class MySecureRandom {

public static void main(String[] argv) {
    int index = 0;

    while (index < 20) {

        for (int i = 0; i < 20; i++) {
            index++;
        }
    }

    int xx = index;
    assert(xx==1);

}

}

[kroening]

Can you check wether pull requests #185 or #193 fix this?

[vladrich]

Not sure how to merge this with the fix for bug #197.

[mgudemann]

This is an instance of the error fixed in #185

    LocalVariableTable:
      Start  Length  Slot  Name   Signature
            10      15     2     i   I
             0      50     0  argv   [Ljava/lang/String;
             2      48     1 index   I
            30      20     2    xx   I

in the local variable table, xx has the same slot index as i and "shadows" it without the PR.

[kroening]

This now works.