diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
index eb20d1fa5be..3075d87c2c7 100644
--- a/src/analyses/flow_insensitive_analysis.cpp
+++ b/src/analyses/flow_insensitive_analysis.cpp
@@ -53,12 +53,12 @@ void flow_insensitive_analysis_baset::operator()(
   fixedpoint(goto_functions);
 }
 
-void flow_insensitive_analysis_baset::operator()(
-  const goto_programt &goto_program)
+void flow_insensitive_analysis_baset::
+operator()(const irep_idt &function_id, const goto_programt &goto_program)
 {
   initialize(goto_program);
   goto_functionst goto_functions;
-  fixedpoint(goto_program, goto_functions);
+  fixedpoint(function_id, goto_program, goto_functions);
 }
 
 void flow_insensitive_analysis_baset::output(
@@ -69,14 +69,14 @@ void flow_insensitive_analysis_baset::output(
   {
     out << "////\n" << "//// Function: " << f_it->first << "\n////\n\n";
 
-    output(f_it->second.body, f_it->first, out);
+    output(f_it->first, f_it->second.body, out);
   }
 }
 
 void flow_insensitive_analysis_baset::output(
-  const goto_programt &,
   const irep_idt &,
-  std::ostream &out) const
+  const goto_programt &,
+  std::ostream &out)
 {
   get_state().output(ns, out);
 }
