Merge pull request #4241 from tautschnig/cex-string

Counterexamples: show strings, not address-of-character

Author: tautschnig

regression/cbmc/trace-strings/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  char *c = "abc";
+  ++c;
+  assert(0);
+}

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

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());

src/util/simplify_expr.cpp

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 #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);