diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index 53ed886c9f1..9a7ca193ea8 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -38,7 +38,7 @@ SRC = accelerate/accelerate.cpp \
       dump_c.cpp \
       full_slicer.cpp \
       function.cpp \
-      function_modifies.cpp \
+      function_assigns.cpp \
       generate_function_bodies.cpp \
       goto_instrument_languages.cpp \
       goto_instrument_main.cpp \
diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h
index 883eee8c8e2..3059c9e882c 100644
--- a/src/goto-instrument/contracts/assigns.h
+++ b/src/goto-instrument/contracts/assigns.h
@@ -118,7 +118,7 @@ class assigns_clauset
 class havoc_assigns_targetst : public havoc_if_validt
 {
 public:
-  havoc_assigns_targetst(const modifiest &mod, const namespacet &ns)
+  havoc_assigns_targetst(const assignst &mod, const namespacet &ns)
     : havoc_if_validt(mod, ns)
   {
   }
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 54f766be01f..ad2f38f0624 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -150,7 +150,7 @@ void code_contractst::check_apply_loop_contracts(
       loop_end = t;
 
   // check for assigns, invariant, and decreases clauses
-  auto assigns = static_cast<const exprt &>(
+  auto assigns_clause = static_cast<const exprt &>(
     loop_end->get_condition().find(ID_C_spec_assigns));
   auto invariant = static_cast<const exprt &>(
     loop_end->get_condition().find(ID_C_spec_loop_invariant));
@@ -158,13 +158,13 @@ void code_contractst::check_apply_loop_contracts(
     loop_end->get_condition().find(ID_C_spec_decreases));
 
   assigns_clauset loop_assigns(
-    assigns.operands(), log, ns, function_name, symbol_table);
+    assigns_clause.operands(), log, ns, function_name, symbol_table);
 
   loop_assigns.add_static_locals_to_write_set(goto_functions, function_name);
 
   if(invariant.is_nil())
   {
-    if(decreases_clause.is_nil() && assigns.is_nil())
+    if(decreases_clause.is_nil() && assigns_clause.is_nil())
       return;
     else
     {
@@ -253,12 +253,12 @@ void code_contractst::check_apply_loop_contracts(
     add_pragma_disable_assigns_check(generated_code));
 
   // havoc the variables that may be modified
-  modifiest modifies;
-  if(assigns.is_nil())
+  assignst assigns;
+  if(assigns_clause.is_nil())
   {
     try
     {
-      get_modifies(local_may_alias, loop, modifies);
+      get_assigns(local_may_alias, loop, assigns);
     }
     catch(const analysis_exceptiont &exc)
     {
@@ -271,7 +271,8 @@ void code_contractst::check_apply_loop_contracts(
   }
   else
   {
-    modifies.insert(assigns.operands().cbegin(), assigns.operands().cend());
+    assigns.insert(
+      assigns_clause.operands().cbegin(), assigns_clause.operands().cend());
 
     // Create snapshots of write set CARs.
     // This must be done before havocing the write set.
@@ -287,13 +288,13 @@ void code_contractst::check_apply_loop_contracts(
       function_name, goto_function.body, loop_head, loop_end, loop_assigns);
   }
 
-  havoc_assigns_targetst havoc_gen(modifies, ns);
+  havoc_assigns_targetst havoc_gen(assigns, ns);
   havoc_gen.append_full_havoc_code(
     loop_head->source_location(), generated_code);
 
   // Add the havocing code, but only check against the enclosing scope's
   // write set if it was manually specified.
-  if(assigns.is_nil())
+  if(assigns_clause.is_nil())
     insert_before_swap_and_advance(
       goto_function.body,
       loop_head,
@@ -624,7 +625,7 @@ bool code_contractst::apply_function_contract(
   const auto &type = to_code_with_contract_type(function_symbol.type);
 
   // Isolate each component of the contract.
-  auto assigns = type.assigns();
+  auto assigns_clause = type.assigns();
   auto requires = conjunction(type.requires());
   auto ensures = conjunction(type.ensures());
 
@@ -740,7 +741,7 @@ bool code_contractst::apply_function_contract(
   // ASSIGNS clause should not refer to any quantified variables,
   // and only refer to the common symbols to be replaced.
   exprt targets;
-  for(auto &target : assigns)
+  for(auto &target : assigns_clause)
     targets.add_to_operands(std::move(target));
   common_replace(targets);
 
@@ -748,16 +749,16 @@ bool code_contractst::apply_function_contract(
   goto_programt havoc_instructions;
 
   // ...for assigns clause targets
-  if(!assigns.empty())
+  if(!assigns_clause.empty())
   {
     assigns_clauset assigns_clause(
       targets.operands(), log, ns, target_function, symbol_table);
 
     // Havoc all targets in the write set
-    modifiest modifies;
-    modifies.insert(targets.operands().cbegin(), targets.operands().cend());
+    assignst assigns;
+    assigns.insert(targets.operands().cbegin(), targets.operands().cend());
 
-    havoc_assigns_targetst havoc_gen(modifies, ns);
+    havoc_assigns_targetst havoc_gen(assigns, ns);
     havoc_gen.append_full_havoc_code(location, havoc_instructions);
   }
 
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
index 589ab0981b2..1614ce023a3 100644
--- a/src/goto-instrument/contracts/utils.h
+++ b/src/goto-instrument/contracts/utils.h
@@ -25,7 +25,7 @@ Date: September 2021
 class havoc_if_validt : public havoc_utilst
 {
 public:
-  havoc_if_validt(const modifiest &mod, const namespacet &ns)
+  havoc_if_validt(const assignst &mod, const namespacet &ns)
     : havoc_utilst(mod), ns(ns)
   {
   }
diff --git a/src/goto-instrument/function_assigns.cpp b/src/goto-instrument/function_assigns.cpp
new file mode 100644
index 00000000000..06d2e8879d9
--- /dev/null
+++ b/src/goto-instrument/function_assigns.cpp
@@ -0,0 +1,78 @@
+/*******************************************************************\
+
+Module: Compute objects assigned to in a function
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Compute objects assigned to in a function.
+
+#include "function_assigns.h"
+
+#include <util/std_expr.h>
+
+#include <analyses/local_may_alias.h>
+
+#include "loop_utils.h"
+
+void function_assignst::get_assigns(
+  const local_may_aliast &local_may_alias,
+  const goto_programt::const_targett i_it,
+  assignst &assigns)
+{
+  const goto_programt::instructiont &instruction = *i_it;
+
+  if(instruction.is_assign())
+  {
+    get_assigns_lhs(local_may_alias, i_it, instruction.assign_lhs(), assigns);
+  }
+  else if(instruction.is_function_call())
+  {
+    const exprt &lhs = instruction.call_lhs();
+
+    // return value assignment
+    if(lhs.is_not_nil())
+      get_assigns_lhs(local_may_alias, i_it, lhs, assigns);
+
+    get_assigns_function(instruction.call_function(), assigns);
+  }
+}
+
+void function_assignst::get_assigns_function(
+  const exprt &function,
+  assignst &assigns)
+{
+  if(function.id() == ID_symbol)
+  {
+    const irep_idt &identifier = to_symbol_expr(function).get_identifier();
+
+    function_mapt::const_iterator fm_it = function_map.find(identifier);
+
+    if(fm_it != function_map.end())
+    {
+      // already done
+      assigns.insert(fm_it->second.begin(), fm_it->second.end());
+      return;
+    }
+
+    goto_functionst::function_mapt::const_iterator f_it =
+      goto_functions.function_map.find(identifier);
+
+    if(f_it == goto_functions.function_map.end())
+      return;
+
+    local_may_aliast local_may_alias(f_it->second);
+
+    const goto_programt &goto_program = f_it->second.body;
+
+    forall_goto_program_instructions(i_it, goto_program)
+      get_assigns(local_may_alias, i_it, assigns);
+  }
+  else if(function.id() == ID_if)
+  {
+    get_assigns_function(to_if_expr(function).true_case(), assigns);
+    get_assigns_function(to_if_expr(function).false_case(), assigns);
+  }
+}
diff --git a/src/goto-instrument/function_assigns.h b/src/goto-instrument/function_assigns.h
new file mode 100644
index 00000000000..0e4357712cd
--- /dev/null
+++ b/src/goto-instrument/function_assigns.h
@@ -0,0 +1,51 @@
+/*******************************************************************\
+
+Module: Compute objects assigned to in a function
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Compute objects assigned to in a function.
+
+#ifndef CPROVER_GOTO_INSTRUMENT_FUNCTION_ASSIGNS_H
+#define CPROVER_GOTO_INSTRUMENT_FUNCTION_ASSIGNS_H
+
+#include <goto-programs/goto_program.h>
+
+#include <map>
+
+class goto_functionst;
+class local_may_aliast;
+
+class function_assignst
+{
+public:
+  explicit function_assignst(const goto_functionst &_goto_functions)
+    : goto_functions(_goto_functions)
+  {
+  }
+
+  typedef std::set<exprt> assignst;
+
+  void get_assigns(
+    const local_may_aliast &local_may_alias,
+    const goto_programt::const_targett,
+    assignst &);
+
+  void get_assigns_function(const exprt &, assignst &);
+
+  void operator()(const exprt &function, assignst &assigns)
+  {
+    get_assigns_function(function, assigns);
+  }
+
+protected:
+  const goto_functionst &goto_functions;
+
+  typedef std::map<irep_idt, assignst> function_mapt;
+  function_mapt function_map;
+};
+
+#endif // CPROVER_GOTO_INSTRUMENT_FUNCTION_ASSIGNS_H
diff --git a/src/goto-instrument/function_modifies.cpp b/src/goto-instrument/function_modifies.cpp
deleted file mode 100644
index 6c27d83721b..00000000000
--- a/src/goto-instrument/function_modifies.cpp
+++ /dev/null
@@ -1,79 +0,0 @@
-/*******************************************************************\
-
-Module: Modifies
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-/// \file
-/// Modifies
-
-#include "function_modifies.h"
-
-#include <util/std_expr.h>
-
-#include <analyses/local_may_alias.h>
-
-#include "loop_utils.h"
-
-void function_modifiest::get_modifies(
-  const local_may_aliast &local_may_alias,
-  const goto_programt::const_targett i_it,
-  modifiest &modifies)
-{
-  const goto_programt::instructiont &instruction=*i_it;
-
-  if(instruction.is_assign())
-  {
-    get_modifies_lhs(local_may_alias, i_it, instruction.assign_lhs(), modifies);
-  }
-  else if(instruction.is_function_call())
-  {
-    const exprt &lhs = instruction.call_lhs();
-
-    // return value assignment
-    if(lhs.is_not_nil())
-      get_modifies_lhs(local_may_alias, i_it, lhs, modifies);
-
-    get_modifies_function(instruction.call_function(), modifies);
-  }
-}
-
-void function_modifiest::get_modifies_function(
-  const exprt &function,
-  modifiest &modifies)
-{
-  if(function.id()==ID_symbol)
-  {
-    const irep_idt &identifier=to_symbol_expr(function).get_identifier();
-
-    function_mapt::const_iterator fm_it=
-      function_map.find(identifier);
-
-    if(fm_it!=function_map.end())
-    {
-      // already done
-      modifies.insert(fm_it->second.begin(), fm_it->second.end());
-      return;
-    }
-
-    goto_functionst::function_mapt::const_iterator
-      f_it=goto_functions.function_map.find(identifier);
-
-    if(f_it==goto_functions.function_map.end())
-      return;
-
-    local_may_aliast local_may_alias(f_it->second);
-
-    const goto_programt &goto_program=f_it->second.body;
-
-    forall_goto_program_instructions(i_it, goto_program)
-      get_modifies(local_may_alias, i_it, modifies);
-  }
-  else if(function.id()==ID_if)
-  {
-    get_modifies_function(to_if_expr(function).true_case(), modifies);
-    get_modifies_function(to_if_expr(function).false_case(), modifies);
-  }
-}
diff --git a/src/goto-instrument/function_modifies.h b/src/goto-instrument/function_modifies.h
deleted file mode 100644
index fa235955069..00000000000
--- a/src/goto-instrument/function_modifies.h
+++ /dev/null
@@ -1,53 +0,0 @@
-/*******************************************************************\
-
-Module: Modifies
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-/// \file
-/// Modifies
-
-#ifndef CPROVER_GOTO_INSTRUMENT_FUNCTION_MODIFIES_H
-#define CPROVER_GOTO_INSTRUMENT_FUNCTION_MODIFIES_H
-
-#include <goto-programs/goto_program.h>
-
-#include <map>
-
-class goto_functionst;
-class local_may_aliast;
-
-class function_modifiest
-{
-public:
-  explicit function_modifiest(const goto_functionst &_goto_functions):
-    goto_functions(_goto_functions)
-  {
-  }
-
-  typedef std::set<exprt> modifiest;
-
-  void get_modifies(
-    const local_may_aliast &local_may_alias,
-    const goto_programt::const_targett,
-    modifiest &);
-
-  void get_modifies_function(
-    const exprt &,
-    modifiest &);
-
-  void operator()(const exprt &function, modifiest &modifies)
-  {
-    get_modifies_function(function, modifies);
-  }
-
-protected:
-  const goto_functionst &goto_functions;
-
-  typedef std::map<irep_idt, modifiest> function_mapt;
-  function_mapt function_map;
-};
-
-#endif // CPROVER_GOTO_INSTRUMENT_FUNCTION_MODIFIES_H
diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-instrument/havoc_loops.cpp
index 3a368dfe016..92e73cb68ac 100644
--- a/src/goto-instrument/havoc_loops.cpp
+++ b/src/goto-instrument/havoc_loops.cpp
@@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/remove_skip.h>
 
-#include "function_modifies.h"
+#include "function_assigns.h"
 #include "havoc_utils.h"
 #include "loop_utils.h"
 
@@ -26,12 +26,12 @@ class havoc_loopst
   typedef goto_functionst::goto_functiont goto_functiont;
 
   havoc_loopst(
-    function_modifiest &_function_modifies,
-    goto_functiont &_goto_function):
-    goto_function(_goto_function),
-    local_may_alias(_goto_function),
-    function_modifies(_function_modifies),
-    natural_loops(_goto_function.body)
+    function_assignst &_function_assigns,
+    goto_functiont &_goto_function)
+    : goto_function(_goto_function),
+      local_may_alias(_goto_function),
+      function_assigns(_function_assigns),
+      natural_loops(_goto_function.body)
   {
     havoc_loops();
   }
@@ -39,10 +39,10 @@ class havoc_loopst
 protected:
   goto_functiont &goto_function;
   local_may_aliast local_may_alias;
-  function_modifiest &function_modifies;
+  function_assignst &function_assigns;
   natural_loops_mutablet natural_loops;
 
-  typedef std::set<exprt> modifiest;
+  typedef std::set<exprt> assignst;
   typedef const natural_loops_mutablet::natural_loopt loopt;
 
   void havoc_loops();
@@ -51,9 +51,7 @@ class havoc_loopst
     const goto_programt::targett loop_head,
     const loopt &);
 
-  void get_modifies(
-    const loopt &,
-    modifiest &);
+  void get_assigns(const loopt &, assignst &);
 };
 
 void havoc_loopst::havoc_loop(
@@ -63,12 +61,12 @@ void havoc_loopst::havoc_loop(
   assert(!loop.empty());
 
   // first find out what can get changed in the loop
-  modifiest modifies;
-  get_modifies(loop, modifies);
+  assignst assigns;
+  get_assigns(loop, assigns);
 
   // build the havocking code
   goto_programt havoc_code;
-  havoc_utilst havoc_gen(modifies);
+  havoc_utilst havoc_gen(assigns);
   havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code);
 
   // Now havoc at the loop head. Use insert_swap to
@@ -101,12 +99,10 @@ void havoc_loopst::havoc_loop(
   remove_skip(goto_function.body);
 }
 
-void havoc_loopst::get_modifies(
-  const loopt &loop,
-  modifiest &modifies)
+void havoc_loopst::get_assigns(const loopt &loop, assignst &assigns)
 {
   for(const auto &instruction_it : loop)
-    function_modifies.get_modifies(local_may_alias, instruction_it, modifies);
+    function_assigns.get_assigns(local_may_alias, instruction_it, assigns);
 }
 
 void havoc_loopst::havoc_loops()
@@ -119,8 +115,8 @@ void havoc_loopst::havoc_loops()
 
 void havoc_loops(goto_modelt &goto_model)
 {
-  function_modifiest function_modifies(goto_model.goto_functions);
+  function_assignst function_assigns(goto_model.goto_functions);
 
   for(auto &gf_entry : goto_model.goto_functions.function_map)
-    havoc_loopst(function_modifies, gf_entry.second);
+    havoc_loopst(function_assigns, gf_entry.second);
 }
diff --git a/src/goto-instrument/havoc_utils.cpp b/src/goto-instrument/havoc_utils.cpp
index 4e3f17daecf..385d4942174 100644
--- a/src/goto-instrument/havoc_utils.cpp
+++ b/src/goto-instrument/havoc_utils.cpp
@@ -22,7 +22,7 @@ void havoc_utilst::append_full_havoc_code(
   const source_locationt location,
   goto_programt &dest) const
 {
-  for(const auto &expr : modifies)
+  for(const auto &expr : assigns)
     append_havoc_code_for_expr(location, expr, dest);
 }
 
diff --git a/src/goto-instrument/havoc_utils.h b/src/goto-instrument/havoc_utils.h
index 0cdbdc699c9..eb9710a4794 100644
--- a/src/goto-instrument/havoc_utils.h
+++ b/src/goto-instrument/havoc_utils.h
@@ -20,13 +20,13 @@ Date: July 2021
 
 #include <util/expr_util.h>
 
-typedef std::set<exprt> modifiest;
+typedef std::set<exprt> assignst;
 
 /// \brief A class containing utility functions for havocing expressions.
 class havoc_utils_is_constantt : public is_constantt
 {
 public:
-  explicit havoc_utils_is_constantt(const modifiest &mod) : modifies(mod)
+  explicit havoc_utils_is_constantt(const assignst &mod) : assigns(mod)
   {
   }
 
@@ -34,27 +34,27 @@ class havoc_utils_is_constantt : public is_constantt
   {
     // Besides the "usual" constants (checked in is_constantt::is_constant),
     // we also treat unmodified symbols as constants
-    if(expr.id() == ID_symbol && modifies.find(expr) == modifies.end())
+    if(expr.id() == ID_symbol && assigns.find(expr) == assigns.end())
       return true;
 
     return is_constantt::is_constant(expr);
   }
 
 protected:
-  const modifiest &modifies;
+  const assignst &assigns;
 };
 
 class havoc_utilst
 {
 public:
-  explicit havoc_utilst(const modifiest &mod) : modifies(mod), is_constant(mod)
+  explicit havoc_utilst(const assignst &mod) : assigns(mod), is_constant(mod)
   {
   }
 
-  /// \brief Append goto instructions to havoc the full `modifies` set
+  /// \brief Append goto instructions to havoc the full `assigns` set
   ///
   /// This function invokes `append_havoc_code_for_expr` on each expression in
-  /// the `modifies` set.
+  /// the `assigns` set.
   ///
   /// \param location The source location to annotate on the havoc instruction
   /// \param dest The destination goto program to append the instructions to
@@ -99,7 +99,7 @@ class havoc_utilst
     goto_programt &dest) const;
 
 protected:
-  const modifiest &modifies;
+  const assignst &assigns;
   const havoc_utils_is_constantt is_constant;
 };
 
diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp
index db11ec8425f..5ed91b4317e 100644
--- a/src/goto-instrument/k_induction.cpp
+++ b/src/goto-instrument/k_induction.cpp
@@ -92,12 +92,12 @@ void k_inductiont::process_loop(
     // step case
 
     // find out what can get changed in the loop
-    modifiest modifies;
-    get_modifies(local_may_alias, loop, modifies);
+    assignst assigns;
+    get_assigns(local_may_alias, loop, assigns);
 
     // build the havocking code
     goto_programt havoc_code;
-    havoc_utilst havoc_gen(modifies);
+    havoc_utilst havoc_gen(assigns);
     havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code);
 
     // unwind to get k+1 copies
diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp
index a488c4ae738..a3f8144157d 100644
--- a/src/goto-instrument/loop_utils.cpp
+++ b/src/goto-instrument/loop_utils.cpp
@@ -36,15 +36,14 @@ goto_programt::targett get_loop_exit(const loopt &loop)
   return ++last;
 }
 
-
-void get_modifies_lhs(
+void get_assigns_lhs(
   const local_may_aliast &local_may_alias,
   goto_programt::const_targett t,
   const exprt &lhs,
-  modifiest &modifies)
+  assignst &assigns)
 {
   if(lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index)
-    modifies.insert(lhs);
+    assigns.insert(lhs);
   else if(lhs.id()==ID_dereference)
   {
     const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
@@ -56,24 +55,24 @@ void get_modifies_lhs(
         throw analysis_exceptiont("Alias analysis returned UNKNOWN!");
       }
       if(ptr.offset.is_nil())
-        modifies.insert(dereference_exprt{typed_mod});
+        assigns.insert(dereference_exprt{typed_mod});
       else
-        modifies.insert(dereference_exprt{plus_exprt{typed_mod, ptr.offset}});
+        assigns.insert(dereference_exprt{plus_exprt{typed_mod, ptr.offset}});
     }
   }
   else if(lhs.id()==ID_if)
   {
     const if_exprt &if_expr=to_if_expr(lhs);
 
-    get_modifies_lhs(local_may_alias, t, if_expr.true_case(), modifies);
-    get_modifies_lhs(local_may_alias, t, if_expr.false_case(), modifies);
+    get_assigns_lhs(local_may_alias, t, if_expr.true_case(), assigns);
+    get_assigns_lhs(local_may_alias, t, if_expr.false_case(), assigns);
   }
 }
 
-void get_modifies(
+void get_assigns(
   const local_may_aliast &local_may_alias,
   const loopt &loop,
-  modifiest &modifies)
+  assignst &assigns)
 {
   for(loopt::const_iterator
       i_it=loop.begin(); i_it!=loop.end(); i_it++)
@@ -83,12 +82,12 @@ void get_modifies(
     if(instruction.is_assign())
     {
       const exprt &lhs = instruction.assign_lhs();
-      get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
+      get_assigns_lhs(local_may_alias, *i_it, lhs, assigns);
     }
     else if(instruction.is_function_call())
     {
       const exprt &lhs = instruction.call_lhs();
-      get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
+      get_assigns_lhs(local_may_alias, *i_it, lhs, assigns);
     }
   }
 }
diff --git a/src/goto-instrument/loop_utils.h b/src/goto-instrument/loop_utils.h
index 3263192d8cc..dd5c0f9b9dc 100644
--- a/src/goto-instrument/loop_utils.h
+++ b/src/goto-instrument/loop_utils.h
@@ -16,19 +16,19 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class local_may_aliast;
 
-typedef std::set<exprt> modifiest;
+typedef std::set<exprt> assignst;
 typedef natural_loops_mutablet::natural_loopt loopt;
 
-void get_modifies(
+void get_assigns(
   const local_may_aliast &local_may_alias,
   const loopt &loop,
-  modifiest &modifies);
+  assignst &assigns);
 
-void get_modifies_lhs(
+void get_assigns_lhs(
   const local_may_aliast &local_may_alias,
   goto_programt::const_targett t,
   const exprt &lhs,
-  modifiest &modifies);
+  assignst &assigns);
 
 goto_programt::targett get_loop_exit(const loopt &);