[TG-7706] Add new JSON value assignment feature for static fields

jbmc/regression/jbmc/deterministic_assignments_json/Bar.java

@@ -0,0 +1,12 @@
+public class Bar {
+  private static int c = Util.setTo(10);
+  private int x;
+
+  public Bar(int x) {
+    this.x = Util.setTo(x);
+  }
+
+  public int get() {
+    return x + c;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/Color.java

@@ -0,0 +1,29 @@
+public enum Color {
+  RED(false),
+  BLUE(false),
+  GREEN(false),
+  WHITE(true),
+  GREY(true),
+  BLACK(true);
+
+  private boolean grayscale;
+
+  Color(boolean grayscale) {
+    this.grayscale = grayscale;
+  }
+
+  public boolean isGrayscale() {
+    return grayscale;
+  }
+
+  public static Color enumField = Color.WHITE;
+  public static void testEnumInOwnTypePass() {
+    assert enumField == Color.WHITE && enumField.name().equals("WHITE") &&
+        enumField.ordinal() == 3 && enumField.isGrayscale();
+  }
+  public static void testEnumInOwnTypeFail() {
+    assert enumField != Color.WHITE || !enumField.name().equals("WHITE") ||
+        enumField.ordinal() != 3 || !enumField.isGrayscale();
+  }
+
+}

jbmc/regression/jbmc/deterministic_assignments_json/Foo.java

@@ -0,0 +1,14 @@
+public class Foo {
+  private int i;
+  private Bar b;
+
+  public Foo(int i, int x)
+  {
+    this.i = Util.setTo(i);
+    this.b = new Bar(x);
+  }
+
+  public int get() {
+    return i + b.get();
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementation.java

@@ -0,0 +1,20 @@
+public class GenericImplementation<T> implements GenericInterface<T> {
+
+  T[] elements;
+
+  public GenericImplementation(T[] array) {
+    elements = array;
+  }
+
+  public int size() {
+    return elements.length;
+  }
+
+  public T first() {
+    return elements[0];
+  }
+
+  public int num() {
+    return 5;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationLess.java

@@ -0,0 +1,21 @@
+public class GenericImplementationLess implements GenericInterface<Foo> {
+
+  Foo[] elements;
+
+  public GenericImplementationLess(Foo[] array) {
+    elements = array;
+  }
+
+  public int size() {
+    return elements.length;
+  }
+
+  public Foo first() {
+    return elements[0];
+  }
+
+  public int num() {
+    return first().get();
+  }
+
+}

jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationMore.java

@@ -0,0 +1,25 @@
+public class GenericImplementationMore<T, U> implements GenericInterface<T> {
+
+  T[] elementsT;
+  U[] elementsU;
+
+  public GenericImplementationMore(T[] arrayT, U[] arrayU) {
+    elementsT = arrayT;
+    elementsU = arrayU;
+  }
+
+  public int size() {
+    return elementsT.length + elementsU.length;
+  }
+
+  public T first() {
+    return elementsT[0];
+  }
+
+  public int num() {
+    if (elementsU[0] instanceof Bar) {
+      return ((Bar) elementsU[0]).get();
+    }
+    return elementsU.length;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/GenericImplementationSimpleMore.java

@@ -0,0 +1,22 @@
+public class GenericImplementationSimpleMore<T, U> implements GenericInterface<T> {
+  T t;
+  U u;
+
+  public GenericImplementationSimpleMore(T t, U u) {
+    this.t = t;
+    this.u = u;
+  }
+
+  public int size() {
+    return 2;
+  }
+  public T first() {
+    return t;
+  }
+  public int num() {
+    if (u instanceof Bar) {
+      return ((Bar) u).get();
+    }
+    return 1;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/GenericInterface.java

@@ -0,0 +1,8 @@
+public interface GenericInterface<T> {
+
+  int size();
+
+  T first();
+
+  int num();
+}

jbmc/regression/jbmc/deterministic_assignments_json/GenericMultiDim.java

@@ -0,0 +1,11 @@
+public class GenericMultiDim<K, V> {
+
+  public K key;
+  public V value;
+
+  public GenericMultiDim(K k, V v) {
+    key = k;
+    value = v;
+  }
+
+}

jbmc/regression/jbmc/deterministic_assignments_json/GenericType.java

@@ -0,0 +1,8 @@
+public class GenericType<T> {
+  public T field;
+
+  public GenericType(T f) {
+    field = f;
+  }
+
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractClass.java

@@ -0,0 +1,8 @@
+public abstract class MyAbstractClass {
+
+  abstract public int num();
+
+  public int concreteNum() {
+    return 11;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationA.java

@@ -0,0 +1,5 @@
+public class MyAbstractImplementationA extends MyAbstractClass {
+  public int num() {
+    return concreteNum();
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyAbstractImplementationB.java

@@ -0,0 +1,5 @@
+public class MyAbstractImplementationB extends MyAbstractClass {
+  public int num() {
+    return 2 * concreteNum();
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyClassWithInheritedFields.java

@@ -0,0 +1,10 @@
+public class MyClassWithInheritedFields extends MyParent {
+  int childField = Util.setTo(4);
+
+  public static int sum(MyClassWithInheritedFields myTemp) {
+    int sum = myTemp.childField + myTemp.parentField;
+    if (sum == 10)
+      return sum;
+    return sum;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyConcreteClass.java

@@ -0,0 +1,8 @@
+public class MyConcreteClass {
+
+  public static int numField = Util.setTo(10);
+
+  public int num() {
+    return numField;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationA.java

@@ -0,0 +1,6 @@
+public class MyImplementationA implements MyInterface {
+  int field = Util.setTo(11);
+  public int num() {
+    return field;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyImplementationB.java

@@ -0,0 +1,6 @@
+public class MyImplementationB implements MyInterface {
+  int field = Util.setTo(22);
+  public int num() {
+    return field;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyInterface.java

@@ -0,0 +1,5 @@
+public interface MyInterface {
+
+  int num();
+
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerA.java

@@ -0,0 +1,6 @@
+public class MyInterfaceContainerA {
+  MyImplementationA field = new MyImplementationA();
+  public MyInterface getField() {
+    return field;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyInterfaceContainerB.java

@@ -0,0 +1,6 @@
+public class MyInterfaceContainerB {
+  MyInterface field = new MyImplementationB();
+  public MyInterface getField() {
+    return field;
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/MyParent.java

@@ -0,0 +1,4 @@
+public class MyParent {
+  int parentField = Util.setTo(3);
+  String parentString = "parent";
+}

jbmc/regression/jbmc/deterministic_assignments_json/MySubclassA.java

@@ -0,0 +1,6 @@
+public class MySubclassA extends MyConcreteClass {
+  @Override
+  public int num() {
+    return 2 * super.num();
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/MySubclassB.java

@@ -0,0 +1,6 @@
+public class MySubclassB extends MyConcreteClass {
+  @Override
+  public int num() {
+    return 3 * super.num();
+  }
+}

jbmc/regression/jbmc/deterministic_assignments_json/OtherClass.java

@@ -0,0 +1,4 @@
+public class OtherClass {
+
+  public static Foo otherField = new Foo(12, 24);
+}

jbmc/regression/jbmc/deterministic_assignments_json/README

@@ -0,0 +1,10 @@
+This directory contains tests for the --static-values feature: reading initial
+values of static fields from a JSON file.
+Most of the tests are in StaticValues.java, some more tests are included in
+Color.java, and all other classes are used to create instances of various kinds
+of objects to use in the tests.
+The initial static field values are read from the file clinit-state.json.
+The script generate-json.sh (which calls org.cprover.JsonGenerator in the Maven
+project) can be used to generate output similar to the contents of
+clinit-state.json (with slightly less pretty-printing/newlines, which are not
+supported in the custom writers and were manually added to clinit-state.json).

jbmc/regression/jbmc/deterministic_assignments_json/StaticParent.java

@@ -0,0 +1,3 @@
+public class StaticParent {
+  protected static int inheritedStatic = Util.setTo(10);
+}