Merge pull request #4973 from antlechner/antonia/vr-primitive-wrappers

[TG-8623] Fix primitive wrapper types in JSON value retriever

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

@@ -199,6 +199,148 @@ 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;
+  }
+
+  // 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;
+  }
+
+  public static Integer[] integerWrapperArray = {1111};
+  public static void testIntegerWrapperArrayPass() {
+    assert integerWrapperArray.length == 1 && integerWrapperArray[0] == 1111;
+  }
+  public static void testIntegerWrapperArrayFail() {
+    assert integerWrapperArray.length != 1 || integerWrapperArray[0] != 1111;
+  }
+
   // Strings
   public static String stringField = Util.repeat("hello! ", 6);
   public static void testStringPass() {

jbmc/regression/jbmc/deterministic_assignments_json/ContainerForFloat.java

@@ -412,6 +412,76 @@
         "@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
+    },
+    "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
+    },
+    "integerWrapperArray":{
+      "@type":"[Ljava.lang.Integer;",
+      "@items":[
+        1111
+      ]
     }
   },
   "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.testBooleanWrapperFail
+^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.testBooleanWrapperPass
+^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.testByteWrapperContainerFail
+^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.testByteWrapperContainerPass
+^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.testByteWrapperFail
+^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.testByteWrapperPass
+^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.testCharacterWrapperContainerFail
+^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.testCharacterWrapperContainerPass
+^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.testCharacterWrapperFail
+^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.testCharacterWrapperPass
+^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.testDoubleWrapperContainerFail
+^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.testDoubleWrapperContainerPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--