MMIO rewriting must maintain type consistency

MMIO read functions may (have to) return values of varying types.
Expression replacement must maintain, via type casts, consistency with
whatever the type of the original expression was.

Author: tautschnig

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();