Merge pull request #4903 from tautschnig/memcpy-strings

Support OBJECT_SIZE over string constants

Author: tautschnig

regression/cbmc/String8/main.c

@@ -0,0 +1,19 @@
+int main()
+{
+  _Bool branch;
+  const char *str = 0;
+
+  if(branch)
+  {
+    str = "foo";
+  }
+  else
+  {
+    str = "bar";
+  }
+
+  char a = str[2];
+  __CPROVER_assert(a == 'o' || a == 'r', "");
+
+  return 0;
+}

regression/cbmc/String8/test.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/solvers/flattening/bv_pointers.cpp

@@ -768,7 +768,7 @@ void bv_pointerst::do_postponed(
     {
       const exprt &expr=*it;
 
-      if(expr.id() != ID_symbol)
+      if(expr.id() != ID_symbol && expr.id() != ID_string_constant)
         continue;
 
       const auto size_expr = size_of_expr(expr.type(), ns);

src/solvers/smt2/smt2_conv.cpp

@@ -220,7 +220,8 @@ void smt2_convt::define_object_size(
       numeric_cast<mp_integer>(size_expr.value_or(nil_exprt()));
 
     if(
-      o.id() != ID_symbol || !size_expr.has_value() || !object_size.has_value())
+      (o.id() != ID_symbol && o.id() != ID_string_constant) ||
+      !size_expr.has_value() || !object_size.has_value())
     {
       ++number;
       continue;