From a939baf4b745f4b0689f80da15d2e7a36ab02859 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 30 May 2023 10:38:26 +0000
Subject: [PATCH] Field sensitivity: also rewrite byte extract to type casts

With /~https://github.com/model-checking/kani/pull/2456 we see examples
where a pointer of a different type is byte-extracted from a union. This
is caused by Rust's niche placement. `get_subexpression_at_offset`
already catered for that, but we didn't use it in field expansion.
---
 src/goto-symex/field_sensitivity.cpp | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
index a430fe4c5962..a0cb3e1658d2 100644
--- a/src/goto-symex/field_sensitivity.cpp
+++ b/src/goto-symex/field_sensitivity.cpp
@@ -123,6 +123,20 @@ exprt field_sensitivityt::apply(
           else
             return apply(ns, state, std::move(tmp), write);
         }
+        else if(
+          recursive_member.has_value() && recursive_member->id() == ID_typecast)
+        {
+          if(was_l2)
+          {
+            return apply(
+              ns,
+              state,
+              state.rename(std::move(*recursive_member), ns).get(),
+              write);
+          }
+          else
+            return apply(ns, state, std::move(*recursive_member), write);
+        }
       }
     }
   }