From 871d3a503a68c948964287fd646412448e339e17 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Feb 2022 16:35:50 +0000 Subject: [PATCH] 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. --- regression/cbmc/mm_io1/main.c | 1 + src/goto-programs/mm_io.cpp | 5 ++++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/regression/cbmc/mm_io1/main.c b/regression/cbmc/mm_io1/main.c index 2f1638f63c3..186d01678dd 100644 --- a/regression/cbmc/mm_io1/main.c +++ b/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; diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index cf18e2f9f2b..d26b9b0afb2 100644 --- a/src/goto-programs/mm_io.cpp +++ b/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();