@@ -99,6 +99,7 @@ flow_insensitive_analysis_baset::get_next(
 }
 
 bool flow_insensitive_analysis_baset::fixedpoint(
+  const irep_idt &function_id,
   const goto_programt &goto_program,
   const goto_functionst &goto_functions)
 {
@@ -119,7 +120,7 @@ bool flow_insensitive_analysis_baset::fixedpoint(
   {
     locationt l=get_next(working_set);
 
-    if(visit(l, working_set, goto_program, goto_functions))
+    if(visit(function_id, l, working_set, goto_program, goto_functions))
       new_data=true;
   }
 
@@ -127,6 +128,7 @@ bool flow_insensitive_analysis_baset::fixedpoint(
 }
 
 bool flow_insensitive_analysis_baset::visit(
+  const irep_idt &function_id,
   locationt l,
   working_sett &working_set,
   const goto_programt &goto_program,
@@ -157,16 +159,16 @@ bool flow_insensitive_analysis_baset::visit(
       // this is a big special case
       const code_function_callt &code = to_code_function_call(l->code);
 
-      changed=
-        do_function_call_rec(
-          l,
-          code.function(),
-          code.arguments(),
-          get_state(),
-          goto_functions);
+      changed = do_function_call_rec(
+        function_id,
+        l,
+        code.function(),
+        code.arguments(),
+        get_state(),
+        goto_functions);
     }
     else
-      changed = get_state().transform(ns, l, to_l);
+      changed = get_state().transform(ns, function_id, l, function_id, to_l);
 
     if(changed || !seen(to_l))
     {
@@ -193,6 +195,7 @@ bool flow_insensitive_analysis_baset::visit(
 }
 
 bool flow_insensitive_analysis_baset::do_function_call(
+  const irep_idt &calling_function,
   locationt l_call,
   const goto_functionst &goto_functions,
   const goto_functionst::function_mapt::const_iterator f_it,
@@ -221,9 +224,15 @@ bool flow_insensitive_analysis_baset::do_function_call(
     t->location_number=1;
 
     locationt l_next=l_call; l_next++;
-    bool new_data=state.transform(ns, l_call, r);
-    new_data = state.transform(ns, r, t) || new_data;
-    new_data = state.transform(ns, t, l_next) || new_data;
+    // do the edge from the call site to the simulated function (the artificial
+    // return statement that we just generated)
+    bool new_data =
+      state.transform(ns, calling_function, l_call, f_it->first, r);
+    // do the edge from the return to the artificial end-of-function
+    new_data = state.transform(ns, f_it->first, r, f_it->first, t) || new_data;
+    // do edge from (artificial) end of function to instruction after call
+    new_data =
+      state.transform(ns, f_it->first, t, calling_function, l_next) || new_data;
 
     return new_data;
   }
@@ -240,7 +249,8 @@ bool flow_insensitive_analysis_baset::do_function_call(
       l_begin->function == f_it->first, "function names have to match");
 
     // do the edge from the call site to the beginning of the function
-    new_data=state.transform(ns, l_call, l_begin);
+    new_data =
+      state.transform(ns, calling_function, l_call, f_it->first, l_begin);
 
     // do each function at least once
     if(functions_done.find(f_it->first)==
@@ -254,7 +264,7 @@ bool flow_insensitive_analysis_baset::do_function_call(
     if(new_data)
     {
       // recursive call
-      fixedpoint(goto_function.body, goto_functions);
+      fixedpoint(f_it->first, goto_function.body, goto_functions);
       new_data=true; // could be reset by fixedpoint
     }
   }
@@ -268,13 +278,16 @@ bool flow_insensitive_analysis_baset::do_function_call(
     // do edge from end of function to instruction after call
     locationt l_next=l_call;
     l_next++;
-    new_data = state.transform(ns, l_end, l_next) || new_data;
+    new_data =
+      state.transform(ns, f_it->first, l_end, calling_function, l_next) ||
+      new_data;
   }
 
   return new_data;
 }
 
 bool flow_insensitive_analysis_baset::do_function_call_rec(
+  const irep_idt &calling_function,
   locationt l_call,
   const exprt &function,
   const exprt::operandst &arguments,
@@ -301,13 +314,8 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
     if(it==goto_functions.function_map.end())
       throw "failed to find function "+id2string(identifier);
 
-    new_data =
-      do_function_call(
-        l_call,
-        goto_functions,
-        it,
-        arguments,
-        state);
+    new_data = do_function_call(
+      calling_function, l_call, goto_functions, it, arguments, state);
 
     recursion_set.erase(identifier);
   }
@@ -316,12 +324,21 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
     const auto &if_expr = to_if_expr(function);
 
     new_data = do_function_call_rec(
-      l_call, if_expr.true_case(), arguments, state, goto_functions);
+      calling_function,
+      l_call,
+      if_expr.true_case(),
+      arguments,
+      state,
+      goto_functions);
 
-    new_data =
-      do_function_call_rec(
-        l_call, if_expr.false_case(), arguments, state, goto_functions) ||
-      new_data;
+    new_data = do_function_call_rec(
+                 calling_function,
+                 l_call,
+                 if_expr.false_case(),
+                 arguments,
+                 state,
+                 goto_functions) ||
+               new_data;
   }
   else if(function.id()==ID_dereference)
   {
@@ -343,13 +360,14 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
 
         if(it!=goto_functions.function_map.end())
         {
-          new_data =
-            do_function_call_rec(
-              l_call,
-              o.object(),
-              arguments,
-              state,
-              goto_functions) || new_data;
+          new_data = do_function_call_rec(
+                       calling_function,
+                       l_call,
+                       o.object(),
+                       arguments,
+                       state,
+                       goto_functions) ||
+                     new_data;
         }
       }
     }
@@ -392,7 +410,7 @@ bool flow_insensitive_analysis_baset::fixedpoint(
   const goto_functionst &goto_functions)
 {
   functions_done.insert(it->first);
-  return fixedpoint(it->second.body, goto_functions);
+  return fixedpoint(it->first, it->second.body, goto_functions);
 }
 
 void flow_insensitive_analysis_baset::update(const goto_functionst &)
diff --git a/src/analyses/flow_insensitive_analysis.h b/src/analyses/flow_insensitive_analysis.h
index a1653622389..3e1c4674122 100644
--- a/src/analyses/flow_insensitive_analysis.h
+++ b/src/analyses/flow_insensitive_analysis.h
@@ -47,8 +47,10 @@ class flow_insensitive_abstract_domain_baset
 
   virtual bool transform(
     const namespacet &ns,
+    const irep_idt &function_from,
     locationt from,
-    locationt to)=0;
+    const irep_idt &function_to,
+    locationt to) = 0;
 
   virtual ~flow_insensitive_abstract_domain_baset()
   {
@@ -126,8 +128,8 @@ class flow_insensitive_analysis_baset
 
   virtual void update(const goto_functionst &goto_functions);
 
-  virtual void operator()(
-    const goto_programt &goto_program);
+  virtual void
+  operator()(const irep_idt &function_id, const goto_programt &goto_program);
 
   virtual void operator()(
     const goto_functionst &goto_functions);
@@ -146,20 +148,13 @@ class flow_insensitive_analysis_baset
     std::ostream &out);
 
   virtual void output(
+    const irep_idt &function_id,
     const goto_programt &goto_program,
-    std::ostream &out)
-  {
-    output(goto_program, "", out);
-  }
+    std::ostream &out);
 
 protected:
   const namespacet &ns;
 
