Pointer dereferencing cleanup: Make try_add_offset_to_indices file-local

This function does not require access to any state, and is really not
generally usable or useful. Also, make explicit why it would not work
for type casts.

Author: tautschnig

src/pointer-analysis/value_set_dereference.cpp

@@ -99,9 +99,11 @@ static json_objectt value_set_dereference_stats_to_json(
   return json_result;
 }
 
-optionalt<exprt> value_set_dereferencet::try_add_offset_to_indices(
-  const exprt &expr,
-  const exprt &offset_elements)
+/// If `expr` is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...)
+/// then return `c1 ? e1[o1 + offset] : e2[o2 + offset] : c3 ? ...`
+/// otherwise return an empty optionalt.
+static optionalt<exprt>
+try_add_offset_to_indices(const exprt &expr, const exprt &offset_elements)
 {
   if(const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr))
   {
@@ -123,6 +125,13 @@ optionalt<exprt> value_set_dereferencet::try_add_offset_to_indices(
       return {};
     return if_exprt{if_expr->cond(), *true_case, *false_case};
   }
+  else if(can_cast_expr<typecast_exprt>(expr))
+  {
+    // the case of a type cast is _not_ handled here, because that would require
+    // doing arithmetic on the offset, and may result in an offset into some
+    // sub-element
+    return {};
+  }
   else
   {
     return {};

src/pointer-analysis/value_set_dereference.h

@@ -54,12 +54,6 @@ class value_set_dereferencet final
   /// \param display_points_to_sets: Display size and contents of points to sets
   exprt dereference(const exprt &pointer, bool display_points_to_sets = false);
 
-  /// If `expr` is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...)
-  /// then return `c1 ? e1[o1 + offset] : e2[o2 + offset] : c3 ? ...`
-  /// otherwise return an empty optionalt.
-  optionalt<exprt>
-  try_add_offset_to_indices(const exprt &expr, const exprt &offset);
-
   /// Return value for `build_reference_to`; see that method for documentation.
   class valuet
   {