Merge pull request #7685 from tautschnig/cleanup/remove-make_map_start_address

Remove dfcc_utilst::make_map_start_address

Author: tautschnig

src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp

@@ -457,14 +457,6 @@ exprt dfcc_utilst::make_sizeof_expr(const exprt &expr)
   return size.value();
 }
 
-exprt dfcc_utilst::make_map_start_address(const exprt &expr)
-{
-  return typecast_exprt::conditional_cast(
-    address_of_exprt(index_exprt(
-      expr, from_integer(0, to_array_type(expr.type()).index_type()))),
-    pointer_type(bool_typet()));
-}
-
 void dfcc_utilst::inline_function(const irep_idt &function_id)
 {
   auto &goto_function = goto_model.goto_functions.function_map.at(function_id);

src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h

@@ -195,9 +195,6 @@ class dfcc_utilst
   /// \brief Returns the expression `sizeof(expr)`.
   exprt make_sizeof_expr(const exprt &expr);
 
-  /// \brief Returns the expression `&expr[0]`
-  exprt make_map_start_address(const exprt &expr);
-
   /// \brief Inlines the given function, aborts on recursive calls during
   /// inlining.
   void inline_function(const irep_idt &function_id);