From 6d3167925b56c1c9c4c2b0a3b26fd1d62256507a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Feb 2019 23:34:36 +0000
Subject: [PATCH] Counterexamples: show strings, not address-of-character

Pointers to strings (or into strings) should not be printed as
address-of-character. This was an undesired side-effect of d4296f167 ("Use
get_subexpression_at_offset in pointer_logict").
---
 regression/cbmc/trace-strings/main.c     |  6 ++++++
 regression/cbmc/trace-strings/test.desc  | 10 ++++++++++
 src/solvers/flattening/pointer_logic.cpp | 14 ++++++++++++++
 src/util/simplify_expr.cpp               |  5 +++++
 4 files changed, 35 insertions(+)
 create mode 100644 regression/cbmc/trace-strings/main.c
 create mode 100644 regression/cbmc/trace-strings/test.desc

diff --git a/regression/cbmc/trace-strings/main.c b/regression/cbmc/trace-strings/main.c
new file mode 100644
index 00000000000..96c578993c1
--- /dev/null
+++ b/regression/cbmc/trace-strings/main.c
@@ -0,0 +1,6 @@
+int main()
+{
+  char *c = "abc";
+  ++c;
+  assert(0);
+}
diff --git a/regression/cbmc/trace-strings/test.desc b/regression/cbmc/trace-strings/test.desc
new file mode 100644
index 00000000000..59766b4c193
--- /dev/null
+++ b/regression/cbmc/trace-strings/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+c="abc"
+c=\{ 'b', 'c', 0 \}
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index 1d796e254e9..69d2f2694b7 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -104,6 +104,20 @@ exprt pointer_logict::pointer_expr(
   // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
   if(subtype.id() == ID_empty)
     subtype = char_type();
+  if(object_expr.id() == ID_string_constant)
+  {
+    subtype = object_expr.type();
+
+    // a string constant must be array-typed with fixed size
+    const array_typet &array_type = to_array_type(object_expr.type());
+    mp_integer array_size =
+      numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
+    if(array_size > pointer.offset)
+    {
+      to_array_type(subtype).size() =
+        from_integer(array_size - pointer.offset, array_type.size().type());
+    }
+  }
   exprt deep_object =
     get_subexpression_at_offset(object_expr, pointer.offset, subtype, ns);
   CHECK_RETURN(deep_object.is_not_nil());
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index e7e3fd32764..fb6702e8067 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "rational_tools.h"
 #include "simplify_utils.h"
 #include "std_expr.h"
+#include "string_constant.h"
 #include "string_expr.h"
 #include "symbol.h"
 #include "type_eq.h"
@@ -1795,6 +1796,10 @@ optionalt<std::string> simplify_exprt::expr2bits(
         constant_exprt(value, to_c_enum_type(type).subtype()), little_endian);
     }
   }
+  else if(expr.id() == ID_string_constant)
+  {
+    return expr2bits(to_string_constant(expr).to_array_expr(), little_endian);
+  }
   else if(expr.id()==ID_union)
   {
     return expr2bits(to_union_expr(expr).op(), little_endian);