Factor out is_read_only_object function

Author: smowton

src/goto-symex/goto_symex_state.h

@@ -239,6 +239,14 @@ class goto_symex_statet final : public goto_statet
     return fresh_l2_name_provider;
   }
 
+  /// Returns true if \p lvalue is a read-only object, such as the null object
+  static bool is_read_only_object(const exprt &lvalue)
+  {
+    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";
+  }
+
 private:
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
 

src/goto-symex/symex_assign.cpp

@@ -67,11 +67,7 @@ void symex_assignt::assign_rec(
     assign_if(to_if_expr(lhs), full_lhs, rhs, guard);
   else if(lhs.id()==ID_typecast)
     assign_typecast(to_typecast_expr(lhs), full_lhs, rhs, guard);
-  else if(lhs.id() == ID_string_constant ||
-          lhs.id() == ID_null_object ||
-          lhs.id() == "zero_string" ||
-          lhs.id() == "is_zero_string" ||
-          lhs.id() == "zero_string_length")
+  else if(goto_symex_statet::is_read_only_object(lhs))
   {
     // ignore
   }