Add tests for static fields with references to primitive wrappers

In this case, the values are represented as simple JSON numbers,
booleans or strings. This did not work before the recent fix for
primitive wrapper types.

Author: antlechner

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForBoolean.class

@@ -0,0 +1,4 @@
+public class ContainerForBoolean {
+  public Boolean booleanField;
+  public ContainerForBoolean(Boolean b) { booleanField = b; }
+}

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForBoolean.java

@@ -0,0 +1,4 @@
+public class ContainerForByte {
+  public Byte byteField;
+  public ContainerForByte(Byte b) { byteField = b; }
+}

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForByte.class

@@ -0,0 +1,4 @@
+public class ContainerForCharacter {
+  public Character characterField;
+  public ContainerForCharacter(Character c) { characterField = c; }
+}

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForByte.java

@@ -0,0 +1,4 @@
+public class ContainerForDouble {
+  public Double doubleField;
+  public ContainerForDouble(Double d) { doubleField = d; }
+}

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForCharacter.class

@@ -0,0 +1,4 @@
+public class ContainerForFloat {
+  public Float floatField;
+  public ContainerForFloat(Float f) { floatField = f; }
+}

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForCharacter.java

@@ -0,0 +1,4 @@
+public class ContainerForInteger {
+  public Integer integerField;
+  public ContainerForInteger(Integer i) { integerField = Util.setTo(i); }
+}

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForDouble.class

@@ -0,0 +1,4 @@
+public class ContainerForLong {
+  public Long longField;
+  public ContainerForLong(Long l) { longField = l; }
+}

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForDouble.java

@@ -0,0 +1,4 @@
+public class ContainerForShort {
+  public Short shortField;
+  public ContainerForShort(Short s) { shortField = s; }
+}

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForFloat.class

@@ -260,6 +260,79 @@ public static void testShortWrapperFail() {
     assert shortWrapperField != (short)200;
   }
 
+  // Primitive wrapper types as fields of static field types
+  public static ContainerForBoolean booleanWrapperContainer =
+      new ContainerForBoolean(true);
+  public static void testBooleanWrapperContainerPass() {
+    assert booleanWrapperContainer.booleanField;
+  }
+  public static void testBooleanWrapperContainerFail() {
+    assert !booleanWrapperContainer.booleanField;
+  }
+
+  public static ContainerForByte byteWrapperContainer =
+      new ContainerForByte((byte)50);
+  public static void testByteWrapperContainerPass() {
+    assert byteWrapperContainer.byteField == (byte)50;
+  }
+  public static void testByteWrapperContainerFail() {
+    assert byteWrapperContainer.byteField != (byte)50;
+  }
+
+  public static ContainerForCharacter characterWrapperContainer =
+      new ContainerForCharacter('!');
+  public static void testCharacterWrapperContainerPass() {
+    assert characterWrapperContainer.characterField == '!';
+  }
+  public static void testCharacterWrapperContainerFail() {
+    assert characterWrapperContainer.characterField != '!';
+  }
+
+  public static ContainerForDouble doubleWrapperContainer =
+      new ContainerForDouble(24.56);
+  public static void testDoubleWrapperContainerPass() {
+    assert doubleWrapperContainer.doubleField == 24.56;
+  }
+  public static void testDoubleWrapperContainerFail() {
+    assert doubleWrapperContainer.doubleField != 24.56;
+  }
+
+  public static ContainerForFloat floatWrapperContainer =
+      new ContainerForFloat(13.13f);
+  public static void testFloatWrapperContainerPass() {
+    assert floatWrapperContainer.floatField == 13.13f;
+  }
+  public static void testFloatWrapperContainerFail() {
+    assert floatWrapperContainer.floatField != 13.13f;
+  }
+
+  public static ContainerForInteger integerWrapperContainer =
+      new ContainerForInteger(1000);
+  public static void testIntegerWrapperContainerPass() {
+    assert integerWrapperContainer.integerField == 1000;
+  }
+  public static void testIntegerWrapperContainerFail() {
+    assert integerWrapperContainer.integerField != 1000;
+  }
+
+  public static ContainerForLong longWrapperContainer =
+      new ContainerForLong(21000000000L);
+  public static void testLongWrapperContainerPass() {
+    assert longWrapperContainer.longField == 21000000000L;
+  }
+  public static void testLongWrapperContainerFail() {
+    assert longWrapperContainer.longField != 21000000000L;
+  }
+
+  public static ContainerForShort shortWrapperContainer =
+      new ContainerForShort((short)200);
+  public static void testShortWrapperContainerPass() {
+    assert shortWrapperContainer.shortField == (short)200;
+  }
+  public static void testShortWrapperContainerFail() {
+    assert shortWrapperContainer.shortField != (short)200;
+  }
+
   // Strings
   public static String stringField = Util.repeat("hello! ", 6);
   public static void testStringPass() {

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForFloat.java

@@ -444,6 +444,38 @@
     "shortWrapperField":{
       "@type":"java.lang.Short",
       "value":200
+    },
+    "booleanWrapperContainer":{
+      "@type":"ContainerForBoolean",
+      "booleanField":true
+    },
+    "byteWrapperContainer":{
+      "@type":"ContainerForByte",
+      "byteField":50
+    },
+    "characterWrapperContainer":{
+      "@type":"ContainerForCharacter",
+      "characterField":"!"
+    },
+    "doubleWrapperContainer":{
+      "@type":"ContainerForDouble",
+      "doubleField":24.56
+    },
+    "floatWrapperContainer":{
+      "@type":"ContainerForFloat",
+      "floatField":13.13
+    },
+    "integerWrapperContainer":{
+      "@type":"ContainerForInteger",
+      "integerField":1000
+    },
+    "longWrapperContainer":{
+      "@type":"ContainerForLong",
+      "longField":"21000000000"
+    },
+    "shortWrapperContainer":{
+      "@type":"ContainerForShort",
+      "shortField":200
     }
   },
   "OtherClass":{

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForInteger.class

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testBooleanWrapperContainerFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForInteger.java

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testBooleanWrapperContainerPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForLong.class

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testByteWrapperContainerFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForLong.java

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testByteWrapperContainerPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForShort.class

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testCharacterWrapperContainerFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForShort.java

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testCharacterWrapperContainerPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.class

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testDoubleWrapperContainerFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.java

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testDoubleWrapperContainerPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/clinit-state.json

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testFloatWrapperContainerFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_boolean_wrapper_container_fail.desc

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testFloatWrapperContainerPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_boolean_wrapper_container_pass.desc

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testIntegerWrapperContainerFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_byte_wrapper_container_fail.desc

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testIntegerWrapperContainerPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_byte_wrapper_container_pass.desc

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testLongWrapperContainerFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_character_wrapper_container_fail.desc

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testLongWrapperContainerPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_character_wrapper_container_pass.desc

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testShortWrapperContainerFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_double_wrapper_container_fail.desc

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testShortWrapperContainerPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--