Fix issue with set and non-bit-sized value

Author: Enrico Steffinlongo

src/goto-symex/shadow_memory.cpp

@@ -154,11 +154,18 @@ void shadow_memoryt::symex_set_field(
         << ". Insert a cast to the type that you want to access.";
       throw invalid_input_exceptiont(s.str());
     }
+
+    // Get the type of the shadow memory for this field
+    const typet &sm_field_type = get_field_init_type(field_name, state);
+    // Add a conditional cast to the shadow memory field type if `rhs` is not of
+    // the expected type
+    const exprt casted_rhs =
+      typecast_exprt::conditional_cast(rhs, sm_field_type);
     // We replicate the rhs value on each byte of the value that we set.
     // This allows the get_field or/max semantics to operate correctly
     // on unions.
     const auto per_byte_rhs =
-      expr_initializer(lhs.type(), expr.source_location(), ns, rhs);
+      expr_initializer(lhs.type(), expr.source_location(), ns, casted_rhs);
     CHECK_RETURN(per_byte_rhs.has_value());
 
 #ifdef DEBUG_SM

src/goto-symex/shadow_memory_util.cpp

@@ -256,6 +256,13 @@ get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state)
   return field_type_it->second;
 }
 
+const typet &
+get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state)
+{
+  const exprt &field_init_expr = get_field_init_expr(field_name, state);
+  return field_init_expr.type();
+}
+
 /// Given a pointer expression `address` checks if any expr in value_set is
 /// compatible
 bool contains_null_or_invalid(

src/goto-symex/shadow_memory_util.h

@@ -109,6 +109,10 @@ std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
   const typet &lhs_type,
   bool &exact_match);
 
+// TODO: doxygen
+const typet &
+get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state);
+
 // TODO: doxygen
 bool contains_null_or_invalid(
   const std::vector<exprt> &value_set,