Merge pull request #4998 from smowton/smowton/fix/lhs-string-constant

[TG-8994] Tolerate a constant on the LHS of an assignment

Author: smowton

regression/cbmc/lhs-pointer-aliases-constant/test.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int x;
+  const char *c = "Hello world";
+
+  int *p = (argc ? &x : (int *)c);
+
+  *p = 1;
+
+  assert(*p == 1);
+
+  return 0;
+}

regression/cbmc/lhs-pointer-aliases-constant/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that we tolerate an apparent write to a string constant, which of course
+can't happen in reality but may appear to happen due to over-approximate alias analysis.

src/goto-symex/goto_symex_state.h

@@ -247,9 +247,12 @@ class goto_symex_statet final : public goto_statet
   /// Returns true if \p lvalue is a read-only object, such as the null object
   static bool is_read_only_object(const exprt &lvalue)
   {
+    // Note ID_constant can occur due to a partial write to a string constant,
+    // (i.e. something like byte_extract int from "hello" offset 2), which
+    // 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() == "zero_string_length" || lvalue.id() == ID_constant;
   }
 
 private: