Merge pull request #7739 from tautschnig/feature/fs-typecast

Field sensitivity: also rewrite byte extract to type casts

Author: tautschnig

regression/contracts/assigns_enforce_conditional_unions/program-only.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-contract update _ --program-only
+^EXIT=0$
+^SIGNAL=0$
+--
+^\(\d+\) guard#\d+ == .*byte_extract
+--
+Confirms that field sensitivity can resolve pointer byte extracts to type casts.

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);
+        }
       }
     }
   }