Add tests for static fields of primitive wrapper type

In this case, the values are represented as JSON objects with @type
keys. This already worked before the fix in the previous commit.

Author: antlechner

jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.class

@@ -199,6 +199,67 @@ public static void testReferenceToReferenceArrayFail() {
     assert referenceToReferenceArray != referenceArrayField;
   }
 
+  // Primitive wrapper types as static field types
+  public static Boolean booleanWrapperField = true;
+  public static void testBooleanWrapperPass() { assert booleanWrapperField; }
+  public static void testBooleanWrapperFail() { assert !booleanWrapperField; }
+
+  public static Byte byteWrapperField = (byte)50;
+  public static void testByteWrapperPass() {
+    assert byteWrapperField == (byte)50;
+  }
+  public static void testByteWrapperFail() {
+    assert byteWrapperField != (byte)50;
+  }
+
+  public static Character characterWrapperField = '!';
+  public static void testCharacterWrapperPass() {
+    assert characterWrapperField == '!';
+  }
+  public static void testCharacterWrapperFail() {
+    assert characterWrapperField != '!';
+  }
+
+  public static Double doubleWrapperField = 24.56;
+  public static void testDoubleWrapperPass() {
+    assert doubleWrapperField == 24.56;
+  }
+  public static void testDoubleWrapperFail() {
+    assert doubleWrapperField != 24.56;
+  }
+
+  public static Float floatWrapperField = 13.13f;
+  public static void testFloatWrapperPass() {
+    assert floatWrapperField == 13.13f;
+  }
+  public static void testFloatWrapperFail() {
+    assert floatWrapperField != 13.13f;
+  }
+
+  public static Integer integerWrapperField = Util.setTo(1000);
+  public static void testIntegerWrapperPass() {
+    assert integerWrapperField == 1000;
+  }
+  public static void testIntegerWrapperFail() {
+    assert integerWrapperField != 1000;
+  }
+
+  public static Long longWrapperField = 21000000000L;
+  public static void testLongWrapperPass() {
+    assert longWrapperField == 21000000000L;
+  }
+  public static void testLongWrapperFail() {
+    assert longWrapperField != 21000000000L;
+  }
+
+  public static Short shortWrapperField = (short)200;
+  public static void testShortWrapperPass() {
+    assert shortWrapperField == (short)200;
+  }
+  public static void testShortWrapperFail() {
+    assert shortWrapperField != (short)200;
+  }
+
   // Strings
   public static String stringField = Util.repeat("hello! ", 6);
   public static void testStringPass() {

jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.java

@@ -412,6 +412,38 @@
         "@type":"java.lang.Boolean",
         "value":true
       }
+    },
+    "booleanWrapperField":{
+      "@type":"java.lang.Boolean",
+      "value":true
+    },
+    "byteWrapperField":{
+      "@type":"java.lang.Byte",
+      "value":50
+    },
+    "characterWrapperField":{
+      "@type":"java.lang.Character",
+      "value":"!"
+    },
+    "doubleWrapperField":{
+      "@type":"java.lang.Double",
+      "value":24.56
+    },
+    "floatWrapperField":{
+      "@type":"java.lang.Float",
+      "value":13.13
+    },
+    "integerWrapperField":{
+      "@type":"java.lang.Integer",
+      "value":1000
+    },
+    "longWrapperField":{
+      "@type":"java.lang.Long",
+      "value":"21000000000"
+    },
+    "shortWrapperField":{
+      "@type":"java.lang.Short",
+      "value":200
     }
   },
   "OtherClass":{

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.testBooleanWrapperFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_boolean_wrapper_field_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.testBooleanWrapperPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_boolean_wrapper_field_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.testByteWrapperFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_byte_wrapper_field_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.testByteWrapperPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_byte_wrapper_field_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.testCharacterWrapperFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_character_wrapper_field_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.testCharacterWrapperPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_character_wrapper_field_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.testDoubleWrapperFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_double_wrapper_field_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.testDoubleWrapperPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_double_wrapper_field_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.testFloatWrapperFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_float_wrapper_field_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.testFloatWrapperPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_float_wrapper_field_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.testIntegerWrapperFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_integer_wrapper_field_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.testIntegerWrapperPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_integer_wrapper_field_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.testLongWrapperFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_long_wrapper_field_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.testLongWrapperPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_long_wrapper_field_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.testShortWrapperFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_short_wrapper_field_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.testShortWrapperPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--