From a99b25418cfdc9cead164dc6f8794a0521ead084 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 13 Oct 2017 10:48:47 +0100
Subject: [PATCH] Indirect value_set_domaint -> value_sett operations via
 non-member functions

These provide an oportunity for future implementers of value-sets not to have to
conform to the same public interface as value_sett, e.g. to provide some type they
can't or don't want to augment and provide non-member function specialisations
instead.
---
 src/pointer-analysis/value_set_domain.h | 92 ++++++++++++++++++++++---
 1 file changed, 82 insertions(+), 10 deletions(-)

diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h
index 4b0e0a876cf..163f3a183b3 100644
--- a/src/pointer-analysis/value_set_domain.h
+++ b/src/pointer-analysis/value_set_domain.h
@@ -17,6 +17,77 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "value_set.h"
 
+template<class> class value_set_domaint;
+
+// Forwarders for value_set_domaint's calls against value_sett.
+// Specialise these if for some reason you can't just write a member function,
+// or for location numbers, expose the field.
+template<typename VST>
+inline bool value_set_make_union(VST &value_set, const VST &other)
+{
+  return value_set.make_union(other);
+}
+
+template<typename VST>
+inline void value_set_output(
+  const VST &value_set, const namespacet &ns, std::ostream &out)
+{
+  value_set.output(ns, out);
+}
+
+template<typename VST>
+inline void value_set_clear(VST &value_set)
+{
+  value_set.clear();
+}
+
+template<typename VST>
+inline void value_set_set_location_number(VST &value_set, unsigned loc)
+{
+  value_set.location_number=loc;
+}
+
+template<typename VST>
+inline void value_set_read_reference_set(
+  const VST &value_set,
+  const exprt &expr,
+  value_setst::valuest &dest,
+  const namespacet &ns)
+{
+  value_set.read_reference_set(expr, dest, ns);
+}
+
+template<typename VST>
+inline void value_set_do_end_function(
+  VST &value_set, const exprt &return_expr, const namespacet &ns)
+{
+  value_set.do_end_function(return_expr, ns);
+}
+
+template<typename VST>
+inline void value_set_apply_code(
+  VST &value_set, const codet &code, const namespacet &ns)
+{
+  value_set.apply_code(code, ns);
+}
+
+template<typename VST>
+inline void value_set_guard(
+  VST &value_set, const exprt &guard, const namespacet &ns)
+{
+  value_set.guard(guard, ns);
+}
+
+template<typename VST>
+inline void value_set_do_function_call(
+  VST &value_set,
+  const irep_idt &function,
+  const exprt::operandst &arguments,
+  const namespacet &ns)
+{
+  value_set.do_function_call(function, arguments, ns);
+}
+
 template<class VST>
 class value_set_domaint:public domain_baset
 {
@@ -25,23 +96,23 @@ class value_set_domaint:public domain_baset
 
   // overloading
 
-  bool merge(const value_set_domaint &other, locationt to)
+  bool merge(const value_set_domaint<VST> &other, locationt to)
   {
-    return value_set.make_union(other.value_set);
+    return value_set_make_union(value_set, other.value_set);
   }
 
   virtual void output(
     const namespacet &ns,
     std::ostream &out) const
   {
-    value_set.output(ns, out);
+    value_set_output(value_set, ns, out);
   }
 
   virtual void initialize(
     const namespacet &ns,
     locationt l)
   {
-    value_set.clear();
+    value_set_clear(value_set);
     value_set.location_number=l->location_number;
   }
 
@@ -50,7 +121,7 @@ class value_set_domaint:public domain_baset
     const exprt &expr,
     value_setst::valuest &dest)
   {
-    value_set.read_reference_set(expr, dest, ns);
+    value_set_read_reference_set(value_set, expr, dest, ns);
   }
 
   virtual void transform(
@@ -66,8 +137,8 @@ class value_set_domaint:public domain_baset
 
     case END_FUNCTION:
     {
-      value_set.do_end_function(
-        static_analysis_baset::get_return_lhs(to_l), ns);
+      value_set_do_end_function(
+        value_set, static_analysis_baset::get_return_lhs(to_l), ns);
       break;
     }
 
@@ -77,11 +148,11 @@ class value_set_domaint:public domain_baset
     case ASSIGN:
     case DECL:
     case DEAD:
-      value_set.apply_code(from_l->code, ns);
+      value_set_apply_code(value_set, from_l->code, ns);
       break;
 
     case ASSUME:
-      value_set.guard(from_l->guard, ns);
+      value_set_guard(value_set, from_l->guard, ns);
       break;
 
     case FUNCTION_CALL:
@@ -89,7 +160,8 @@ class value_set_domaint:public domain_baset
         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(
+          value_set, to_l->function, code.arguments(), ns);
       }
     break;