Test we don't call static initialisers unnecessarily

Previously we couldn't properly track when we had definitely already called
them.

Author: owen-mc-diffblue

jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.class

@@ -0,0 +1,7 @@
+public class ClassWithStaticInit {
+  public static int x;
+
+  static { x = 42; }
+
+  public static int getStaticValue() { return x; }
+}

jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.java

@@ -0,0 +1,17 @@
+public class Test {
+  public static void test(boolean b) {
+    int x;
+    if (b) {
+      x = ClassWithStaticInit.getStaticValue();
+    }
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    x = ClassWithStaticInit.getStaticValue();
+    assert (false);
+  }
+}

jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.class

@@ -0,0 +1,16 @@
+CORE
+Test.class
+--function Test.test --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+--
+java::ClassWithStaticInit::clinit_already_run#[1-9][0-9]
+^warning: ignoring
+--
+After the second call to ClassWithStaticInit.getStaticValue(), symex should have
+java::ClassWithStaticInit::clinit_already_run in its constant propagator with
+the value true, and hence the static initialiser won't need to be run again.
+It's quite hard to check this in a test, so we check that the generation of
+java::ClassWithStaticInit::clinit_already_run doesn't get into double digits
+despite many calls to ClassWithStaticInit.getStaticValue(). Hopefully this isn't
+brittle to small changes in how often generations are updated.