Merge pull request #6683 from tautschnig/bugfixes/mmio-cast

MMIO rewriting must maintain type consistency

Author: kroening

regression/cbmc/mm_io1/main.c

@@ -16,6 +16,7 @@ int main()
 {
   long i=0x10;
   char *p=(char *)i;
+  unsigned char u = *(unsigned char *)i;
   char some_var=100;
 
   char z;

src/goto-programs/mm_io.cpp

@@ -62,7 +62,10 @@ void mm_io(
           source_locationt source_location = it->source_location();
           const code_typet &ct=to_code_type(mm_io_r.type());
 
-          if_exprt if_expr(integer_address(d.pointer()), mm_io_r_value, d);
+          if_exprt if_expr(
+            integer_address(d.pointer()),
+            typecast_exprt::conditional_cast(mm_io_r_value, d.type()),
+            d);
           replace_expr(d, if_expr, a_rhs);
 
           const typet &pt=ct.parameters()[0].type();