-  virtual void output(
-    const goto_programt &goto_program,
-    const irep_idt &identifier,
-    std::ostream &out) const;
-
   typedef std::priority_queue<locationt> working_sett;
 
   locationt get_next(working_sett &working_set);
@@ -173,6 +168,7 @@ class flow_insensitive_analysis_baset
 
   // true = found something new
   bool fixedpoint(
+    const irep_idt &function_id,
     const goto_programt &goto_program,
     const goto_functionst &goto_functions);
 
@@ -185,6 +181,7 @@ class flow_insensitive_analysis_baset
 
   // true = found something new
   bool visit(
+    const irep_idt &function_id,
     locationt l,
     working_sett &working_set,
     const goto_programt &goto_program,
@@ -206,6 +203,7 @@ class flow_insensitive_analysis_baset
 
   // function calls
   bool do_function_call_rec(
+    const irep_idt &calling_function,
     locationt l_call,
     const exprt &function,
     const exprt::operandst &arguments,
@@ -213,6 +211,7 @@ class flow_insensitive_analysis_baset
     const goto_functionst &goto_functions);
 
   bool do_function_call(
+    const irep_idt &calling_function,
     locationt l_call,
     const goto_functionst &goto_functions,
     const goto_functionst::function_mapt::const_iterator f_it,
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 6b2926c8694..81d1c7f86fc 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -626,7 +626,7 @@ void rw_range_set_value_sett::get_objects_dereference(
     size);
 
   exprt object=deref;
-  dereference(target, object, ns, value_sets);
+  dereference(function, target, object, ns, value_sets);
 
   auto type_bits = pointer_offset_bits(object.type(), ns);
 
diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp
index 7f29f3030f1..8e6be956dbd 100644
--- a/src/goto-instrument/rw_set.cpp
+++ b/src/goto-instrument/rw_set.cpp
@@ -159,7 +159,7 @@ void _rw_set_loct::read_write_rec(
       read_write_rec(*it, r, w, suffix, guard);
     }
     #else
-    dereference(target, tmp, ns, value_sets);
+    dereference(function_id, target, tmp, ns, value_sets);
 
     read_write_rec(tmp, r, w, suffix, guard);
     #endif
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index 8b604408108..cdf9a972d90 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -113,7 +113,8 @@ void preconditiont::compute_rec(exprt &dest)
     // aliasing may happen here
 
     value_setst::valuest expr_set;
-    value_sets.get_values(target, deref_expr.pointer(), expr_set);
+    value_sets.get_values(
+      SSA_step.source.function_id, target, deref_expr.pointer(), expr_set);
     std::unordered_set<irep_idt> symbols;
 
     for(value_setst::valuest::const_iterator
@@ -127,7 +128,7 @@ void preconditiont::compute_rec(exprt &dest)
       // may alias!
       exprt tmp;
       tmp.swap(deref_expr.pointer());
-      dereference(target, tmp, ns, value_sets);
+      dereference(SSA_step.source.function_id, target, tmp, ns, value_sets);
       deref_expr.swap(tmp);
       compute_rec(deref_expr);
     }
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
index b9e3ca64d7e..a029883ffe7 100644
--- a/src/pointer-analysis/goto_program_dereference.cpp
+++ b/src/pointer-analysis/goto_program_dereference.cpp
@@ -227,7 +227,7 @@ void goto_program_dereferencet::get_value_set(
   const exprt &expr,
   value_setst::valuest &dest)
 {
-  value_sets.get_values(current_target, expr, dest);
+  value_sets.get_values(current_function, current_target, expr, dest);
 }
 
 /// Remove dereference expressions contained in `expr`.
@@ -357,9 +357,11 @@ void goto_program_dereferencet::dereference_instruction(
 
 /// Set the current target to `target` and remove derefence from expr.
 void goto_program_dereferencet::dereference_expression(
+  const irep_idt &function_id,
   goto_programt::const_targett target,
   exprt &expr)
 {
+  current_function = function_id;
   current_target=target;
   #if 0
   valid_local_variables=&target->local_variables;
@@ -448,6 +450,7 @@ void pointer_checks(
 /// Remove dereferences in `expr` using `value_sets` to determine to what
 /// objects the pointers may be pointing to.
 void dereference(
+  const irep_idt &function_id,
   goto_programt::const_targett target,
   exprt &expr,
   const namespacet &ns,
@@ -457,5 +460,5 @@ void dereference(
   symbol_tablet new_symbol_table;
   goto_program_dereferencet
     goto_program_dereference(ns, new_symbol_table, options, value_sets);
-  goto_program_dereference.dereference_expression(target, expr);
+  goto_program_dereference.dereference_expression(function_id, target, expr);
 }
diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h
index 0f15a891d33..34cf6dc52c0 100644
--- a/src/pointer-analysis/goto_program_dereference.h
+++ b/src/pointer-analysis/goto_program_dereference.h
@@ -52,6 +52,7 @@ class goto_program_dereferencet:protected dereference_callbackt
   void pointer_checks(goto_functionst &goto_functions);
 
   void dereference_expression(
+    const irep_idt &function_id,
     goto_programt::const_targett target,
     exprt &expr);
 
@@ -93,6 +94,7 @@ class goto_program_dereferencet:protected dereference_callbackt
 #if 0
   const std::set<irep_idt> *valid_local_variables;
 #endif
+  irep_idt current_function;
   goto_programt::const_targett current_target;
 
   /// Unused
@@ -106,6 +108,7 @@ class goto_program_dereferencet:protected dereference_callbackt
 };
 
 void dereference(
+  const irep_idt &function_id,
   goto_programt::const_targett target,
   exprt &expr,
   const namespacet &,
diff --git a/src/pointer-analysis/value_set_analysis.h b/src/pointer-analysis/value_set_analysis.h
index 34acca8f406..94206b00b51 100644
--- a/src/pointer-analysis/value_set_analysis.h
+++ b/src/pointer-analysis/value_set_analysis.h
@@ -59,6 +59,7 @@ class value_set_analysis_templatet:
 public:
   // interface value_sets
   virtual void get_values(
+    const irep_idt &,
     locationt l,
     const exprt &expr,
     value_setst::valuest &dest)
diff --git a/src/pointer-analysis/value_set_analysis_fi.h b/src/pointer-analysis/value_set_analysis_fi.h
index da50d27357c..ec6b9d99a81 100644
--- a/src/pointer-analysis/value_set_analysis_fi.h
+++ b/src/pointer-analysis/value_set_analysis_fi.h
@@ -35,8 +35,8 @@ class value_set_analysis_fit:
 
   typedef flow_insensitive_analysist<value_set_domain_fit> baset;
 
-  virtual void initialize(const goto_programt &goto_program);
-  virtual void initialize(const goto_functionst &goto_functions);
+  void initialize(const goto_programt &goto_program) override;
+  void initialize(const goto_functionst &goto_functions) override;
 
 protected:
   track_optionst track_options;
@@ -58,15 +58,16 @@ class value_set_analysis_fit:
 
 public:
   // interface value_sets
-  virtual void get_values(
+  void get_values(
+    const irep_idt &function_id,
     locationt l,
     const exprt &expr,
-    std::list<exprt> &dest)
+    std::list<exprt> &dest) override
   {
     state.value_set.from_function =
-      state.value_set.function_numbering.number(l->function);
+      state.value_set.function_numbering.number(function_id);
     state.value_set.to_function =
-      state.value_set.function_numbering.number(l->function);
+      state.value_set.function_numbering.number(function_id);
     state.value_set.from_target_index = l->location_number;
     state.value_set.to_target_index = l->location_number;
     state.value_set.get_value_set(expr, dest, ns);
diff --git a/src/pointer-analysis/value_set_analysis_fivr.h b/src/pointer-analysis/value_set_analysis_fivr.h
index edd1b512f32..67b02213129 100644
--- a/src/pointer-analysis/value_set_analysis_fivr.h
+++ b/src/pointer-analysis/value_set_analysis_fivr.h
@@ -35,25 +35,28 @@ class value_set_analysis_fivrt:
 
   typedef flow_insensitive_analysist<value_set_domain_fivrt> baset;
 
-  virtual void initialize(const goto_programt &goto_program);
-  virtual void initialize(const goto_functionst &goto_functions);
+  void initialize(const goto_programt &goto_program) override;
+  void initialize(const goto_functionst &goto_functions) override;
 
   using baset::output;
-  void output(locationt l, std::ostream &out)
+  void output(const irep_idt &function_id, locationt l, std::ostream &out)
   {
-    state.value_set.set_from(l->function, l->location_number);
-    state.value_set.set_to(l->function, l->location_number);
+    state.value_set.set_from(function_id, l->location_number);
+    state.value_set.set_to(function_id, l->location_number);
     state.output(ns, out);
   }
 
-  void output(const goto_programt &goto_program, std::ostream &out)
+  void output(
+    const irep_idt &function_id,
+    const goto_programt &goto_program,
+    std::ostream &out) override
   {
     forall_goto_program_instructions(it, goto_program)
     {
       out << "**** " << it->source_location << '\n';
-      output(it, out);
+      output(function_id, it, out);
       out << '\n';
-      goto_program.output_instruction(ns, "", out, *it);
+      goto_program.output_instruction(ns, function_id, out, *it);
       out << '\n';
     }
   }
@@ -78,15 +81,16 @@ class value_set_analysis_fivrt:
 
 public:
   // interface value_sets
-  virtual void get_values(
+  void get_values(
+    const irep_idt &function_id,
     locationt l,
     const exprt &expr,
-    std::list<exprt> &dest)
+    std::list<exprt> &dest) override
   {
     state.value_set.from_function =
-      state.value_set.function_numbering.number(l->function);
+      state.value_set.function_numbering.number(function_id);
     state.value_set.to_function =
-      state.value_set.function_numbering.number(l->function);
+      state.value_set.function_numbering.number(function_id);
     state.value_set.from_target_index = l->location_number;
     state.value_set.to_target_index = l->location_number;
     state.value_set.get_value_set(expr, dest, ns);
diff --git a/src/pointer-analysis/value_set_analysis_fivrns.h b/src/pointer-analysis/value_set_analysis_fivrns.h
index d87595b02a1..eea3160d7df 100644
--- a/src/pointer-analysis/value_set_analysis_fivrns.h
+++ b/src/pointer-analysis/value_set_analysis_fivrns.h
@@ -41,21 +41,24 @@ class value_set_analysis_fivrnst:
 
   using baset::output;
 
-  virtual void output(locationt l, std::ostream &out)
+  void output(const irep_idt &function_id, locationt l, std::ostream &out)
   {
-    state.value_set.set_from(l->function, l->location_number);
-    state.value_set.set_to(l->function, l->location_number);
+    state.value_set.set_from(function_id, l->location_number);
+    state.value_set.set_to(function_id, l->location_number);
     state.output(ns, out);
   }
 
-  void output(const goto_programt &goto_program, std::ostream &out)
+  void output(
+    const irep_idt &function_id,
+    const goto_programt &goto_program,
+    std::ostream &out)
   {
     forall_goto_program_instructions(it, goto_program)
     {
       out << "**** " << it->source_location << '\n';
-      output(it, out);
+      output(function_id, it, out);
       out << '\n';
-      goto_program.output_instruction(ns, "", out, *it);
+      goto_program.output_instruction(ns, function_id, out, *it);
       out << '\n';
     }
   }
@@ -81,14 +84,15 @@ class value_set_analysis_fivrnst:
 public:
   // interface value_sets
   virtual void get_values(
+    const irep_idt &function_id,
     locationt l,
     const exprt &expr,
     std::list<exprt> &dest)
   {
     state.value_set.from_function =
-      state.value_set.function_numbering.number(l->function);
+      state.value_set.function_numbering.number(function_id);
     state.value_set.to_function =
-      state.value_set.function_numbering.number(l->function);
+      state.value_set.function_numbering.number(function_id);
     state.value_set.from_target_index = l->location_number;
     state.value_set.to_target_index = l->location_number;
     state.value_set.get_value_set(expr, dest, ns);
diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp
index 09bc21174f5..12702e046a1 100644
--- a/src/pointer-analysis/value_set_domain_fi.cpp
+++ b/src/pointer-analysis/value_set_domain_fi.cpp
@@ -16,17 +16,19 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool value_set_domain_fit::transform(
   const namespacet &ns,
+  const irep_idt &function_from,
   locationt from_l,
+  const irep_idt &function_to,
   locationt to_l)
 {
   value_set.changed = false;
 
-  value_set.set_from(from_l->function, from_l->location_number);
-  value_set.set_to(to_l->function, to_l->location_number);
+  value_set.set_from(function_from, from_l->location_number);
+  value_set.set_to(function_to, to_l->location_number);
 
-//  std::cout << "transforming: " <<
-//      from_l->function << " " << from_l->location_number << " to " <<
-//      to_l->function << " " << to_l->location_number << '\n';
+  //  std::cout << "transforming: " <<
+  //      from_l->function << " " << from_l->location_number << " to " <<
+  //      to_l->function << " " << to_l->location_number << '\n';
 
   switch(from_l->type)
   {
@@ -49,7 +51,7 @@ bool value_set_domain_fit::transform(
       const code_function_callt &code=
         to_code_function_call(from_l->code);
 
-      value_set.do_function_call(to_l->function, code.arguments(), ns);
+      value_set.do_function_call(function_to, code.arguments(), ns);
     }
     break;
 
diff --git a/src/pointer-analysis/value_set_domain_fi.h b/src/pointer-analysis/value_set_domain_fi.h
index e50ebcc8f7a..f6412dfb7a9 100644
--- a/src/pointer-analysis/value_set_domain_fi.h
+++ b/src/pointer-analysis/value_set_domain_fi.h
@@ -29,32 +29,32 @@ class value_set_domain_fit:public flow_insensitive_abstract_domain_baset
 //    return value_set.make_union(other.value_set);
 //  }
 
-  virtual void output(
-    const namespacet &ns,
-    std::ostream &out) const
+  void output(const namespacet &ns, std::ostream &out) const override
   {
     value_set.output(ns, out);
   }
 
-  virtual void initialize(const namespacet &)
+  void initialize(const namespacet &) override
   {
     value_set.clear();
   }
 
-  virtual bool transform(
+  bool transform(
     const namespacet &ns,
+    const irep_idt &function_from,
     locationt from_l,
-    locationt to_l);
+    const irep_idt &function_to,
+    locationt to_l) override;
 
-  virtual void get_reference_set(
+  void get_reference_set(
     const namespacet &ns,
     const exprt &expr,
-    expr_sett &expr_set)
+    expr_sett &expr_set) override
   {
     value_set.get_reference_set(expr, expr_set, ns);
   }
 
-  virtual void clear(void)
+  void clear(void) override
   {
     value_set.clear();
   }
diff --git a/src/pointer-analysis/value_set_domain_fivr.cpp b/src/pointer-analysis/value_set_domain_fivr.cpp
index 27fec810fcc..7e45ce424a6 100644
--- a/src/pointer-analysis/value_set_domain_fivr.cpp
+++ b/src/pointer-analysis/value_set_domain_fivr.cpp
@@ -16,17 +16,19 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool value_set_domain_fivrt::transform(
   const namespacet &ns,
+  const irep_idt &function_from,
   locationt from_l,
+  const irep_idt &function_to,
   locationt to_l)
 {
-  value_set.set_from(from_l->function, from_l->location_number);
-  value_set.set_to(to_l->function, to_l->location_number);
+  value_set.set_from(function_from, from_l->location_number);
+  value_set.set_to(function_to, to_l->location_number);
 
-  #if 0
+#if 0
   std::cout << "Transforming: " <<
     from_l->function << " " << from_l->location_number << " to " <<
     to_l->function << " " << to_l->location_number << '\n';
-  #endif
+#endif
 
   switch(from_l->type)
   {
@@ -45,7 +47,7 @@ bool value_set_domain_fivrt::transform(
       const code_function_callt &code=
         to_code_function_call(from_l->code);
 
-      value_set.do_function_call(to_l->function, code.arguments(), ns);
+      value_set.do_function_call(function_to, code.arguments(), ns);
       break;
     }
 
diff --git a/src/pointer-analysis/value_set_domain_fivr.h b/src/pointer-analysis/value_set_domain_fivr.h
index 3dde90527e0..f1440d1462c 100644
--- a/src/pointer-analysis/value_set_domain_fivr.h
+++ b/src/pointer-analysis/value_set_domain_fivr.h
@@ -24,33 +24,32 @@ class value_set_domain_fivrt:public flow_insensitive_abstract_domain_baset
 
   // overloading
 
-  virtual void output(
-    const namespacet &ns,
-    std::ostream &out) const
+  void output(const namespacet &ns, std::ostream &out) const override
   {
     value_set.output(ns, out);
   }
 
-  virtual void initialize(
-    const namespacet &)
+  void initialize(const namespacet &) override
   {
     value_set.clear();
   }
 
-  virtual bool transform(
+  bool transform(
     const namespacet &ns,
+    const irep_idt &function_from,
     locationt from_l,
-    locationt to_l);
+    const irep_idt &function_to,
+    locationt to_l) override;
 
-  virtual void get_reference_set(
+  void get_reference_set(
     const namespacet &ns,
     const exprt &expr,
-    expr_sett &expr_set)
+    expr_sett &expr_set) override
   {
     value_set.get_reference_set(expr, expr_set, ns);
   }
 
-  virtual void clear(void)
+  void clear(void) override
   {
     value_set.clear();
   }
diff --git a/src/pointer-analysis/value_set_domain_fivrns.cpp b/src/pointer-analysis/value_set_domain_fivrns.cpp
index c2ae1e81771..6baf68a059a 100644
--- a/src/pointer-analysis/value_set_domain_fivrns.cpp
+++ b/src/pointer-analysis/value_set_domain_fivrns.cpp
@@ -16,17 +16,19 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool value_set_domain_fivrnst::transform(
   const namespacet &ns,
+  const irep_idt &function_from,
   locationt from_l,
+  const irep_idt &function_to,
   locationt to_l)
 {
-  value_set.set_from(from_l->function, from_l->location_number);
-  value_set.set_to(to_l->function, to_l->location_number);
+  value_set.set_from(function_from, from_l->location_number);
+  value_set.set_to(function_to, to_l->location_number);
 
-  #if 0
+#if 0
   std::cout << "Transforming: " <<
     from_l->function << " " << from_l->location_number << " to " <<
     to_l->function << " " << to_l->location_number << '\n';
-  #endif
+#endif
 
   switch(from_l->type)
   {
@@ -45,7 +47,7 @@ bool value_set_domain_fivrnst::transform(
       const code_function_callt &code=
         to_code_function_call(from_l->code);
 
-      value_set.do_function_call(to_l->function, code.arguments(), ns);
+      value_set.do_function_call(function_to, code.arguments(), ns);
       break;
     }
 
diff --git a/src/pointer-analysis/value_set_domain_fivrns.h b/src/pointer-analysis/value_set_domain_fivrns.h
index 130f3367a4b..9ab79169681 100644
--- a/src/pointer-analysis/value_set_domain_fivrns.h
+++ b/src/pointer-analysis/value_set_domain_fivrns.h
@@ -40,7 +40,9 @@ class value_set_domain_fivrnst:
 
   virtual bool transform(
     const namespacet &ns,
+    const irep_idt &function_from,
     locationt from_l,
+    const irep_idt &function_to,
     locationt to_l);
 
   virtual void get_reference_set(
diff --git a/src/pointer-analysis/value_sets.h b/src/pointer-analysis/value_sets.h
index e230f72ebe7..24153a71781 100644
--- a/src/pointer-analysis/value_sets.h
+++ b/src/pointer-analysis/value_sets.h
@@ -29,9 +29,10 @@ class value_setst
 
   // this is not const to allow a lazy evaluation
   virtual void get_values(
+    const irep_idt &function_id,
     goto_programt::const_targett l,
     const exprt &expr,
-    valuest &dest)=0;
+    valuest &dest) = 0;
 
   virtual ~value_setst()
   {