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/Empty.java

@@ -0,0 +1,3 @@
+public class Empty {
+
+}

jbmc/regression/jbmc/deterministic_assignments_json/EmptyNonEmpty.class

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

jbmc/regression/jbmc/deterministic_assignments_json/EmptyNonEmpty.java

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

jbmc/regression/jbmc/deterministic_assignments_json/NonEmpty.class

@@ -0,0 +1,12 @@
+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 non-empty class is substitued with an empty
+one after compilation: After compiling EmptyNonEmpty.class and Empty.class,
+Empty.class is moved to NonEmpty.class.
+We should at least ensure that JBMC does not crash.