Symex: ignore assignments to string constant even through type casts

We previously ignored various forms of strings already, but failed to
consider the case where an array was created by simplification due to
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: