Merge pull request #6741 from tautschnig/bugfixes/ignore-array

Symex: ignore assignments to string constant even through type casts

Author: tautschnig

regression/cbmc/string_assignment1/main.c

@@ -0,0 +1,15 @@
+typedef char array_t[2][2];
+
+void foo(array_t(*a))
+{
+  unsigned char i = 0;
+  unsigned char j = 0;
+  (*a)[i][j] = 0;
+}
+
+unsigned char main()
+{
+  char *x = "abcd";
+  foo(x);
+  __CPROVER_assert(x[0] == 'a', "a");
+}

regression/cbmc/string_assignment1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^l2_rename_rvalues case `array' not handled
+^warning: ignoring
+--
+The assignment to a C string constant should be ignored by symex, even when it
+happens via a type cast to a two-dimensional array.

src/goto-symex/goto_symex_state.h

@@ -251,7 +251,8 @@ class goto_symex_statet final : public goto_statet
     // simplifies to a plain constant.
     return lvalue.id() == ID_string_constant || lvalue.id() == ID_null_object ||
            lvalue.id() == "zero_string" || lvalue.id() == "is_zero_string" ||
-           lvalue.id() == "zero_string_length" || lvalue.id() == ID_constant;
+           lvalue.id() == "zero_string_length" || lvalue.id() == ID_constant ||
+           lvalue.id() == ID_array;
   }
 
 private: