Merge pull request #1066 from diffblue/smowton/fix/json_trace_pointer_offset

Fix remove_pointer_offsets

Author: smowton

regression/cbmc-java/json_trace1/Test.class

@@ -0,0 +1,21 @@
+public class Test {
+
+  byte main(byte[] a) {
+    if (a.length != 9) {
+      return -1;
+    }
+
+    byte diff = 0;
+    for (byte i = 0; i < 9; i++) {
+      if (a[i] == 1) {
+        diff++;
+      } else if (a[i] == 2) {
+        diff--;
+      } else if (a[i] != 0) {
+        return -1;
+      }
+    }
+
+    return -1;
+  }
+}

regression/cbmc-java/json_trace1/Test.java

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--cover location --trace --json-ui
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-java/json_trace1/test.desc

@@ -17,6 +17,7 @@ Author: Daniel Kroening
 #include <util/arith_tools.h>
 
 #include <langapi/language_util.h>
+#include <solvers/flattening/pointer_logic.h>
 
 #include "json_goto_trace.h"
 
@@ -25,8 +26,16 @@ Author: Daniel Kroening
 /// \param src: an expression
 void remove_pointer_offsets(exprt &src)
 {
-  if(src.id()==ID_pointer_offset && src.op0().id()==ID_constant)
-    src=src.op0();
+  if(src.id()==ID_pointer_offset &&
+     src.op0().id()==ID_constant &&
+     src.op0().type().id()==ID_pointer)
+  {
+    std::string binary_str=id2string(to_constant_expr(src.op0()).get_value());
+    // The constant address consists of OBJECT-ID || OFFSET.
+    // Shift out the object-identifier bits, leaving only the offset:
+    mp_integer offset=binary2integer(binary_str.substr(BV_ADDR_BITS), false);
+    src=from_integer(offset, src.type());
+  }
   else
     for(auto &op : src.operands())
       remove_pointer_offsets(op);