Merge pull request #6667 from tautschnig/bugfixes/string-abstraction-typecast

String abstraction: gracefully handle type casts from non-char types

Author: tautschnig

regression/cbmc/String_Abstraction24/main.c

@@ -0,0 +1,21 @@
+#include <stdint.h>
+#include <stdlib.h>
+#include <string.h>
+
+int main()
+{
+  size_t len;
+  __CPROVER_assume(0 < len);
+  uint16_t *data = malloc(len * sizeof(uint16_t));
+  if(data)
+  {
+    len = (len + 1) * sizeof(uint16_t);
+    uint16_t *ptr = malloc(len);
+    if(ptr)
+    {
+      memcpy(ptr, data, len);
+      ptr[len] = 0;
+    }
+  }
+  return 0;
+}

regression/cbmc/String_Abstraction24/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--string-abstraction
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed
+--
+String abstraction is not necessarily precise enough to reason across type casts
+from non-char pointer types, but must not fail to process such examples.

src/goto-programs/string_abstraction.cpp

@@ -651,12 +651,18 @@ exprt string_abstractiont::build(
   // take care of pointer typecasts now
   if(pointer.id()==ID_typecast)
   {
+    const exprt &op = to_typecast_expr(pointer).op();
+
     // cast from another pointer type?
-    if(to_typecast_expr(pointer).op().type().id() != ID_pointer)
+    if(
+      op.type().id() != ID_pointer ||
+      !is_char_type(to_pointer_type(op.type()).base_type()))
+    {
       return build_unknown(what, write);
+    }
 
     // recursive call
-    return build(to_typecast_expr(pointer).op(), what, write, source_location);
+    return build(op, what, write, source_location);
   }
 
   exprt str_struct;