Merge pull request #4481 from JohnDumbell/jd/enhancement/isx_double_cast

i2x cast back to int for byte, short and char

Author: JohnDumbell

jbmc/regression/jbmc/i2x_argument_double_cast/IntToX.class

@@ -0,0 +1,47 @@
+public class IntToX {
+    public void shortCast(int arg) {
+        intMethod((byte)arg);
+        assert true;
+    }
+
+    public void byteCast(int arg) {
+        intMethod((short)arg);
+        assert true;
+    }
+
+    public void charCast(int arg) {
+        intMethod((char)arg);
+        assert true;
+    }
+
+    public void floatCast(int arg) {
+        floatMethod((float)arg);
+        assert true;
+    }
+
+    public float floatMethod(float f) {
+        return f;
+    }
+
+    public void longCast(int arg) {
+        longMethod((long)arg);
+        assert true;
+    }
+
+    public float longMethod(long f) {
+        return f;
+    }
+
+    public void doubleCast(int arg) {
+        doubleMethod((double)arg);
+        assert true;
+    }
+
+    public double doubleMethod(double f) {
+        return f;
+    }
+
+    public int intMethod(int i) {
+        return i;
+    }
+}

jbmc/regression/jbmc/i2x_argument_double_cast/IntToX.java

@@ -0,0 +1,8 @@
+CORE
+IntToX.class
+--function IntToX.byteCast
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/i2x_argument_double_cast/byte.desc

@@ -0,0 +1,8 @@
+CORE
+IntToX.class
+--function IntToX.charCast
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/i2x_argument_double_cast/char.desc

@@ -0,0 +1,8 @@
+CORE
+IntToX.class
+--function IntToX.doubleCast
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/i2x_argument_double_cast/double.desc

@@ -0,0 +1,8 @@
+CORE
+IntToX.class
+--function IntToX.floatCast
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/i2x_argument_double_cast/float.desc

@@ -0,0 +1,8 @@
+CORE
+IntToX.class
+--function IntToX.longCast
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/i2x_argument_double_cast/long.desc

@@ -0,0 +1,8 @@
+CORE
+IntToX.class
+--function IntToX.shortCast
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/i2x_argument_double_cast/short.desc

@@ -1582,6 +1582,15 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       PRECONDITION(op.size() == 1 && results.size() == 1);
       typet type=java_type_from_char(statement[2]);
       results[0] = typecast_exprt::conditional_cast(op[0], type);
+
+      // These types get converted/truncated then immediately turned back into
+      // ints again, so we just double-cast here.
+      if(
+        type == java_char_type() || type == java_byte_type() ||
+        type == java_short_type())
+      {
+        results[0] = typecast_exprt(results[0], java_int_type());
+      }
     }
     else if(statement=="new")
     {