Add a regression test for nondet-static

Author: svorenova

jbmc/regression/jbmc/nondet-static/My.class

@@ -0,0 +1,29 @@
+public class My {
+  public static int s_non_init;
+  public static int s_init = 1;
+  public static int s_static_init;
+  static { s_static_init = 2; }
+
+  public static final int sf_init = 1;
+  public static final int sf_static_init;
+  static { sf_static_init = 2; }
+
+  public int field;
+  public My(int i) {
+    String s = "bla";
+    field = i;
+    if (s_non_init != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (s_init != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (s_static_init != 2)
+      field = 108; // this line can only be covered with nondet-static
+
+    if (sf_init != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (sf_static_init != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (s != "bla")
+      field = 108; // this line cannot be covered even with nondet-static
+  }
+}

jbmc/regression/jbmc/nondet-static/My.java

@@ -0,0 +1,19 @@
+CORE symex-driven-lazy-loading-expected-failure
+My.class
+--function "My.<init>" --cover location --nondet-static
+^EXIT=0$
+^SIGNAL=0$
+file My\.java line 18 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 19 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 20 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 25 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 27 function java::My\.\<init\>:\(I\)V.*FAILED$
+--
+file My\.java line 23 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+--
+This tests nondet-static option, namely that static (non-final) variables are
+non-det initialized regardless of whether they are given a (static) initializer
+or not but constants such as strings are not non-det initialized
+
+This fails under symex-driven lazy loading because nondet-static cannot be used
+with it