Add a regression test for nondet-static

Author: svorenova

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

@@ -0,0 +1,21 @@
+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 int field;
+
+  public My(int i) {
+    String s = "bla";
+    field = i;
+
+    /* Pass normally but fail with nondet-static */
+    assert(s_non_init == 0);
+    assert(s_init == 1);
+    assert(s_static_init == 2);
+
+    /* Should still pass */
+    assert(s == "bla");
+  }
+}

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

@@ -0,0 +1,15 @@
+CORE
+My.class
+--function "My.<init>" --nondet-static
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+assertion at file My\.java line 14 function java::My\.\<init\>:\(I\)V.*FAILURE$
+assertion at file My\.java line 15 function java::My\.\<init\>:\(I\)V.*FAILURE$
+assertion at file My\.java line 16 function java::My\.\<init\>:\(I\)V.*FAILURE$
+assertion at file My\.java line 19 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+--
+--
+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