Add static-values tests with class substitution

This adds a test in which an non-empty class is replaced by an empty
class after compilation and before JBMC is called.
This used to cause a crash in the retrieval of static values.
This kind of substitution is not uncommon in the jar packaging of
libraries. A similar error was triggered when analyising a project which
used mongodb as a dependency, and mongodb seems to use such tricks.

Author: romainbrenguier

jbmc/regression/jbmc/deterministic_assignments_json/ClassWithNoStaticField.java

@@ -0,0 +1 @@
+public class ClassWithNoStaticField {}

jbmc/regression/jbmc/deterministic_assignments_json/ClassWithStaticFieldToBeSubstituted.class

@@ -0,0 +1 @@
+public class ClassWithStaticFieldToBeSubstituted { public static int i = 23; }

jbmc/regression/jbmc/deterministic_assignments_json/ClassWithStaticFieldToBeSubstituted.java

@@ -0,0 +1,9 @@
+public class EmptyNonEmpty {
+
+  /// This test is meant to illustrate what happens when a class
+  /// with a static field is substituted with an empty one after compilation.
+  public int test() {
+    int x = ClassWithStaticFieldToBeSubstituted.i;
+    return x;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/EmptyNonEmpty.class

@@ -0,0 +1,14 @@
+CORE
+EmptyNonEmpty.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function EmptyNonEmpty.test
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This tests what happens when the class with a static field is substituted with
+a class with no static field after compilation: after compiling
+ClassWithStaticFieldToBeSubstitued.class and ClassWithNoStaticField.class,
+we copy ClassWithNoStaticField.class to ClassWithStaticFieldToBeSubstitued.class
+in order to overwrite it.
+We should at least ensure that JBMC does not crash.