Include pointer offset in counterexample output

While the bit-level pointer output would convey the information, the
human-readable expression previously did not consider non-zero offsets except
for null pointers.

Author: tautschnig

regression/cbmc/trace_address_arithmetic1/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+typedef struct
+{
+  int inta;
+  int intb;
+} struct_t;
+
+typedef union {
+  int intaa;
+  struct_t structbb;
+} union_struct_t;
+
+int main()
+{
+  union_struct_t uuu;
+  char *ptr = (char *)&uuu.structbb.intb;
+  int A[2];
+  int *ip = &A[1];
+  uuu.structbb.intb = 1;
+  // assert(*ptr == 1);
+  assert(0);
+}

regression/cbmc/trace_address_arithmetic1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+ptr=\(char \*\)&uuu!0@1 \+ 4(l+)? \(.*\)$
+ip=A!0@1 \+ 1(l+)? \(.*\)$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/solvers/flattening/pointer_logic.cpp

@@ -99,8 +99,33 @@ exprt pointer_logict::pointer_expr(
   const exprt &object_expr=objects[pointer.object];
 
   exprt deep_object=object_rec(pointer.offset, type, object_expr);
+  const address_of_exprt base(deep_object);
 
-  return address_of_exprt(deep_object, type);
+  if(pointer.offset == 0)
+    return typecast_exprt::conditional_cast(base, type);
+
+  const auto object_size = pointer_offset_size(deep_object.type(), ns);
+  if(object_size.has_value() && *object_size <= 1)
+  {
+    return typecast_exprt::conditional_cast(
+      plus_exprt(base, from_integer(pointer.offset, pointer_diff_type())),
+      type);
+  }
+  else if(object_size.has_value() && pointer.offset % *object_size == 0)
+  {
+    return typecast_exprt::conditional_cast(
+      plus_exprt(
+        base, from_integer(pointer.offset % *object_size, pointer_diff_type())),
+      type);
+  }
+  else
+  {
+    return typecast_exprt::conditional_cast(
+      plus_exprt(
+        typecast_exprt(base, pointer_type(char_type())),
+        from_integer(pointer.offset, pointer_diff_type())),
+      type);
+  }
 }
 
 exprt pointer_logict::object_rec(