CBMC verification failure with --lazy-methods, brace-initialized static array

[reuk]

Using the current tip of test-gen-support (7cbe566), the following program fails verification when invoked with --lazy-methods and succeeds otherwise. The full command-line is cbmc Main.class (--lazy-methods).

class Problem {
  private static final Object[] DEFAULT = {};
  private Object data;

  Problem() {
    this.data = DEFAULT;
  }

  void checkInvariant() {
    assert data != null;
  }
}

public class Main {
  public static void main(String[] args) {
    new Problem().checkInvariant();
  }
}

@smowton, do you know why this might be?

[smowton]

Yep, the initialisation takes place in a static initialiser, and they currently aren't picked up by lazy method elaboration. Will put a patch together tomorrow morning.

[smowton]

@reuk I can't assign reviewers, but you should probably look at #855