[TG-9450] Allocate reference arrays with constant size in assignments from json

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.java

@@ -0,0 +1,36 @@
+class Util {
+  public static char[] chars(int count) {
+    char result[] = new char[count];
+    for (int i = 0; i < count; ++i) {
+      result[i] = (char)((int)'a' + i);
+    }
+    return result;
+  }
+}
+
+public class Test {
+  // static field which is initialized to a non-empty value
+  public static char[] staticCharArray = Util.chars(26);
+  // reference to the same array
+  public static char[] staticCharArrayRef = staticCharArray;
+
+  public static char[] charArray() {
+    staticCharArray[0] = staticCharArray[3];
+    staticCharArray[1] = 'e';
+    assert staticCharArray[0] == 'd';
+    assert staticCharArray[0] == 'A';
+    return staticCharArray;
+  }
+
+  public static char[] charArrayRef() {
+    staticCharArrayRef[0] = staticCharArray[3];
+    staticCharArray[1] = 'e';
+    if (staticCharArray[0] == 'A') {
+      assert false;
+    } else if (staticCharArray[0] == 'd') {
+      assert false;
+    }
+
+    return staticCharArray;
+  }
+}

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/static-values.json

@@ -0,0 +1,17 @@
+{
+    "@type":"com.diffblue.retriever.StaticFieldMap",
+    "Test":{
+        "@type":"com.diffblue.retriever.StaticFieldMap",
+        "staticCharArrayRef":{
+            "@type":"[C",
+            "@ref": "id1"
+        },
+        "staticCharArray":{
+            "@type":"[C",
+            "@id": "id1",
+            "@items":[
+                "abcAefghijklmnopqrstuvwxyz"
+            ]
+        }
+    }
+}

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc

@@ -0,0 +1,13 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.charArrayRef --property "java::Test.charArrayRef:()[C.assertion.2" --static-values static-values.json
+Generated 0 VCC[(]s[)], 0 remaining after simplification
+assertion at file Test.java line 31 .*: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Not that the json file has been modified on purpose so that this checks
+that it is actually loaded and not retrieved by execution of the Util function.
+This test does not work with symex-driven-lazy-loading because this option is
+not compatible with --property.

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc

@@ -0,0 +1,13 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.charArrayRef --property "java::Test.charArrayRef:()[C.assertion.1"
+Generated 0 VCC[(]s[)], 0 remaining after simplification
+assertion at file Test.java line 29 .*: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Note that the json file has been modified on purpose so that this checks
+that it is actually loaded and not retrieved by execution of the Util function.
+This test does not work with symex-driven-lazy-loading because this option is
+not compatible with --property.

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc

@@ -0,0 +1,13 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.charArray --property "java::Test.charArray:()[C.assertion.2" --static-values static-values.json
+Generated 0 VCC[(]s[)], 0 remaining after simplification
+assertion at file Test.java line 21 .*: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Note that the json file has been modified on purpose so that this checks
+that it is actually loaded and not retrieved by execution of the Util function.
+This test does not work with symex-driven-lazy-loading because this option is
+not compatible with --property.

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc

@@ -0,0 +1,12 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.charArray --property "java::Test.charArray:()[C.assertion.1"
+Generated 0 VCC[(]s[)], 0 remaining after simplification
+assertion at file Test.java line 20 .*: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Checks that constant propagation happens through static arrays.
+This test does not work with symex-driven-lazy-loading because this option is
+not compatible with --property.

jbmc/src/java_bytecode/Makefile

@@ -3,6 +3,7 @@ SRC = assignments_from_json.cpp \
       character_refine_preprocess.cpp \
       ci_lazy_methods.cpp \
       ci_lazy_methods_needed.cpp \
+      code_with_references.cpp \
       convert_java_nondet.cpp \
       create_array_with_type_intrinsic.cpp \
       expr2java.cpp \