From 30866b59b0bc87d6146e4073af3b46ccf84e2cef Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Thu, 15 Jun 2017 09:54:08 +0100
Subject: [PATCH 1/2] Force simplification of cast-from-universal-integer

These are otherwise illegal expressions (at least to boolbvt), and so
get ignored. This problem usually doesn't show up as it requires
--no-simplify to escape subsequent incidental simplification.
---
 src/java_bytecode/java_bytecode_convert_method.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index f9f75e45dbe..b80a67cdb8c 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/prefix.h>
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>
+#include <util/simplify_expr.h>
 
 #include <linking/zero_initializer.h>
 
@@ -1416,7 +1417,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("?ipush"))
     {
       assert(results.size()==1);
-      results[0]=typecast_exprt(arg0, java_int_type());
+      namespacet ns(symbol_table);
+      // Force a simplify here in case we have --no-simplify
+      // because the simplifier is the only pass that knows how to
+      // deal with this cast from integer_typet:
+      results[0]=simplify_expr(typecast_exprt(arg0, java_int_type()), ns);
     }
     else if(statement==patternt("if_?cmp??"))
     {

From e2e23608b700aa6f01971fb6c4477bb03a111c9b Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Thu, 15 Jun 2017 09:57:52 +0100
Subject: [PATCH 2/2] Add test for Java integers with --no-simplify

See issue cbmc#1015 for detail.
---
 .../integer_without_simplify1/test.class          | Bin 0 -> 232 bytes
 .../cbmc-java/integer_without_simplify1/test.desc |   7 +++++++
 .../cbmc-java/integer_without_simplify1/test.java |  10 ++++++++++
 .../java_bytecode_convert_method.cpp              |   9 ++++-----
 4 files changed, 21 insertions(+), 5 deletions(-)
 create mode 100644 regression/cbmc-java/integer_without_simplify1/test.class
 create mode 100644 regression/cbmc-java/integer_without_simplify1/test.desc
 create mode 100644 regression/cbmc-java/integer_without_simplify1/test.java

diff --git a/regression/cbmc-java/integer_without_simplify1/test.class b/regression/cbmc-java/integer_without_simplify1/test.class
new file mode 100644
index 0000000000000000000000000000000000000000..1ee5d36d95a1146b40d261aa0fd1d49b7d1ec54a
GIT binary patch
literal 232
zcmYL?%?`m(5QWe5zg6@FB<!%zL@XN{iIuP*_HA9#rrM-#y_c25!UK3HG1r1w%+Ghu
z%)H)@Cx96`9(1&9_%_-EE6U1D&I$T(v?myg>L3W+RaT01b52CPi<5#09SPpHYU)%h
zGX-2JE^?B`*Vu;vlUEfW1PX;kT%N*Bl8aPg0F6JY(7-mBoGqSuT#2hWzJqSu5NyuY
d7b>gsv-Ww?STllY^mlq+X7O={b(eJw-Um~HA(Q|B

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/integer_without_simplify1/test.desc b/regression/cbmc-java/integer_without_simplify1/test.desc
new file mode 100644
index 00000000000..284277c7b4a
--- /dev/null
+++ b/regression/cbmc-java/integer_without_simplify1/test.desc
@@ -0,0 +1,7 @@
+CORE
+test.class
+--no-simplify --function test.f --cover location
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/integer_without_simplify1/test.java b/regression/cbmc-java/integer_without_simplify1/test.java
new file mode 100644
index 00000000000..62b2060b7c0
--- /dev/null
+++ b/regression/cbmc-java/integer_without_simplify1/test.java
@@ -0,0 +1,10 @@
+
+public class test {
+
+  public void f() {
+
+    int x = 50;
+
+  }
+
+}
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index b80a67cdb8c..95bb864fa12 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1417,11 +1417,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("?ipush"))
     {
       assert(results.size()==1);
-      namespacet ns(symbol_table);
-      // Force a simplify here in case we have --no-simplify
-      // because the simplifier is the only pass that knows how to
-      // deal with this cast from integer_typet:
-      results[0]=simplify_expr(typecast_exprt(arg0, java_int_type()), ns);
+      mp_integer int_value;
+      bool ret=to_integer(to_constant_expr(arg0), int_value);
+      INVARIANT(!ret, "?ipush argument should be an integer");
+      results[0]=from_integer(int_value, java_int_type());
     }
     else if(statement==patternt("if_?cmp??"))
     {