diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index da40ae0cae3..d0cfeeedffe 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -231,6 +231,7 @@ ai_baset::locationt ai_baset::get_next(
 }
 
 bool ai_baset::fixedpoint(
+  const irep_idt &function_identifier,
   const goto_programt &goto_program,
   const goto_functionst &goto_functions,
   const namespacet &ns)
@@ -250,7 +251,8 @@ bool ai_baset::fixedpoint(
     locationt l=get_next(working_set);
 
     // goto_program is really only needed for iterator manipulation
-    if(visit(l, working_set, goto_program, goto_functions, ns))
+    if(visit(
+         function_identifier, l, working_set, goto_program, goto_functions, ns))
       new_data=true;
   }
 
@@ -258,6 +260,7 @@ bool ai_baset::fixedpoint(
 }
 
 bool ai_baset::visit(
+  const irep_idt &function_identifier,
   locationt l,
   working_sett &working_set,
   const goto_programt &goto_program,
@@ -288,10 +291,13 @@ bool ai_baset::visit(
         to_code_function_call(l->code);
 
       if(do_function_call_rec(
-          l, to_l,
-          code.function(),
-          code.arguments(),
-          goto_functions, ns))
+           function_identifier,
+           l,
+           to_l,
+           code.function(),
+           code.arguments(),
+           goto_functions,
+           ns))
         have_new_values=true;
     }
     else
@@ -299,7 +305,8 @@ bool ai_baset::visit(
       // initialize state, if necessary
       get_state(to_l);
 
-      new_values.transform(l, to_l, *this, ns);
+      new_values.transform(
+        function_identifier, l, function_identifier, to_l, *this, ns);
 
       if(merge(new_values, l, to_l))
         have_new_values=true;
@@ -316,7 +323,9 @@ bool ai_baset::visit(
 }
 
 bool ai_baset::do_function_call(
-  locationt l_call, locationt l_return,
+  const irep_idt &calling_function_identifier,
+  locationt l_call,
+  locationt l_return,
   const goto_functionst &goto_functions,
   const goto_functionst::function_mapt::const_iterator f_it,
   const exprt::operandst &,
@@ -334,7 +343,13 @@ bool ai_baset::do_function_call(
   {
     // if we don't have a body, we just do an edige call -> return
     std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
-    tmp_state->transform(l_call, l_return, *this, ns);
+    tmp_state->transform(
+      calling_function_identifier,
+      l_call,
+      calling_function_identifier,
+      l_return,
+      *this,
+      ns);
 
     return merge(*tmp_state, l_call, l_return);
   }
@@ -351,7 +366,8 @@ bool ai_baset::do_function_call(
 
     // do the edge from the call site to the beginning of the function
     std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
-    tmp_state->transform(l_call, l_begin, *this, ns);
+    tmp_state->transform(
+      calling_function_identifier, l_call, f_it->first, l_begin, *this, ns);
 
     bool new_data=false;
 
@@ -361,7 +377,7 @@ bool ai_baset::do_function_call(
 
     // do we need to do/re-do the fixedpoint of the body?
     if(new_data)
-      fixedpoint(goto_function.body, goto_functions, ns);
+      fixedpoint(f_it->first, goto_function.body, goto_functions, ns);
   }
 
   // This is the edge from function end to return site.
@@ -378,7 +394,8 @@ bool ai_baset::do_function_call(
       return false; // function exit point not reachable
 
     std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
-    tmp_state->transform(l_end, l_return, *this, ns);
+    tmp_state->transform(
+      f_it->first, l_end, calling_function_identifier, l_return, *this, ns);
 
     // Propagate those
     return merge(*tmp_state, l_end, l_return);
@@ -386,7 +403,9 @@ bool ai_baset::do_function_call(
 }
 
 bool ai_baset::do_function_call_rec(
-  locationt l_call, locationt l_return,
+  const irep_idt &calling_function_identifier,
+  locationt l_call,
+  locationt l_return,
   const exprt &function,
   const exprt::operandst &arguments,
   const goto_functionst &goto_functions,
@@ -411,8 +430,14 @@ bool ai_baset::do_function_call_rec(
     it != goto_functions.function_map.end(),
     "Function " + id2string(identifier) + "not in function map");
 
-  new_data =
-    do_function_call(l_call, l_return, goto_functions, it, arguments, ns);
+  new_data = do_function_call(
+    calling_function_identifier,
+    l_call,
+    l_return,
+    goto_functions,
+    it,
+    arguments,
+    ns);
 
   return new_data;
 }
@@ -425,7 +450,7 @@ void ai_baset::sequential_fixedpoint(
     f_it=goto_functions.function_map.find(goto_functions.entry_point());
 
   if(f_it!=goto_functions.function_map.end())
-    fixedpoint(f_it->second.body, goto_functions, ns);
+    fixedpoint(f_it->first, f_it->second.body, goto_functions, ns);
 }
 
 void ai_baset::concurrent_fixedpoint(
@@ -443,8 +468,24 @@ void ai_baset::concurrent_fixedpoint(
   goto_programt::const_targett sh_target=tmp.instructions.begin();
   statet &shared_state=get_state(sh_target);
 
-  typedef std::list<std::pair<goto_programt const*,
-                              goto_programt::const_targett> > thread_wlt;
+  struct wl_entryt
+  {
+    wl_entryt(
+      const irep_idt &_function_identifier,
+      const goto_programt &_goto_program,
+      locationt _location)
+      : function_identifier(_function_identifier),
+        goto_program(&_goto_program),
+        location(_location)
+    {
+    }
+
+    irep_idt function_identifier;
+    const goto_programt *goto_program;
+    locationt location;
+  };
+
+  typedef std::list<wl_entryt> thread_wlt;
   thread_wlt thread_wl;
 
   forall_goto_functions(it, goto_functions)
@@ -452,7 +493,7 @@ void ai_baset::concurrent_fixedpoint(
     {
       if(is_threaded(t_it))
       {
-        thread_wl.push_back(std::make_pair(&(it->second.body), t_it));
+        thread_wl.push_back(wl_entryt(it->first, it->second.body, t_it));
 
         goto_programt::const_targett l_end=
           it->second.body.instructions.end();
@@ -469,19 +510,25 @@ void ai_baset::concurrent_fixedpoint(
   {
     new_shared=false;
 
-    for(const auto &wl_pair : thread_wl)
+    for(const auto &wl_entry : thread_wl)
     {
       working_sett working_set;
-      put_in_working_set(working_set, wl_pair.second);
+      put_in_working_set(working_set, wl_entry.location);
 
-      statet &begin_state=get_state(wl_pair.second);
-      merge(begin_state, sh_target, wl_pair.second);
+      statet &begin_state = get_state(wl_entry.location);
+      merge(begin_state, sh_target, wl_entry.location);
 
       while(!working_set.empty())
       {
         goto_programt::const_targett l=get_next(working_set);
 
-        visit(l, working_set, *(wl_pair.first), goto_functions, ns);
+        visit(
+          wl_entry.function_identifier,
+          l,
+          working_set,
+          *(wl_entry.goto_program),
+          goto_functions,
+          ns);
 
         // the underlying domain must make sure that the final state
         // carries all possible values; otherwise we would need to
diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index e575df23146..b1396935134 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -45,13 +45,14 @@ class ai_baset
 
   /// Running the interpreter
   void operator()(
+    const irep_idt &function_identifier,
     const goto_programt &goto_program,
     const namespacet &ns)
   {
     goto_functionst goto_functions;
     initialize(goto_program);
     entry_state(goto_program);
-    fixedpoint(goto_program, goto_functions, ns);
+    fixedpoint(function_identifier, goto_program, goto_functions, ns);
     finalize();
   }
 
@@ -75,13 +76,14 @@ class ai_baset
   }
 
   void operator()(
+    const irep_idt &function_identifier,
     const goto_functionst::goto_functiont &goto_function,
     const namespacet &ns)
   {
     goto_functionst goto_functions;
     initialize(goto_function);
     entry_state(goto_function.body);
-    fixedpoint(goto_function.body, goto_functions, ns);
+    fixedpoint(function_identifier, goto_function.body, goto_functions, ns);
     finalize();
   }
 
@@ -234,6 +236,7 @@ class ai_baset
 
   // true = found something new
   bool fixedpoint(
+    const irep_idt &function_identifier,
     const goto_programt &goto_program,
     const goto_functionst &goto_functions,
     const namespacet &ns);
@@ -245,6 +248,7 @@ class ai_baset
   void sequential_fixedpoint(
     const goto_functionst &goto_functions,
     const namespacet &ns);
+
   void concurrent_fixedpoint(
     const goto_functionst &goto_functions,
     const namespacet &ns);
@@ -254,6 +258,7 @@ class ai_baset
   // or applications of the abstract transformer
   // true = found something new
   bool visit(
+    const irep_idt &function_identifier,
     locationt l,
     working_sett &working_set,
     const goto_programt &goto_program,
@@ -262,14 +267,18 @@ class ai_baset
 
   // function calls
   bool do_function_call_rec(
-    locationt l_call, locationt l_return,
+    const irep_idt &calling_function_identifier,
+    locationt l_call,
+    locationt l_return,
     const exprt &function,
     const exprt::operandst &arguments,
     const goto_functionst &goto_functions,
     const namespacet &ns);
 
   bool do_function_call(
-    locationt l_call, locationt l_return,
+    const irep_idt &calling_function_identifier,
+    locationt l_call,
+    locationt l_return,
     const goto_functionst &goto_functions,
     const goto_functionst::function_mapt::const_iterator f_it,
     const exprt::operandst &arguments,
@@ -384,11 +393,8 @@ class ait:public ai_baset
   void dummy(const domainT &s) { const statet &x=s; (void)x; }
 
   // not implemented in sequential analyses
-  bool merge_shared(
-    const statet &,
-    goto_programt::const_targett,
-    goto_programt::const_targett,
-    const namespacet &) override
+  bool merge_shared(const statet &, locationt, locationt, const namespacet &)
+    override
   {
     throw "not implemented";
   }
@@ -398,7 +404,8 @@ template<typename domainT>
 class concurrency_aware_ait:public ait<domainT>
 {
 public:
-  typedef typename ait<domainT>::statet statet;
+  using statet = typename ait<domainT>::statet;
+  using locationt = typename statet::locationt;
 
   // constructor
   concurrency_aware_ait():ait<domainT>()
@@ -407,8 +414,8 @@ class concurrency_aware_ait:public ait<domainT>
 
   bool merge_shared(
     const statet &src,
-    goto_programt::const_targett from,
-    goto_programt::const_targett to,
+    locationt from,
+    locationt to,
     const namespacet &ns) override
   {
     statet &dest=this->get_state(to);
diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h
index 2dc1b6e33ec..700103faee8 100644
--- a/src/analyses/ai_domain.h
+++ b/src/analyses/ai_domain.h
@@ -55,7 +55,9 @@ class ai_domain_baset
   ///              (from->is_function_call() || from->is_end_function())
 
   virtual void transform(
+    const irep_idt &function_from,
     locationt from,
+    const irep_idt &function_to,
     locationt to,
     ai_baset &ai,
     const namespacet &ns) = 0;
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 9a849be93eb..0779eeda196 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -58,7 +58,9 @@ void constant_propagator_domaint::assign_rec(
 }
 
 void constant_propagator_domaint::transform(
+  const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt to,
   ai_baset &ai,
   const namespacet &ns)
@@ -146,7 +148,7 @@ void constant_propagator_domaint::transform(
       const irep_idt id=symbol_expr.get_identifier();
 
       // Functions with no body
-      if(from->function == to->function)
+      if(function_from == function_to)
       {
         if(id==CPROVER_PREFIX "set_must" ||
            id==CPROVER_PREFIX "get_must" ||
@@ -195,7 +197,7 @@ void constant_propagator_domaint::transform(
     {
       // unresolved call
       INVARIANT(
-        from->function == to->function,
+        function_from == function_to,
         "Unresolved call can only be approximated if a skip");
 
       if(have_dirty)
@@ -208,7 +210,7 @@ void constant_propagator_domaint::transform(
   {
     // erase parameters
 
-    const irep_idt id=from->function;
+    const irep_idt id = function_from;
     const symbolt &symbol=ns.lookup(id);
 
     const code_typet &type=to_code_type(symbol.type);
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 62c3cb919f9..6edef4a513b 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -34,7 +34,9 @@ class constant_propagator_domaint:public ai_domain_baset
 {
 public:
   virtual void transform(
+    const irep_idt &function_from,
     locationt from,
+    const irep_idt &function_to,
     locationt to,
     ai_baset &ai_base,
     const namespacet &ns) final override;
@@ -196,13 +198,13 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
   }
 
   constant_propagator_ait(
+    const irep_idt &function_identifier,
     goto_functionst::goto_functiont &goto_function,
     const namespacet &ns,
-    should_track_valuet should_track_value = track_all_values):
-    dirty(goto_function),
-    should_track_value(should_track_value)
+    should_track_valuet should_track_value = track_all_values)
+    : dirty(goto_function), should_track_value(should_track_value)
   {
-    operator()(goto_function, ns);
+    operator()(function_identifier, goto_function, ns);
     replace(goto_function, ns);
   }
 
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index 9cf4ace1324..791143386d8 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -268,7 +268,9 @@ void custom_bitvector_domaint::assign_struct_rec(
 }
 
 void custom_bitvector_domaint::transform(
+  const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt to,
   ai_baset &ai,
   const namespacet &ns)
@@ -400,7 +402,7 @@ void custom_bitvector_domaint::transform(
         else
         {
           // only if there is an actual call, i.e., we have a body
-          if(from->function != to->function)
+          if(function_from != function_to)
           {
             const code_typet &code_type=
               to_code_type(ns.lookup(identifier).type);
diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h
index 4142d6930c1..511c3093833 100644
--- a/src/analyses/custom_bitvector_analysis.h
+++ b/src/analyses/custom_bitvector_analysis.h
@@ -23,9 +23,13 @@ class custom_bitvector_analysist;
 class custom_bitvector_domaint:public ai_domain_baset
 {
 public:
-  void
-  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
-    final override;
+  void transform(
+    const irep_idt &function_from,
+    locationt from,
+    const irep_idt &function_to,
+    locationt to,
+    ai_baset &ai,
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index 95e035ffe3c..71125df8273 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -191,7 +191,9 @@ void dep_graph_domaint::data_dependencies(
 }
 
 void dep_graph_domaint::transform(
+  const irep_idt &function_from,
   goto_programt::const_targett from,
+  const irep_idt &function_to,
   goto_programt::const_targett to,
   ai_baset &ai,
   const namespacet &ns)
@@ -202,7 +204,7 @@ void dep_graph_domaint::transform(
   // propagate control dependencies across function calls
   if(from->is_function_call())
   {
-    if(from->function == to->function)
+    if(function_from == function_to)
     {
       control_dependencies(from, to, *dep_graph);
     }
diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index de7ee8c5a20..d7a8b6c1340 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -81,7 +81,9 @@ class dep_graph_domaint:public ai_domain_baset
     goto_programt::const_targett to);
 
   void transform(
+    const irep_idt &function_from,
     goto_programt::const_targett from,
+    const irep_idt &function_to,
     goto_programt::const_targett to,
     ai_baset &ai,
     const namespacet &ns) final override;
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
index c6ff1cd49ed..ba06b5854b0 100644
--- a/src/analyses/escape_analysis.cpp
+++ b/src/analyses/escape_analysis.cpp
@@ -166,7 +166,9 @@ void escape_domaint::get_rhs_aliases_address_of(
 }
 
 void escape_domaint::transform(
+  const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt,
   ai_baset &,
   const namespacet &)
diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h
index 1ea16879a10..1324e508698 100644
--- a/src/analyses/escape_analysis.h
+++ b/src/analyses/escape_analysis.h
@@ -28,9 +28,13 @@ class escape_domaint:public ai_domain_baset
   {
   }
 
-  void
-  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
-    final override;
+  void transform(
+    const irep_idt &function_from,
+    locationt from,
+    const irep_idt &function_to,
+    locationt to,
+    ai_baset &ai,
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp
index ce823ab9a66..cf24920144b 100644
--- a/src/analyses/global_may_alias.cpp
+++ b/src/analyses/global_may_alias.cpp
@@ -76,7 +76,9 @@ void global_may_alias_domaint::get_rhs_aliases_address_of(
 }
 
 void global_may_alias_domaint::transform(
+  const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt,
   ai_baset &,
   const namespacet &)
diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h
index 2d7491d0ada..98af9d55627 100644
--- a/src/analyses/global_may_alias.h
+++ b/src/analyses/global_may_alias.h
@@ -28,9 +28,13 @@ class global_may_alias_domaint:public ai_domain_baset
   {
   }
 
-  void
-  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
-    final override;
+  void transform(
+    const irep_idt &function_from,
+    locationt from,
+    const irep_idt &function_to,
+    locationt to,
+    ai_baset &ai,
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 3e0db34c306..efa128fbbb5 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -57,7 +57,9 @@ void interval_domaint::output(
 }
 
 void interval_domaint::transform(
+  const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt to,
   ai_baset &,
   const namespacet &ns)
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index 15c75e455d7..19f07484876 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -32,9 +32,13 @@ class interval_domaint:public ai_domain_baset
   {
   }
 
-  void
-  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
-    final override;
+  void transform(
+    const irep_idt &function_from,
+    locationt from,
+    const irep_idt &function_to,
+    locationt to,
+    ai_baset &ai,
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
index f7a524e7554..b25878a7a8c 100644
--- a/src/analyses/invariant_set_domain.cpp
+++ b/src/analyses/invariant_set_domain.cpp
@@ -14,7 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 
 void invariant_set_domaint::transform(
+  const irep_idt &function_from,
   locationt from_l,
+  const irep_idt &function_to,
   locationt to_l,
   ai_baset &,
   const namespacet &ns)
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 94a09a40ff3..55c22572b71 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -53,7 +53,9 @@ class invariant_set_domaint:public ai_domain_baset
   }
 
   virtual void transform(
+    const irep_idt &function_from,
     locationt from_l,
+    const irep_idt &function_to,
     locationt to_l,
     ai_baset &ai,
     const namespacet &ns) final override;
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index c48edd1113d..a39d3c3c39b 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -46,9 +46,13 @@ class is_threaded_domaint:public ai_domain_baset
            old_is_threaded!=is_threaded;
   }
 
-  void
-  transform(locationt from, locationt, ai_baset &, const namespacet &)
-    final override
+  void transform(
+    const irep_idt &,
+    locationt from,
+    const irep_idt &,
+    locationt,
+    ai_baset &,
+    const namespacet &) final override
   {
     INVARIANT(reachable,
               "Transformers are only applied at reachable locations");
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index 2d2bc3b1dee..d6dfd5957bb 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -56,7 +56,9 @@ void rd_range_domaint::populate_cache(const irep_idt &identifier) const
 }
 
 void rd_range_domaint::transform(
+  const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt to,
   ai_baset &ai,
   const namespacet &ns)
@@ -78,10 +80,10 @@ void rd_range_domaint::transform(
     transform_start_thread(ns, *rd);
   // do argument-to-parameter assignments
   else if(from->is_function_call())
-    transform_function_call(ns, from, to, *rd);
+    transform_function_call(ns, function_from, from, function_to, to, *rd);
   // cleanup parameters
   else if(from->is_end_function())
-    transform_end_function(ns, from, to, *rd);
+    transform_end_function(ns, function_from, from, function_to, to, *rd);
   // lhs assignments
   else if(from->is_assign())
     transform_assign(ns, from, from, *rd);
@@ -167,14 +169,16 @@ void rd_range_domaint::transform_start_thread(
 
 void rd_range_domaint::transform_function_call(
   const namespacet &ns,
+  const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt to,
   reaching_definitions_analysist &rd)
 {
   const code_function_callt &code=to_code_function_call(from->code);
 
   // only if there is an actual call, i.e., we have a body
-  if(from->function != to->function)
+  if(function_from != function_to)
   {
     for(valuest::iterator it=values.begin();
         it!=values.end();
@@ -229,11 +233,13 @@ void rd_range_domaint::transform_function_call(
 
 void rd_range_domaint::transform_end_function(
   const namespacet &ns,
+  const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt to,
   reaching_definitions_analysist &rd)
 {
-  goto_programt::const_targett call=to;
+  locationt call = to;
   --call;
   const code_function_callt &code=to_code_function_call(call->code);
 
@@ -263,8 +269,7 @@ void rd_range_domaint::transform_end_function(
     }
   }
 
-  const code_typet &code_type=
-    to_code_type(ns.lookup(from->function).type);
+  const code_typet &code_type = to_code_type(ns.lookup(function_from).type);
 
   for(const auto &param : code_type.parameters())
   {
@@ -666,8 +671,8 @@ bool rd_range_domaint::merge(
 /// \return returns true iff there is something new
 bool rd_range_domaint::merge_shared(
   const rd_range_domaint &other,
-  goto_programt::const_targett,
-  goto_programt::const_targett,
+  locationt,
+  locationt,
   const namespacet &ns)
 {
   // TODO: dirty vars
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index a4fd7702367..c00745d70ab 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -113,9 +113,13 @@ class rd_range_domaint:public ai_domain_baset
     bv_container=&_bv_container;
   }
 
-  void
-  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
-    final override;
+  void transform(
+    const irep_idt &function_from,
+    locationt from,
+    const irep_idt &function_to,
+    locationt to,
+    ai_baset &ai,
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
@@ -212,12 +216,16 @@ class rd_range_domaint:public ai_domain_baset
     reaching_definitions_analysist &rd);
   void transform_function_call(
     const namespacet &ns,
+    const irep_idt &function_from,
     locationt from,
+    const irep_idt &function_to,
     locationt to,
     reaching_definitions_analysist &rd);
   void transform_end_function(
     const namespacet &ns,
+    const irep_idt &function_from,
     locationt from,
+    const irep_idt &function_to,
     locationt to,
     reaching_definitions_analysist &rd);
   void transform_assign(
@@ -256,10 +264,9 @@ class reaching_definitions_analysist:
 
   virtual ~reaching_definitions_analysist();
 
-  virtual void initialize(
-    const goto_functionst &goto_functions) override;
+  void initialize(const goto_functionst &goto_functions) override;
 
-  virtual statet &get_state(goto_programt::const_targett l) override
+  statet &get_state(locationt l) override
   {
     statet &s=concurrency_aware_ait<rd_range_domaint>::get_state(l);
 
diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp
index 04c0bb8d0fa..c5f45750ba6 100644
--- a/src/analyses/uninitialized_domain.cpp
+++ b/src/analyses/uninitialized_domain.cpp
@@ -19,7 +19,9 @@ Date: January 2010
 #include <list>
 
 void uninitialized_domaint::transform(
+  const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt,
   ai_baset &,
   const namespacet &ns)
diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h
index 2d957d0bbb5..a2a04d272fa 100644
--- a/src/analyses/uninitialized_domain.h
+++ b/src/analyses/uninitialized_domain.h
@@ -29,9 +29,13 @@ class uninitialized_domaint:public ai_domain_baset
   typedef std::set<irep_idt> uninitializedt;
   uninitializedt uninitialized;
 
-  void
-  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
-    final override;
+  void transform(
+    const irep_idt &function_from,
+    locationt from,
+    const irep_idt &function_to,
+    locationt to,
+    ai_baset &ai,
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp
index e01493a0f22..1c5e85b68fc 100644
--- a/src/goto-instrument/uninitialized.cpp
+++ b/src/goto-instrument/uninitialized.cpp
@@ -28,7 +28,9 @@ class uninitializedt
   {
   }
 
-  void add_assertions(goto_programt &goto_program);
+  void add_assertions(
+    const irep_idt &function_identifer,
+    goto_programt &goto_program);
 
 protected:
   symbol_tablet &symbol_table;
@@ -63,9 +65,11 @@ void uninitializedt::get_tracking(goto_programt::const_targett i_it)
   }
 }
 
-void uninitializedt::add_assertions(goto_programt &goto_program)
+void uninitializedt::add_assertions(
+  const irep_idt &function_identifier,
+  goto_programt &goto_program)
 {
-  uninitialized_analysis(goto_program, ns);
+  uninitialized_analysis(function_identifier, goto_program, ns);
 
   // find out which variables need tracking
 
@@ -200,7 +204,7 @@ void add_uninitialized_locals_assertions(goto_modelt &goto_model)
   {
     uninitializedt uninitialized(goto_model.symbol_table);
 
-    uninitialized.add_assertions(f_it->second.body);
+    uninitialized.add_assertions(f_it->first, f_it->second.body);
   }
 }
 
@@ -218,7 +222,7 @@ void show_uninitialized(
       out << "//// Function: " << f_it->first << '\n';
       out << "////\n\n";
       uninitialized_analysist uninitialized_analysis;
-      uninitialized_analysis(f_it->second.body, ns);
+      uninitialized_analysis(f_it->first, f_it->second.body, ns);
       uninitialized_analysis.output(ns, f_it->second.body, out);
     }
   }
diff --git a/unit/analyses/ai/ai.cpp b/unit/analyses/ai/ai.cpp
index 5aee8d8fd83..9b385f4c2fa 100644
--- a/unit/analyses/ai/ai.cpp
+++ b/unit/analyses/ai/ai.cpp
@@ -36,7 +36,13 @@ class instruction_counter_domaint : public ai_domain_baset
 
   optionalt<unsigned> path_length;
 
-  void transform(locationt, locationt, ai_baset &, const namespacet &) override
+  void transform(
+    const irep_idt &,
+    locationt,
+    const irep_idt &,
+    locationt,
+    ai_baset &,
+    const namespacet &) override
   {
     if(*path_length < 100)
       ++*path_length;
diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp
index 115c724aac4..ee566596e05 100644
--- a/unit/analyses/ai/ai_simplify_lhs.cpp
+++ b/unit/analyses/ai/ai_simplify_lhs.cpp
@@ -26,7 +26,13 @@
 class constant_simplification_mockt:public ai_domain_baset
 {
 public:
-  void transform(locationt, locationt, ai_baset &, const namespacet &) override
+  void transform(
+    const irep_idt &,
+    locationt,
+    const irep_idt &,
+    locationt,
+    ai_baset &,
+    const namespacet &) override
   {}
   void make_bottom() override
   {}
diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp
index 0c2936b5982..37f68599595 100644
--- a/unit/analyses/constant_propagator.cpp
+++ b/unit/analyses/constant_propagator.cpp
@@ -83,7 +83,7 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
     WHEN("We apply conventional constant propagation")
     {
       constant_propagator_ait constant_propagator(main_function);
-      constant_propagator(main_function, ns);
+      constant_propagator(main_function_symbol.name, main_function, ns);
 
       THEN("The propagator should discover values for both 'x' and 'y'")
       {
@@ -97,7 +97,7 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
     WHEN("We apply constant propagation for symbols beginning with 'x'")
     {
       constant_propagator_ait constant_propagator(main_function, starts_with_x);
-      constant_propagator(main_function, ns);
+      constant_propagator(main_function_symbol.name, main_function, ns);
 
       THEN("The propagator should discover a value for 'x' but not 'y'")
       {