From 73a3bd0be5270deefcad3f0e41c81915a7db6802 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Fri, 13 Jan 2017 11:32:34 +0000
Subject: [PATCH 01/17] Adding (failing) tests for function pointer removal

These tests demonstrate the different ways in which we could easily do
better in function pointer resolution. At the moment, each example
thinks the function pointer could be any of the 9 functions but in all
cases can do much better (either know exactly the function or subset of
functions)
---
 regression/goto-analyzer/fp-removal1/main.c   | 27 +++++++++++++++++
 .../goto-analyzer/fp-removal1/test.desc       |  8 +++++
 regression/goto-analyzer/fp-removal2/main.c   | 28 +++++++++++++++++
 .../goto-analyzer/fp-removal2/test.desc       |  8 +++++
 regression/goto-analyzer/fp-removal3/main.c   | 29 ++++++++++++++++++
 .../goto-analyzer/fp-removal3/test.desc       |  8 +++++
 regression/goto-analyzer/fp-removal4/main.c   | 30 +++++++++++++++++++
 .../goto-analyzer/fp-removal4/test.desc       |  8 +++++
 regression/goto-analyzer/fp-removal5/main.c   | 28 +++++++++++++++++
 .../goto-analyzer/fp-removal5/test.desc       | 11 +++++++
 10 files changed, 185 insertions(+)
 create mode 100644 regression/goto-analyzer/fp-removal1/main.c
 create mode 100644 regression/goto-analyzer/fp-removal1/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal2/main.c
 create mode 100644 regression/goto-analyzer/fp-removal2/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal3/main.c
 create mode 100644 regression/goto-analyzer/fp-removal3/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal4/main.c
 create mode 100644 regression/goto-analyzer/fp-removal4/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal5/main.c
 create mode 100644 regression/goto-analyzer/fp-removal5/test.desc

diff --git a/regression/goto-analyzer/fp-removal1/main.c b/regression/goto-analyzer/fp-removal1/main.c
new file mode 100644
index 00000000000..ec7927f5dba
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal1/main.c
@@ -0,0 +1,27 @@
+void f1 (void) { int tk = 1; }
+void f2 (void) { int tk = 2; }
+void f3 (void) { int tk = 3; }
+void f4 (void) { int tk = 4; }
+void f5 (void) { int tk = 5; }
+void f6 (void) { int tk = 6; }
+void f7 (void) { int tk = 7; }
+void f8 (void) { int tk = 8; }
+void f9 (void) { int tk = 9; }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+void_fp fp_tbl[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func1()
+{
+  void_fp fp = f2;
+  fp();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func1(i,0);
+   }
+}
diff --git a/regression/goto-analyzer/fp-removal1/test.desc b/regression/goto-analyzer/fp-removal1/test.desc
new file mode 100644
index 00000000000..707afa692b3
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp == f2 THEN GOTO 1$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal2/main.c b/regression/goto-analyzer/fp-removal2/main.c
new file mode 100644
index 00000000000..32600d7841d
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal2/main.c
@@ -0,0 +1,28 @@
+void f1 (void) { int tk = 1; }
+void f2 (void) { int tk = 2; }
+void f3 (void) { int tk = 3; }
+void f4 (void) { int tk = 4; }
+void f5 (void) { int tk = 5; }
+void f6 (void) { int tk = 6; }
+void f7 (void) { int tk = 7; }
+void f8 (void) { int tk = 8; }
+void f9 (void) { int tk = 9; }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+void_fp fp_tbl[] = {f1, f2, f3, f4, f5 ,f6, f7, f8, f9};
+
+void func2()
+{
+  void_fp fp = f2;
+  void_fp fp2 = fp;
+  fp2();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func2(i,0);
+   }
+}
diff --git a/regression/goto-analyzer/fp-removal2/test.desc b/regression/goto-analyzer/fp-removal2/test.desc
new file mode 100644
index 00000000000..690ca1ea037
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+^Removing function pointers and virtual functions$
+^\s*IF fp2 == f2 THEN GOTO 1$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal3/main.c b/regression/goto-analyzer/fp-removal3/main.c
new file mode 100644
index 00000000000..083846e61ba
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal3/main.c
@@ -0,0 +1,29 @@
+void f1 (void) { int tk = 1; }
+void f2 (void) { int tk = 2; }
+void f3 (void) { int tk = 3; }
+void f4 (void) { int tk = 4; }
+void f5 (void) { int tk = 5; }
+void f6 (void) { int tk = 6; }
+void f7 (void) { int tk = 7; }
+void f8 (void) { int tk = 8; }
+void f9 (void) { int tk = 9; }
+
+typedef void(*void_fp)(void);
+
+void_fp fp_tbl[] = {f1, f2 ,f3};
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+void_fp fp_tbl2[] = {f4, f5 ,f6, f7, f8, f9};
+
+void func3()
+{
+  void_fp fp = fp_tbl[2];
+  fp();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func3(i,0);
+   }
+}
diff --git a/regression/goto-analyzer/fp-removal3/test.desc b/regression/goto-analyzer/fp-removal3/test.desc
new file mode 100644
index 00000000000..15541d21c17
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+^Removing function pointers and virtual functions$
+^\s*IF fp == f3 THEN GOTO 1$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal4/main.c b/regression/goto-analyzer/fp-removal4/main.c
new file mode 100644
index 00000000000..dd27759f72d
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal4/main.c
@@ -0,0 +1,30 @@
+void f1 (void) { int tk = 1; }
+void f2 (void) { int tk = 2; }
+void f3 (void) { int tk = 3; }
+void f4 (void) { int tk = 4; }
+void f5 (void) { int tk = 5; }
+void f6 (void) { int tk = 6; }
+void f7 (void) { int tk = 7; }
+void f8 (void) { int tk = 8; }
+void f9 (void) { int tk = 9; }
+
+typedef void(*void_fp)(void);
+
+void_fp fp_tbl[] = {f1, f2 ,f3};
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+void_fp fp_tbl2[] = {f4, f5 ,f6, f7, f8, f9};
+
+void func4()
+{
+  int x = 1;
+  void_fp fp = fp_tbl[x];
+  fp();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func4(i,0);
+   }
+}
diff --git a/regression/goto-analyzer/fp-removal4/test.desc b/regression/goto-analyzer/fp-removal4/test.desc
new file mode 100644
index 00000000000..3c2a6df4338
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+^Removing function pointers and virtual functions$
+^\s*IF fp == f2 THEN GOTO 1$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal5/main.c b/regression/goto-analyzer/fp-removal5/main.c
new file mode 100644
index 00000000000..35b2a889eac
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal5/main.c
@@ -0,0 +1,28 @@
+void f1 (void) { int tk = 1; }
+void f2 (void) { int tk = 2; }
+void f3 (void) { int tk = 3; }
+void f4 (void) { int tk = 4; }
+void f5 (void) { int tk = 5; }
+void f6 (void) { int tk = 6; }
+void f7 (void) { int tk = 7; }
+void f8 (void) { int tk = 8; }
+void f9 (void) { int tk = 9; }
+
+typedef void(*void_fp)(void);
+
+void_fp fp_tbl[] = {f2, f3 ,f4};
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+void_fp fp_tbl2[] = {f1, f5 ,f6, f7, f8, f9};
+
+void func5(int i, int j){
+   void_fp fp = fp_tbl[i];
+   fp();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func5(i,0);
+   }
+}
diff --git a/regression/goto-analyzer/fp-removal5/test.desc b/regression/goto-analyzer/fp-removal5/test.desc
new file mode 100644
index 00000000000..15840e69fe3
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal5/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp == f2 THEN GOTO 1$
+^\s*IF fp == f3 THEN GOTO 2$
+^\s*IF fp == f4 THEN GOTO 3$
+^SIGNAL=0$
+--
+^warning: ignoring

From 63db62f49453d79be024788192a6ec8be11f5aec Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Fri, 13 Jan 2017 12:29:44 +0000
Subject: [PATCH 02/17] Initial implementation of the function pointer
 improvements

This isn't currently working.
---
 .../remove_function_pointers.cpp              | 233 ++++++++++++++++--
 1 file changed, 210 insertions(+), 23 deletions(-)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 7a25def3823..16074135faf 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -80,6 +80,26 @@ class remove_function_pointerst
       compute_address_taken_functions(s.second.value, address_taken);
   }
 
+private:
+  // These represents our best effors to resolve function pointers more
+  // precisely.
+  // If they suceed they return true and the out parameter will be filled in
+  // appropriately. If they fail, they will return false and the out parameter
+  // will be left untouched.
+  typedef std::list<exprt> functionst;
+
+  bool try_get_precise_call(
+    const exprt &expression, exprt &out_function);
+
+  bool try_get_from_address_of(
+    const exprt &expression, functionst &out_functions);
+
+  bool try_get_call_from_symbol(
+    const exprt &symbol_expr, functionst &out_functions);
+
+  bool try_get_call_from_index(
+    const exprt &index_expr, functionst &out_functions);
+
 };
 
 /*******************************************************************\
@@ -138,6 +158,160 @@ symbolt &remove_function_pointerst::new_tmp_symbol()
   return *symbol_ptr;
 }
 
+bool remove_function_pointerst::try_get_precise_call(
+  const exprt &expression,
+  exprt &out_function)
+{
+  if(expression.id()==ID_symbol && expression.type().id()==ID_code)
+  {
+    out_function=to_symbol_expr(expression);
+  }
+  else
+  {
+    return false;
+  }
+}
+
+bool remove_function_pointerst::try_get_from_address_of(
+  const exprt &expression, functionst &out_functions)
+{
+  if(expression.id()==ID_address_of)
+  {
+    address_of_exprt address_of_expr=to_address_of_expr(expression);
+
+    exprt precise_expr;
+    if(try_get_precise_call(address_of_expr.object(), precise_expr))
+    {
+      out_functions.push_back(precise_expr);
+      return true;
+    }
+    else if(try_get_call_from_symbol(address_of_expr.object(), out_functions))
+    {
+      return true;
+    }
+    else
+    {
+      return false;
+    }
+  }
+  else
+  {
+    return false;
+  }
+}
+
+bool remove_function_pointerst::try_get_call_from_symbol(
+  const exprt &symbol_expr, functionst &out_functions)
+{
+  if(symbol_expr.id()==ID_symbol)
+  {
+    const symbolt &symbol=
+      symbol_table.lookup(symbol_expr.get(ID_identifier));
+    exprt looked_up_val=symbol.value;
+    exprt precise_expr;
+    if(try_get_precise_call(looked_up_val, precise_expr))
+    {
+      out_functions.push_back(precise_expr);
+    }
+    else if(try_get_from_address_of(looked_up_val, out_functions))
+    {
+      return true;
+    }
+    else if(try_get_call_from_index(looked_up_val, out_functions))
+    {
+      return true;
+    }
+    else if(try_get_call_from_symbol(looked_up_val, out_functions))
+    {
+      return true;
+    }
+    else
+    {
+      return false;
+    }
+  }
+  else
+  {
+    return false;
+  }
+}
+
+bool remove_function_pointerst::try_get_call_from_index(
+  const exprt &expr, functionst &out_functions)
+{
+  if(expr.id()==ID_index)
+  {
+    index_exprt index_expr=to_index_expr(expr);
+#if 0
+    const exprt &value_expr=index_expr.index();
+    if(value_expr.id()==ID_constant)
+    {
+      // TODO(tkiley): There should be a way of resolving constant indices
+      // to get precisely the right function pointer
+    }
+    else
+#endif
+    {
+      // We don't know what index it is, but we know the value is from the array
+      exprt array_expr=index_expr.array();
+      array_exprt array_val_expr;
+      bool found_array=false;
+      if(array_expr.id()==ID_array)
+      {
+        array_val_expr=to_array_expr(array_expr);
+        found_array=true;
+      }
+      else if(array_expr.id()==ID_symbol)
+      {
+        // Is there some existing code to follow symbols to the real value?
+        const symbolt &array_symbol=
+          symbol_table.lookup(array_expr.get(ID_identifier));
+
+        const exprt &array_value=array_symbol.value;
+        if(array_value.id()==ID_array)
+        {
+          array_val_expr=to_array_expr(array_value);
+          found_array=true;
+        }
+      }
+
+      if(found_array)
+      {
+        for(const exprt &op : array_val_expr.operands())
+        {
+          exprt precise_match;
+          if(try_get_precise_call(op, precise_match))
+          {
+            out_functions.push_back(precise_match);
+          }
+          else if(try_get_from_address_of(op, out_functions))
+          {
+          }
+          else if(try_get_call_from_symbol(op, out_functions))
+          {
+          }
+          else
+          {
+            // return false?
+            // in this case there is an element
+          }
+        }
+
+        return out_functions.size() > 0;
+      }
+      else
+      {
+        return false;
+      }
+    }
+
+  }
+  else
+  {
+    return false;
+  }
+}
+
 /*******************************************************************\
 
 Function: remove_function_pointerst::arg_is_type_compatible
@@ -364,39 +538,52 @@ void remove_function_pointerst::remove_function_pointer(
 
   const exprt &pointer=function.op0();
 
-  // Is this simple?
-  if(pointer.id()==ID_address_of &&
-     to_address_of_expr(pointer).object().id()==ID_symbol)
+  exprt precise_call;
+  functionst functions;
+  if(try_get_precise_call(pointer, precise_call))
   {
-    to_code_function_call(target->code).function()=
-      to_address_of_expr(pointer).object();
+    to_code_function_call(target->code).function()=precise_call;
     return;
   }
+  else if(try_get_from_address_of(pointer, functions))
+  {
 
-  typedef std::list<exprt> functionst;
-  functionst functions;
+  }
+  else if(try_get_call_from_symbol(pointer, functions))
+  {
 
-  bool return_value_used=code.lhs().is_not_nil();
+  }
+  else if(try_get_call_from_index(pointer, functions))
+  {
 
-  // get all type-compatible functions
-  // whose address is ever taken
-  for(const auto &t : type_map)
+  }
+
+  // if the functions list is still empty we didn't have any luck finding
+  // any valid funcitons (or there are none??)
+  if(functions.size()==0)
   {
-    // address taken?
-    if(address_taken.find(t.first)==address_taken.end())
-      continue;
+    bool return_value_used=code.lhs().is_not_nil();
 
-    // type-compatible?
-    if(!is_type_compatible(return_value_used, call_type, t.second))
-      continue;
+    // get all type-compatible functions
+    // whose address is ever taken
+    for(const auto &t : type_map)
+    {
+      // address taken?
+      if(address_taken.find(t.first)==address_taken.end())
+        continue;
 
-    if(t.first=="pthread_mutex_cleanup")
-      continue;
+      // type-compatible?
+      if(!is_type_compatible(return_value_used, call_type, t.second))
+        continue;
 
-    symbol_exprt expr;
-    expr.type()=t.second;
-    expr.set_identifier(t.first);
-    functions.push_back(expr);
+      if(t.first=="pthread_mutex_cleanup")
+        continue;
+
+      symbol_exprt expr;
+      expr.type()=t.second;
+      expr.set_identifier(t.first);
+      functions.push_back(expr);
+    }
   }
 
   // the final target is a skip

From 2967d747bf7b4382e9351b4424a3c3ee4f635219 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Fri, 13 Jan 2017 14:41:14 +0000
Subject: [PATCH 03/17] Tightened test for when only one possible function

---
 regression/goto-analyzer/fp-removal1/test.desc | 2 +-
 regression/goto-analyzer/fp-removal2/test.desc | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/regression/goto-analyzer/fp-removal1/test.desc b/regression/goto-analyzer/fp-removal1/test.desc
index 707afa692b3..c3065239e49 100644
--- a/regression/goto-analyzer/fp-removal1/test.desc
+++ b/regression/goto-analyzer/fp-removal1/test.desc
@@ -3,6 +3,6 @@ main.c
 --show-goto-functions
 
 ^Removing function pointers and virtual functions$
-^\s*IF fp == f2 THEN GOTO 1$
+^\s*f2();
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal2/test.desc b/regression/goto-analyzer/fp-removal2/test.desc
index 690ca1ea037..9ba26c84989 100644
--- a/regression/goto-analyzer/fp-removal2/test.desc
+++ b/regression/goto-analyzer/fp-removal2/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions
 ^Removing function pointers and virtual functions$
-^\s*IF fp2 == f2 THEN GOTO 1$
+^\s*f2();$
 ^SIGNAL=0$
 --
 ^warning: ignoring

From 615eb578cd3690a5ca4be4ef52a4d486a3c2fa48 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Fri, 13 Jan 2017 14:41:33 +0000
Subject: [PATCH 04/17] If there is only only function we replace the call with
 the function directly

---
 src/goto-programs/remove_function_pointers.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 16074135faf..f1464c3a67d 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -558,6 +558,12 @@ void remove_function_pointerst::remove_function_pointer(
 
   }
 
+  if(functions.size()==1)
+  {
+    to_code_function_call(target->code).function()=functions.front();
+    return;
+  }
+
   // if the functions list is still empty we didn't have any luck finding
   // any valid funcitons (or there are none??)
   if(functions.size()==0)

From 6cc765a37fe2e9d9c16835a7e75e45e255feb5a2 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Fri, 13 Jan 2017 15:24:19 +0000
Subject: [PATCH 05/17] Making tests more consistent

---
 regression/goto-analyzer/fp-removal3/main.c    | 6 +++---
 regression/goto-analyzer/fp-removal3/test.desc | 2 +-
 regression/goto-analyzer/fp-removal4/main.c    | 4 ++--
 regression/goto-analyzer/fp-removal4/test.desc | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/regression/goto-analyzer/fp-removal3/main.c b/regression/goto-analyzer/fp-removal3/main.c
index 083846e61ba..2d78703e53d 100644
--- a/regression/goto-analyzer/fp-removal3/main.c
+++ b/regression/goto-analyzer/fp-removal3/main.c
@@ -10,15 +10,15 @@ void f9 (void) { int tk = 9; }
 
 typedef void(*void_fp)(void);
 
-void_fp fp_tbl[] = {f1, f2 ,f3};
+void_fp fp_tbl[] = {f2, f3 ,f4};
 
 // There is a basic check that excludes all functions that aren't used anywhere
 // This ensures that check can't work in this example
-void_fp fp_tbl2[] = {f4, f5 ,f6, f7, f8, f9};
+void_fp fp_tbl2[] = {f1, f5 ,f6, f7, f8, f9};
 
 void func3()
 {
-  void_fp fp = fp_tbl[2];
+  void_fp fp = fp_tbl[1];
   fp();
 }
 
diff --git a/regression/goto-analyzer/fp-removal3/test.desc b/regression/goto-analyzer/fp-removal3/test.desc
index 15541d21c17..a36fb208c69 100644
--- a/regression/goto-analyzer/fp-removal3/test.desc
+++ b/regression/goto-analyzer/fp-removal3/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions
 ^Removing function pointers and virtual functions$
-^\s*IF fp == f3 THEN GOTO 1$
+^\s*f3();$
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal4/main.c b/regression/goto-analyzer/fp-removal4/main.c
index dd27759f72d..56a3150c4dd 100644
--- a/regression/goto-analyzer/fp-removal4/main.c
+++ b/regression/goto-analyzer/fp-removal4/main.c
@@ -10,11 +10,11 @@ void f9 (void) { int tk = 9; }
 
 typedef void(*void_fp)(void);
 
-void_fp fp_tbl[] = {f1, f2 ,f3};
+void_fp fp_tbl[] = {f2, f3 ,f4};
 
 // There is a basic check that excludes all functions that aren't used anywhere
 // This ensures that check can't work in this example
-void_fp fp_tbl2[] = {f4, f5 ,f6, f7, f8, f9};
+void_fp fp_tbl2[] = {f1, f5 ,f6, f7, f8, f9};
 
 void func4()
 {
diff --git a/regression/goto-analyzer/fp-removal4/test.desc b/regression/goto-analyzer/fp-removal4/test.desc
index 3c2a6df4338..a36fb208c69 100644
--- a/regression/goto-analyzer/fp-removal4/test.desc
+++ b/regression/goto-analyzer/fp-removal4/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions
 ^Removing function pointers and virtual functions$
-^\s*IF fp == f2 THEN GOTO 1$
+^\s*f3();$
 ^SIGNAL=0$
 --
 ^warning: ignoring

From 830244dc7e7962092c95a7ca9c1e090f81d7d1d7 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Fri, 13 Jan 2017 15:25:59 +0000
Subject: [PATCH 06/17] Support for resolving constant indices

If the function pointer comes from an array and the index is constant,
then we can get the actual function call.
---
 .../remove_function_pointers.cpp              | 128 +++++++++++++-----
 1 file changed, 94 insertions(+), 34 deletions(-)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index f1464c3a67d..e0648e9a119 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 
+#include <util/arith_tools.h>
 #include <util/replace_expr.h>
 #include <util/expr_util.h>
 #include <util/source_location.h>
@@ -100,6 +101,12 @@ class remove_function_pointerst
   bool try_get_call_from_index(
     const exprt &index_expr, functionst &out_functions);
 
+  bool try_evaluate_index_value(
+    const exprt &index_value_expr, mp_integer &out_array_index);
+
+  bool try_get_array_from_index(
+    const index_exprt &index_expr, array_exprt &out_array_expr);
+
 };
 
 /*******************************************************************\
@@ -242,42 +249,34 @@ bool remove_function_pointerst::try_get_call_from_index(
   if(expr.id()==ID_index)
   {
     index_exprt index_expr=to_index_expr(expr);
-#if 0
-    const exprt &value_expr=index_expr.index();
-    if(value_expr.id()==ID_constant)
-    {
-      // TODO(tkiley): There should be a way of resolving constant indices
-      // to get precisely the right function pointer
-    }
-    else
-#endif
+
+    array_exprt array_expr;
+    if(try_get_array_from_index(index_expr, array_expr))
     {
-      // We don't know what index it is, but we know the value is from the array
-      exprt array_expr=index_expr.array();
-      array_exprt array_val_expr;
-      bool found_array=false;
-      if(array_expr.id()==ID_array)
-      {
-        array_val_expr=to_array_expr(array_expr);
-        found_array=true;
-      }
-      else if(array_expr.id()==ID_symbol)
+      mp_integer value;
+      if(try_evaluate_index_value(index_expr.index(), value))
       {
-        // Is there some existing code to follow symbols to the real value?
-        const symbolt &array_symbol=
-          symbol_table.lookup(array_expr.get(ID_identifier));
-
-        const exprt &array_value=array_symbol.value;
-        if(array_value.id()==ID_array)
+        const exprt &func_expr=array_expr.operands()[integer2size_t(value)];
+        exprt precise_match;
+        if(try_get_precise_call(func_expr, precise_match))
+        {
+          out_functions.push_back(precise_match);
+        }
+        else if(try_get_from_address_of(func_expr, out_functions))
+        {
+        }
+        else if(try_get_call_from_symbol(func_expr, out_functions))
+        {
+        }
+        else
         {
-          array_val_expr=to_array_expr(array_value);
-          found_array=true;
+          return false;
         }
       }
-
-      if(found_array)
+      else
       {
-        for(const exprt &op : array_val_expr.operands())
+        // We don't know what index it is, but we know the value is from the array
+        for(const exprt &op : array_expr.operands())
         {
           exprt precise_match;
           if(try_get_precise_call(op, precise_match))
@@ -299,12 +298,73 @@ bool remove_function_pointerst::try_get_call_from_index(
 
         return out_functions.size() > 0;
       }
-      else
-      {
-        return false;
-      }
     }
+  }
+  else
+  {
+    return false;
+  }
+}
+
+bool remove_function_pointerst::try_evaluate_index_value(
+  const exprt &index_value_expr, mp_integer &out_array_index)
+{
+  if(index_value_expr.id()==ID_constant)
+  {
+    constant_exprt constant_expr=to_constant_expr(index_value_expr);
+    mp_integer array_index;
+    bool errors=to_integer(constant_expr, array_index);
+    if(!errors)
+    {
+      out_array_index=array_index;
+    }
+    return !errors;
+  }
+  else if(index_value_expr.id()==ID_symbol)
+  {
+    // Resolve symbol and try again
+    const symbolt &index_symbol=
+      symbol_table.lookup(index_value_expr.get(ID_identifier));
+
+    return try_evaluate_index_value(index_symbol.value, out_array_index);
+  }
+  else if(index_value_expr.id()==ID_typecast)
+  {
+    // Follow the typecast
+
+    return try_evaluate_index_value(index_value_expr.op0(), out_array_index);
+  }
+  else
+  {
+    return false;
+  }
+}
+
+bool remove_function_pointerst::try_get_array_from_index(
+  const index_exprt &index_expr, array_exprt &out_array_expr)
+{
+  exprt array_expr=index_expr.array();
+  if(array_expr.id()==ID_array)
+  {
+    out_array_expr=to_array_expr(array_expr);
+    return true;
+  }
+  else if(array_expr.id()==ID_symbol)
+  {
+    // Is there some existing code to follow symbols to the real value?
+    const symbolt &array_symbol=
+      symbol_table.lookup(array_expr.get(ID_identifier));
 
+    const exprt &array_value=array_symbol.value;
+    if(array_value.id()==ID_array)
+    {
+      out_array_expr=to_array_expr(array_value);
+      return true;
+    }
+    else
+    {
+      return false;
+    }
   }
   else
   {

From 0c3645b0510463b9c29efd1039bdd79c806e37f4 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Fri, 13 Jan 2017 18:08:25 +0000
Subject: [PATCH 07/17] Adding function comments

---
 .../remove_function_pointers.cpp              | 129 ++++++++++++++++--
 1 file changed, 114 insertions(+), 15 deletions(-)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index e0648e9a119..fed3fc84098 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -82,18 +82,13 @@ class remove_function_pointerst
   }
 
 private:
-  // These represents our best effors to resolve function pointers more
-  // precisely.
-  // If they suceed they return true and the out parameter will be filled in
-  // appropriately. If they fail, they will return false and the out parameter
-  // will be left untouched.
   typedef std::list<exprt> functionst;
 
   bool try_get_precise_call(
-    const exprt &expression, exprt &out_function);
+    const exprt &expr, exprt &out_function);
 
   bool try_get_from_address_of(
-    const exprt &expression, functionst &out_functions);
+    const exprt &expr, functionst &out_functions);
 
   bool try_get_call_from_symbol(
     const exprt &symbol_expr, functionst &out_functions);
@@ -165,13 +160,28 @@ symbolt &remove_function_pointerst::new_tmp_symbol()
   return *symbol_ptr;
 }
 
+/*******************************************************************\
+
+Function: remove_function_pointerst::try_get_precise_call
+
+  Inputs:
+   expr - The expression that is the value of the function pointer.
+
+ Outputs: Returns true if the expression is a symbol and its value was code.
+          In this case out_function will be the function this is a symbol for.
+
+ Purpose: Find if a symbol is in fact a function that can be used in place
+          of the function pointer
+
+\*******************************************************************/
+
 bool remove_function_pointerst::try_get_precise_call(
-  const exprt &expression,
+  const exprt &expr,
   exprt &out_function)
 {
-  if(expression.id()==ID_symbol && expression.type().id()==ID_code)
+  if(expr.id()==ID_symbol && expr.type().id()==ID_code)
   {
-    out_function=to_symbol_expr(expression);
+    out_function=to_symbol_expr(expr);
   }
   else
   {
@@ -179,12 +189,28 @@ bool remove_function_pointerst::try_get_precise_call(
   }
 }
 
+/*******************************************************************\
+
+Function: remove_function_pointerst::try_get_from_address_of
+
+  Inputs:
+   expr - The expression that is the value of the function pointer.
+
+ Outputs: Returns true if the expression is a address_of_exprt and it was able
+          to either pointing to a function or a sybmol. In either of
+          the true cases the out_functions will contain all the functions the
+          address of could be.
+
+ Purpose: Resolve a address of to its real value.
+
+\*******************************************************************/
+
 bool remove_function_pointerst::try_get_from_address_of(
-  const exprt &expression, functionst &out_functions)
+  const exprt &expr, functionst &out_functions)
 {
-  if(expression.id()==ID_address_of)
+  if(expr.id()==ID_address_of)
   {
-    address_of_exprt address_of_expr=to_address_of_expr(expression);
+    address_of_exprt address_of_expr=to_address_of_expr(expr);
 
     exprt precise_expr;
     if(try_get_precise_call(address_of_expr.object(), precise_expr))
@@ -207,6 +233,25 @@ bool remove_function_pointerst::try_get_from_address_of(
   }
 }
 
+/*******************************************************************\
+
+Function: remove_function_pointerst::try_get_call_from_symbol
+
+  Inputs:
+   symbol_expr - The expression that is the value of the function pointer.
+
+ Outputs: Returns true if the expression is a symbol_exprt and it was able
+          to either find a explict function that this points to (in the case
+          where the symbol is a function) or all a set of functions that it
+          could be by following the valu the symbol represents. In either of
+          the true cases the out_functions will contain all the functions the
+          function pointer could point to.
+
+ Purpose: Resolve a symbol to its real value and recursively try and find
+          all posible functions that could be at that position in the array.
+
+\*******************************************************************/
+
 bool remove_function_pointerst::try_get_call_from_symbol(
   const exprt &symbol_expr, functionst &out_functions)
 {
@@ -243,6 +288,25 @@ bool remove_function_pointerst::try_get_call_from_symbol(
   }
 }
 
+/*******************************************************************\
+
+Function: remove_function_pointerst::try_get_call_from_index
+
+  Inputs:
+   expr - The expression that is the value of the function pointer.
+
+ Outputs: Returns true if the expression is a index_exprt and it was able
+          to either find a explict function that this points to (in the case
+          where the index is constant) or all the functions within the array
+          that the index is indexing. In either of the true cases the
+          out_functions will contain all the functions the function pointer
+          could point to.
+
+ Purpose: Resolve the index of an array to find all posible functions
+          that could be at that position in the array.
+
+\*******************************************************************/
+
 bool remove_function_pointerst::try_get_call_from_index(
   const exprt &expr, functionst &out_functions)
 {
@@ -275,7 +339,8 @@ bool remove_function_pointerst::try_get_call_from_index(
       }
       else
       {
-        // We don't know what index it is, but we know the value is from the array
+        // We don't know what index it is,
+        // but we know the value is from the array
         for(const exprt &op : array_expr.operands())
         {
           exprt precise_match;
@@ -295,7 +360,6 @@ bool remove_function_pointerst::try_get_call_from_index(
             // in this case there is an element
           }
         }
-
         return out_functions.size() > 0;
       }
     }
@@ -306,6 +370,24 @@ bool remove_function_pointerst::try_get_call_from_index(
   }
 }
 
+/*******************************************************************\
+
+Function: remove_function_pointerst::try_evaluate_index_value
+
+  Inputs:
+   index_expr - The expression of the index of the index expression (e.g.
+                index_exprt::index())
+
+ Outputs: Returns true if was able to find a constant value for the index
+          expression. If true, then out_array_index will be the index within
+          the array that the function pointer is pointing to.
+
+ Purpose: Given an index into an array, resolve, if possible, the index
+          that is being accessed. This deals with symbols and typecasts to
+          constant values.
+
+\*******************************************************************/
+
 bool remove_function_pointerst::try_evaluate_index_value(
   const exprt &index_value_expr, mp_integer &out_array_index)
 {
@@ -340,6 +422,23 @@ bool remove_function_pointerst::try_evaluate_index_value(
   }
 }
 
+/*******************************************************************\
+
+Function: remove_function_pointerst::try_get_array_from_index
+
+  Inputs:
+   index_expr - The expression of the index in the array
+
+ Outputs: Returns true if was able to find the array associated
+          with the index. If true, then out_array_expr will contain
+          the expression representing the array.
+
+ Purpose: Given an index into an array, resolve the array expression,
+          following symbol expressions through to the actual array
+          expression.
+
+\*******************************************************************/
+
 bool remove_function_pointerst::try_get_array_from_index(
   const index_exprt &index_expr, array_exprt &out_array_expr)
 {

From fd61477fc04eaedf823a367effe42fb7ee181313 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Thu, 19 Jan 2017 10:02:04 +0000
Subject: [PATCH 08/17] Made the tests more consistent and correct

Added const to arrays that aren't modified which will then be used to
determine arrays whose contents can be known.
---
 regression/goto-analyzer/fp-removal1/main.c | 28 +++++++++----------
 regression/goto-analyzer/fp-removal2/main.c | 31 +++++++++++----------
 regression/goto-analyzer/fp-removal3/main.c | 30 ++++++++++----------
 regression/goto-analyzer/fp-removal4/main.c | 30 ++++++++++----------
 regression/goto-analyzer/fp-removal5/main.c |  8 +++---
 5 files changed, 64 insertions(+), 63 deletions(-)

diff --git a/regression/goto-analyzer/fp-removal1/main.c b/regression/goto-analyzer/fp-removal1/main.c
index ec7927f5dba..f0d8118dfc8 100644
--- a/regression/goto-analyzer/fp-removal1/main.c
+++ b/regression/goto-analyzer/fp-removal1/main.c
@@ -1,27 +1,27 @@
-void f1 (void) { int tk = 1; }
-void f2 (void) { int tk = 2; }
-void f3 (void) { int tk = 3; }
-void f4 (void) { int tk = 4; }
-void f5 (void) { int tk = 5; }
-void f6 (void) { int tk = 6; }
-void f7 (void) { int tk = 7; }
-void f8 (void) { int tk = 8; }
-void f9 (void) { int tk = 9; }
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
 
 typedef void(*void_fp)(void);
 
 // There is a basic check that excludes all functions that aren't used anywhere
 // This ensures that check can't work in this example
-void_fp fp_tbl[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
 
-void func1()
+void func()
 {
   void_fp fp = f2;
   fp();
 }
 
 void main(){
-   for(int i=0;i<3;i++){
-     func1(i,0);
-   }
+  func();
 }
diff --git a/regression/goto-analyzer/fp-removal2/main.c b/regression/goto-analyzer/fp-removal2/main.c
index 32600d7841d..5f44200511c 100644
--- a/regression/goto-analyzer/fp-removal2/main.c
+++ b/regression/goto-analyzer/fp-removal2/main.c
@@ -1,28 +1,29 @@
-void f1 (void) { int tk = 1; }
-void f2 (void) { int tk = 2; }
-void f3 (void) { int tk = 3; }
-void f4 (void) { int tk = 4; }
-void f5 (void) { int tk = 5; }
-void f6 (void) { int tk = 6; }
-void f7 (void) { int tk = 7; }
-void f8 (void) { int tk = 8; }
-void f9 (void) { int tk = 9; }
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
 
 typedef void(*void_fp)(void);
 
 // There is a basic check that excludes all functions that aren't used anywhere
 // This ensures that check can't work in this example
-void_fp fp_tbl[] = {f1, f2, f3, f4, f5 ,f6, f7, f8, f9};
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
 
-void func2()
+void func()
 {
   void_fp fp = f2;
   void_fp fp2 = fp;
   fp2();
 }
 
-void main(){
-   for(int i=0;i<3;i++){
-     func2(i,0);
-   }
+void main()
+{
+  func();
 }
diff --git a/regression/goto-analyzer/fp-removal3/main.c b/regression/goto-analyzer/fp-removal3/main.c
index 2d78703e53d..d822ace2460 100644
--- a/regression/goto-analyzer/fp-removal3/main.c
+++ b/regression/goto-analyzer/fp-removal3/main.c
@@ -1,29 +1,29 @@
-void f1 (void) { int tk = 1; }
-void f2 (void) { int tk = 2; }
-void f3 (void) { int tk = 3; }
-void f4 (void) { int tk = 4; }
-void f5 (void) { int tk = 5; }
-void f6 (void) { int tk = 6; }
-void f7 (void) { int tk = 7; }
-void f8 (void) { int tk = 8; }
-void f9 (void) { int tk = 9; }
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
 
 typedef void(*void_fp)(void);
 
-void_fp fp_tbl[] = {f2, f3 ,f4};
+const void_fp fp_tbl[] = {f2, f3 ,f4};
 
 // There is a basic check that excludes all functions that aren't used anywhere
 // This ensures that check can't work in this example
-void_fp fp_tbl2[] = {f1, f5 ,f6, f7, f8, f9};
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
 
-void func3()
+void func()
 {
   void_fp fp = fp_tbl[1];
   fp();
 }
 
 void main(){
-   for(int i=0;i<3;i++){
-     func3(i,0);
-   }
+  func();
 }
diff --git a/regression/goto-analyzer/fp-removal4/main.c b/regression/goto-analyzer/fp-removal4/main.c
index 56a3150c4dd..d858ea7372a 100644
--- a/regression/goto-analyzer/fp-removal4/main.c
+++ b/regression/goto-analyzer/fp-removal4/main.c
@@ -1,22 +1,24 @@
-void f1 (void) { int tk = 1; }
-void f2 (void) { int tk = 2; }
-void f3 (void) { int tk = 3; }
-void f4 (void) { int tk = 4; }
-void f5 (void) { int tk = 5; }
-void f6 (void) { int tk = 6; }
-void f7 (void) { int tk = 7; }
-void f8 (void) { int tk = 8; }
-void f9 (void) { int tk = 9; }
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
 
 typedef void(*void_fp)(void);
 
-void_fp fp_tbl[] = {f2, f3 ,f4};
+const void_fp fp_tbl[] = {f2, f3 ,f4};
 
 // There is a basic check that excludes all functions that aren't used anywhere
 // This ensures that check can't work in this example
-void_fp fp_tbl2[] = {f1, f5 ,f6, f7, f8, f9};
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
 
-void func4()
+void func()
 {
   int x = 1;
   void_fp fp = fp_tbl[x];
@@ -24,7 +26,5 @@ void func4()
 }
 
 void main(){
-   for(int i=0;i<3;i++){
-     func4(i,0);
-   }
+  func();
 }
diff --git a/regression/goto-analyzer/fp-removal5/main.c b/regression/goto-analyzer/fp-removal5/main.c
index 35b2a889eac..b97343152ab 100644
--- a/regression/goto-analyzer/fp-removal5/main.c
+++ b/regression/goto-analyzer/fp-removal5/main.c
@@ -10,19 +10,19 @@ void f9 (void) { int tk = 9; }
 
 typedef void(*void_fp)(void);
 
-void_fp fp_tbl[] = {f2, f3 ,f4};
+const void_fp fp_tbl[] = {f2, f3 ,f4};
 
 // There is a basic check that excludes all functions that aren't used anywhere
 // This ensures that check can't work in this example
-void_fp fp_tbl2[] = {f1, f5 ,f6, f7, f8, f9};
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
 
-void func5(int i, int j){
+void func(int i){
    void_fp fp = fp_tbl[i];
    fp();
 }
 
 void main(){
    for(int i=0;i<3;i++){
-     func5(i,0);
+     func(i);
    }
 }

From 7e4b3ff5c6ec6903b3c36041c81cbcbaaf86cad2 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Thu, 19 Jan 2017 17:53:40 +0000
Subject: [PATCH 09/17] Check the array is of constant pointers

We require the array to be of constant pointers so we know they haven't
been reassigned. Also fixed some missing return statements.
---
 .../remove_function_pointers.cpp              | 84 ++++++++++++-------
 1 file changed, 54 insertions(+), 30 deletions(-)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index fed3fc84098..620c72c7368 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/type_eq.h>
 
 #include <ansi-c/c_types.h>
+#include <ansi-c/c_qualifiers.h>
 
 #include "remove_skip.h"
 #include "remove_function_pointers.h"
@@ -182,6 +183,7 @@ bool remove_function_pointerst::try_get_precise_call(
   if(expr.id()==ID_symbol && expr.type().id()==ID_code)
   {
     out_function=to_symbol_expr(expr);
+    return true;
   }
   else
   {
@@ -264,6 +266,7 @@ bool remove_function_pointerst::try_get_call_from_symbol(
     if(try_get_precise_call(looked_up_val, precise_expr))
     {
       out_functions.push_back(precise_expr);
+      return true;
     }
     else if(try_get_from_address_of(looked_up_val, out_functions))
     {
@@ -317,51 +320,72 @@ bool remove_function_pointerst::try_get_call_from_index(
     array_exprt array_expr;
     if(try_get_array_from_index(index_expr, array_expr))
     {
-      mp_integer value;
-      if(try_evaluate_index_value(index_expr.index(), value))
-      {
-        const exprt &func_expr=array_expr.operands()[integer2size_t(value)];
-        exprt precise_match;
-        if(try_get_precise_call(func_expr, precise_match))
-        {
-          out_functions.push_back(precise_match);
-        }
-        else if(try_get_from_address_of(func_expr, out_functions))
-        {
-        }
-        else if(try_get_call_from_symbol(func_expr, out_functions))
-        {
-        }
-        else
-        {
-          return false;
-        }
-      }
-      else
+      // Here we require an array of constant pointers to
+      // code (i.e. the pointers cannot be reassigned).
+      // Since it is an array
+      const typet &array_type=array_expr.type();
+      const typet &array_contents_type=array_type.subtype();
+      c_qualifierst array_qaulifiers;
+      array_qaulifiers.read(array_contents_type);
+      if(array_qaulifiers.is_constant)
       {
-        // We don't know what index it is,
-        // but we know the value is from the array
-        for(const exprt &op : array_expr.operands())
+        mp_integer value;
+        if(try_evaluate_index_value(index_expr.index(), value))
         {
+          const exprt &func_expr=array_expr.operands()[integer2size_t(value)];
           exprt precise_match;
-          if(try_get_precise_call(op, precise_match))
+          if(try_get_precise_call(func_expr, precise_match))
           {
             out_functions.push_back(precise_match);
+            return true;
           }
-          else if(try_get_from_address_of(op, out_functions))
+          else if(try_get_from_address_of(func_expr, out_functions))
           {
+            return true;
           }
-          else if(try_get_call_from_symbol(op, out_functions))
+          else if(try_get_call_from_symbol(func_expr, out_functions))
           {
+            return true;
           }
           else
           {
-            // return false?
-            // in this case there is an element
+            return false;
           }
         }
-        return out_functions.size() > 0;
+        else
+        {
+          // We don't know what index it is,
+          // but we know the value is from the array
+          for(const exprt &op : array_expr.operands())
+          {
+            exprt precise_match;
+            if(try_get_precise_call(op, precise_match))
+            {
+              out_functions.push_back(precise_match);
+            }
+            else if(try_get_from_address_of(op, out_functions))
+            {
+            }
+            else if(try_get_call_from_symbol(op, out_functions))
+            {
+            }
+            else
+            {
+              // return false?
+              // in this case there is an element
+            }
+          }
+          return out_functions.size() > 0;
+        }
       }
+      else
+      {
+        return false;
+      }
+    }
+    else
+    {
+      return false;
     }
   }
   else

From 17839b1e1962e4fd45abc6646f6081745edd290c Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Thu, 19 Jan 2017 18:00:58 +0000
Subject: [PATCH 10/17] Extra tests for cases where we can't determine the
 valid functions

Specifically we test arrays that are not constant and are in fact
modified.
---
 regression/goto-analyzer/fp-removal10/main.c  | 31 +++++++++++++++++
 .../goto-analyzer/fp-removal10/test.desc      | 17 ++++++++++
 regression/goto-analyzer/fp-removal6/main.c   | 27 +++++++++++++++
 .../goto-analyzer/fp-removal6/test.desc       | 17 ++++++++++
 regression/goto-analyzer/fp-removal7/main.c   | 25 ++++++++++++++
 .../goto-analyzer/fp-removal7/test.desc       | 17 ++++++++++
 regression/goto-analyzer/fp-removal8/main.c   | 33 +++++++++++++++++++
 .../goto-analyzer/fp-removal8/test.desc       | 17 ++++++++++
 regression/goto-analyzer/fp-removal9/main.c   | 31 +++++++++++++++++
 .../goto-analyzer/fp-removal9/test.desc       | 17 ++++++++++
 10 files changed, 232 insertions(+)
 create mode 100644 regression/goto-analyzer/fp-removal10/main.c
 create mode 100644 regression/goto-analyzer/fp-removal10/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal6/main.c
 create mode 100644 regression/goto-analyzer/fp-removal6/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal7/main.c
 create mode 100644 regression/goto-analyzer/fp-removal7/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal8/main.c
 create mode 100644 regression/goto-analyzer/fp-removal8/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal9/main.c
 create mode 100644 regression/goto-analyzer/fp-removal9/test.desc

diff --git a/regression/goto-analyzer/fp-removal10/main.c b/regression/goto-analyzer/fp-removal10/main.c
new file mode 100644
index 00000000000..c365700a1fe
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal10/main.c
@@ -0,0 +1,31 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+void_fp fp_tbl[] = {f2, f3, f4};
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(void_fp fp, int i){
+  fp_tbl[2] = fp;
+  void_fp fp2 = fp_tbl[2];
+  fp2();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func(fp_all[i+3], i);
+   }
+}
diff --git a/regression/goto-analyzer/fp-removal10/test.desc b/regression/goto-analyzer/fp-removal10/test.desc
new file mode 100644
index 00000000000..7f4fb53760e
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal10/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp2 == f1 THEN GOTO 1$
+^\s*IF fp2 == f2 THEN GOTO 2$
+^\s*IF fp2 == f3 THEN GOTO 3$
+^\s*IF fp2 == f4 THEN GOTO 4$
+^\s*IF fp2 == f5 THEN GOTO 5$
+^\s*IF fp2 == f6 THEN GOTO 6$
+^\s*IF fp2 == f7 THEN GOTO 7$
+^\s*IF fp2 == f8 THEN GOTO 8$
+^\s*IF fp2 == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal6/main.c b/regression/goto-analyzer/fp-removal6/main.c
new file mode 100644
index 00000000000..9825da61479
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal6/main.c
@@ -0,0 +1,27 @@
+void f1 (void) { int tk = 1; }
+void f2 (void) { int tk = 2; }
+void f3 (void) { int tk = 3; }
+void f4 (void) { int tk = 4; }
+void f5 (void) { int tk = 5; }
+void f6 (void) { int tk = 6; }
+void f7 (void) { int tk = 7; }
+void f8 (void) { int tk = 8; }
+void f9 (void) { int tk = 9; }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(int i, int j){
+  void_fp fp_tbl[] = {fp_all[i*2], fp_all[j+1]};
+   void_fp fp = fp_tbl[1];
+   fp();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func(i,0);
+   }
+}
diff --git a/regression/goto-analyzer/fp-removal6/test.desc b/regression/goto-analyzer/fp-removal6/test.desc
new file mode 100644
index 00000000000..3c735d48a55
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal6/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp == f1 THEN GOTO 1$
+^\s*IF fp == f2 THEN GOTO 2$
+^\s*IF fp == f3 THEN GOTO 3$
+^\s*IF fp == f4 THEN GOTO 4$
+^\s*IF fp == f5 THEN GOTO 5$
+^\s*IF fp == f6 THEN GOTO 6$
+^\s*IF fp == f7 THEN GOTO 7$
+^\s*IF fp == f8 THEN GOTO 8$
+^\s*IF fp == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal7/main.c b/regression/goto-analyzer/fp-removal7/main.c
new file mode 100644
index 00000000000..8bbd6ee15d6
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal7/main.c
@@ -0,0 +1,25 @@
+void f1 (void) { int tk = 1; }
+void f2 (void) { int tk = 2; }
+void f3 (void) { int tk = 3; }
+void f4 (void) { int tk = 4; }
+void f5 (void) { int tk = 5; }
+void f6 (void) { int tk = 6; }
+void f7 (void) { int tk = 7; }
+void f8 (void) { int tk = 8; }
+void f9 (void) { int tk = 9; }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(void_fp fp){
+   fp();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func(fp_all[i]);
+   }
+}
diff --git a/regression/goto-analyzer/fp-removal7/test.desc b/regression/goto-analyzer/fp-removal7/test.desc
new file mode 100644
index 00000000000..3c735d48a55
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal7/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp == f1 THEN GOTO 1$
+^\s*IF fp == f2 THEN GOTO 2$
+^\s*IF fp == f3 THEN GOTO 3$
+^\s*IF fp == f4 THEN GOTO 4$
+^\s*IF fp == f5 THEN GOTO 5$
+^\s*IF fp == f6 THEN GOTO 6$
+^\s*IF fp == f7 THEN GOTO 7$
+^\s*IF fp == f8 THEN GOTO 8$
+^\s*IF fp == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal8/main.c b/regression/goto-analyzer/fp-removal8/main.c
new file mode 100644
index 00000000000..74c0b4f4070
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal8/main.c
@@ -0,0 +1,33 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+void_fp fp_tbl[] = {f2, f3, f4};
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(void_fp fp, int i){
+  // It is concievable this could be checked and seen the first value
+  // of the array is unchanged but is kind of a weird edge case.
+  fp_tbl[2] = fp;
+  void_fp fp2 = fp_tbl[1];
+  fp2();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func(fp_all[i+3], i);
+   }
+}
diff --git a/regression/goto-analyzer/fp-removal8/test.desc b/regression/goto-analyzer/fp-removal8/test.desc
new file mode 100644
index 00000000000..7f4fb53760e
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal8/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp2 == f1 THEN GOTO 1$
+^\s*IF fp2 == f2 THEN GOTO 2$
+^\s*IF fp2 == f3 THEN GOTO 3$
+^\s*IF fp2 == f4 THEN GOTO 4$
+^\s*IF fp2 == f5 THEN GOTO 5$
+^\s*IF fp2 == f6 THEN GOTO 6$
+^\s*IF fp2 == f7 THEN GOTO 7$
+^\s*IF fp2 == f8 THEN GOTO 8$
+^\s*IF fp2 == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal9/main.c b/regression/goto-analyzer/fp-removal9/main.c
new file mode 100644
index 00000000000..c365700a1fe
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal9/main.c
@@ -0,0 +1,31 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+void_fp fp_tbl[] = {f2, f3, f4};
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(void_fp fp, int i){
+  fp_tbl[2] = fp;
+  void_fp fp2 = fp_tbl[2];
+  fp2();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func(fp_all[i+3], i);
+   }
+}
diff --git a/regression/goto-analyzer/fp-removal9/test.desc b/regression/goto-analyzer/fp-removal9/test.desc
new file mode 100644
index 00000000000..7f4fb53760e
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal9/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp2 == f1 THEN GOTO 1$
+^\s*IF fp2 == f2 THEN GOTO 2$
+^\s*IF fp2 == f3 THEN GOTO 3$
+^\s*IF fp2 == f4 THEN GOTO 4$
+^\s*IF fp2 == f5 THEN GOTO 5$
+^\s*IF fp2 == f6 THEN GOTO 6$
+^\s*IF fp2 == f7 THEN GOTO 7$
+^\s*IF fp2 == f8 THEN GOTO 8$
+^\s*IF fp2 == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring

From 61de27a8689e37fe82e0f369e4c77f1b71e008b9 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Thu, 19 Jan 2017 18:10:23 +0000
Subject: [PATCH 11/17] Using const references where appropriate

---
 src/goto-programs/remove_function_pointers.cpp | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 620c72c7368..1ebcfb19269 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -212,7 +212,7 @@ bool remove_function_pointerst::try_get_from_address_of(
 {
   if(expr.id()==ID_address_of)
   {
-    address_of_exprt address_of_expr=to_address_of_expr(expr);
+    const address_of_exprt &address_of_expr=to_address_of_expr(expr);
 
     exprt precise_expr;
     if(try_get_precise_call(address_of_expr.object(), precise_expr))
@@ -261,7 +261,7 @@ bool remove_function_pointerst::try_get_call_from_symbol(
   {
     const symbolt &symbol=
       symbol_table.lookup(symbol_expr.get(ID_identifier));
-    exprt looked_up_val=symbol.value;
+    const exprt &looked_up_val=symbol.value;
     exprt precise_expr;
     if(try_get_precise_call(looked_up_val, precise_expr))
     {
@@ -315,7 +315,7 @@ bool remove_function_pointerst::try_get_call_from_index(
 {
   if(expr.id()==ID_index)
   {
-    index_exprt index_expr=to_index_expr(expr);
+    const index_exprt &index_expr=to_index_expr(expr);
 
     array_exprt array_expr;
     if(try_get_array_from_index(index_expr, array_expr))
@@ -417,7 +417,7 @@ bool remove_function_pointerst::try_evaluate_index_value(
 {
   if(index_value_expr.id()==ID_constant)
   {
-    constant_exprt constant_expr=to_constant_expr(index_value_expr);
+    const constant_exprt &constant_expr=to_constant_expr(index_value_expr);
     mp_integer array_index;
     bool errors=to_integer(constant_expr, array_index);
     if(!errors)
@@ -466,7 +466,7 @@ Function: remove_function_pointerst::try_get_array_from_index
 bool remove_function_pointerst::try_get_array_from_index(
   const index_exprt &index_expr, array_exprt &out_array_expr)
 {
-  exprt array_expr=index_expr.array();
+  const exprt &array_expr=index_expr.array();
   if(array_expr.id()==ID_array)
   {
     out_array_expr=to_array_expr(array_expr);

From a032cbb49b574b503a9086594ada5977b888e630 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Thu, 19 Jan 2017 18:24:30 +0000
Subject: [PATCH 12/17] Tidied up nested if/else if structure

Before there was a load of empty if/else if/else clauses to chain the
calls to the different try_* methods so they don't get called if an
earlier one has succeeded. Replaced this with a cleaner approach using
short circuiting and a boolean variable to track if we've succeeded thus
far.
---
 .../remove_function_pointers.cpp              | 89 +++++++------------
 1 file changed, 31 insertions(+), 58 deletions(-)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 1ebcfb19269..9de2ff286c8 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -220,13 +220,9 @@ bool remove_function_pointerst::try_get_from_address_of(
       out_functions.push_back(precise_expr);
       return true;
     }
-    else if(try_get_call_from_symbol(address_of_expr.object(), out_functions))
-    {
-      return true;
-    }
     else
     {
-      return false;
+      return try_get_call_from_symbol(address_of_expr.object(), out_functions);
     }
   }
   else
@@ -268,22 +264,14 @@ bool remove_function_pointerst::try_get_call_from_symbol(
       out_functions.push_back(precise_expr);
       return true;
     }
-    else if(try_get_from_address_of(looked_up_val, out_functions))
-    {
-      return true;
-    }
-    else if(try_get_call_from_index(looked_up_val, out_functions))
-    {
-      return true;
-    }
-    else if(try_get_call_from_symbol(looked_up_val, out_functions))
-    {
-      return true;
-    }
-    else
-    {
-      return false;
-    }
+    bool found_functions=false;
+    found_functions=
+      found_functions||try_get_from_address_of(looked_up_val, out_functions);
+    found_functions=
+      found_functions||try_get_call_from_index(looked_up_val, out_functions);
+    found_functions=
+      found_functions||try_get_call_from_symbol(looked_up_val, out_functions);
+    return found_functions;
   }
   else
   {
@@ -334,23 +322,19 @@ bool remove_function_pointerst::try_get_call_from_index(
         {
           const exprt &func_expr=array_expr.operands()[integer2size_t(value)];
           exprt precise_match;
+
           if(try_get_precise_call(func_expr, precise_match))
           {
             out_functions.push_back(precise_match);
             return true;
           }
-          else if(try_get_from_address_of(func_expr, out_functions))
-          {
-            return true;
-          }
-          else if(try_get_call_from_symbol(func_expr, out_functions))
-          {
-            return true;
-          }
-          else
-          {
-            return false;
-          }
+          bool found_functions=false;
+          found_functions=
+            found_functions||try_get_from_address_of(func_expr, out_functions);
+          found_functions=
+            found_functions||try_get_call_from_symbol(func_expr, out_functions);
+
+          return found_functions;
         }
         else
         {
@@ -363,17 +347,11 @@ bool remove_function_pointerst::try_get_call_from_index(
             {
               out_functions.push_back(precise_match);
             }
-            else if(try_get_from_address_of(op, out_functions))
-            {
-            }
-            else if(try_get_call_from_symbol(op, out_functions))
-            {
-            }
-            else
-            {
-              // return false?
-              // in this case there is an element
-            }
+            bool found_functions=false;
+            found_functions=
+              found_functions||try_get_from_address_of(op, out_functions);
+            found_functions=
+              found_functions||try_get_call_from_symbol(op, out_functions);
           }
           return out_functions.size() > 0;
         }
@@ -437,7 +415,6 @@ bool remove_function_pointerst::try_evaluate_index_value(
   else if(index_value_expr.id()==ID_typecast)
   {
     // Follow the typecast
-
     return try_evaluate_index_value(index_value_expr.op0(), out_array_index);
   }
   else
@@ -723,23 +700,15 @@ void remove_function_pointerst::remove_function_pointer(
 
   exprt precise_call;
   functionst functions;
+  bool found_functions=false;
   if(try_get_precise_call(pointer, precise_call))
   {
     to_code_function_call(target->code).function()=precise_call;
     return;
   }
-  else if(try_get_from_address_of(pointer, functions))
-  {
-
-  }
-  else if(try_get_call_from_symbol(pointer, functions))
-  {
-
-  }
-  else if(try_get_call_from_index(pointer, functions))
-  {
-
-  }
+  found_functions=found_functions||try_get_from_address_of(pointer, functions);
+  found_functions=found_functions||try_get_call_from_symbol(pointer, functions);
+  found_functions=found_functions||try_get_call_from_index(pointer, functions);
 
   if(functions.size()==1)
   {
@@ -749,7 +718,7 @@ void remove_function_pointerst::remove_function_pointer(
 
   // if the functions list is still empty we didn't have any luck finding
   // any valid funcitons (or there are none??)
-  if(functions.size()==0)
+  if(!found_functions)
   {
     bool return_value_used=code.lhs().is_not_nil();
 
@@ -774,6 +743,10 @@ void remove_function_pointerst::remove_function_pointer(
       functions.push_back(expr);
     }
   }
+  else
+  {
+    assert(functions.size()>0);
+  }
 
   // the final target is a skip
   goto_programt final_skip;

From f46cfa50aa102b1b9c4ae09d51cd8bab2a39fbae Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Fri, 20 Jan 2017 11:21:27 +0000
Subject: [PATCH 13/17] Adding test for when FP array declared as a pointer

---
 regression/goto-analyzer/fp-removal11/main.c  | 31 +++++++++++++++++++
 .../goto-analyzer/fp-removal11/test.desc      | 17 ++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 regression/goto-analyzer/fp-removal11/main.c
 create mode 100644 regression/goto-analyzer/fp-removal11/test.desc

diff --git a/regression/goto-analyzer/fp-removal11/main.c b/regression/goto-analyzer/fp-removal11/main.c
new file mode 100644
index 00000000000..892f034bda8
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal11/main.c
@@ -0,0 +1,31 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(){
+  void_fp * const fp_tbl= malloc(sizeof(void_fp) * 3);
+  fp_tbl[0]=f2;
+  fp_tbl[1]=f3;
+  fp_tbl[2]=f4;
+  void_fp fp = fp_tbl[1];
+  fp();
+}
+
+void main(){
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal11/test.desc b/regression/goto-analyzer/fp-removal11/test.desc
new file mode 100644
index 00000000000..3c735d48a55
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal11/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp == f1 THEN GOTO 1$
+^\s*IF fp == f2 THEN GOTO 2$
+^\s*IF fp == f3 THEN GOTO 3$
+^\s*IF fp == f4 THEN GOTO 4$
+^\s*IF fp == f5 THEN GOTO 5$
+^\s*IF fp == f6 THEN GOTO 6$
+^\s*IF fp == f7 THEN GOTO 7$
+^\s*IF fp == f8 THEN GOTO 8$
+^\s*IF fp == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring

From c419218d7a307ec7a682982efc32d5747573abe5 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Tue, 24 Jan 2017 14:48:55 +0000
Subject: [PATCH 14/17] Don't try to follow non-const symbols

If a symbol is not a constant variable then its value may change. As a
result, we cannot reason about its value and hence we resort to the old
mechanism of all type compatible functions. The only exception is when
the symbol is the function itself which is implictly const

As we now require the symbol to be const, updated the tests to reflect
this. Adding tests for demonstrating what was the problem with non constant
pointers
---
 regression/goto-analyzer/fp-removal1/main.c   |  2 +-
 regression/goto-analyzer/fp-removal15/main.c  | 28 +++++++++++++++++
 .../goto-analyzer/fp-removal15/test.desc      | 17 ++++++++++
 regression/goto-analyzer/fp-removal16/main.c  | 31 +++++++++++++++++++
 .../goto-analyzer/fp-removal16/test.desc      | 16 ++++++++++
 regression/goto-analyzer/fp-removal2/main.c   |  2 +-
 regression/goto-analyzer/fp-removal3/main.c   |  2 +-
 regression/goto-analyzer/fp-removal4/main.c   |  2 +-
 regression/goto-analyzer/fp-removal5/main.c   |  2 +-
 .../remove_function_pointers.cpp              | 13 +++++++-
 10 files changed, 109 insertions(+), 6 deletions(-)
 create mode 100644 regression/goto-analyzer/fp-removal15/main.c
 create mode 100644 regression/goto-analyzer/fp-removal15/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal16/main.c
 create mode 100644 regression/goto-analyzer/fp-removal16/test.desc

diff --git a/regression/goto-analyzer/fp-removal1/main.c b/regression/goto-analyzer/fp-removal1/main.c
index f0d8118dfc8..f9b5908bce2 100644
--- a/regression/goto-analyzer/fp-removal1/main.c
+++ b/regression/goto-analyzer/fp-removal1/main.c
@@ -18,7 +18,7 @@ const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
 
 void func()
 {
-  void_fp fp = f2;
+  const void_fp fp = f2;
   fp();
 }
 
diff --git a/regression/goto-analyzer/fp-removal15/main.c b/regression/goto-analyzer/fp-removal15/main.c
new file mode 100644
index 00000000000..4b81bffdb30
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal15/main.c
@@ -0,0 +1,28 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  void_fp fp = f2;
+  fp = f3;
+  fp();
+}
+
+void main(){
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal15/test.desc b/regression/goto-analyzer/fp-removal15/test.desc
new file mode 100644
index 00000000000..3c735d48a55
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal15/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp == f1 THEN GOTO 1$
+^\s*IF fp == f2 THEN GOTO 2$
+^\s*IF fp == f3 THEN GOTO 3$
+^\s*IF fp == f4 THEN GOTO 4$
+^\s*IF fp == f5 THEN GOTO 5$
+^\s*IF fp == f6 THEN GOTO 6$
+^\s*IF fp == f7 THEN GOTO 7$
+^\s*IF fp == f8 THEN GOTO 8$
+^\s*IF fp == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal16/main.c b/regression/goto-analyzer/fp-removal16/main.c
new file mode 100644
index 00000000000..f1d35373e15
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal16/main.c
@@ -0,0 +1,31 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  const void_fp fp = f2;
+  const void_fp fp3 = f4;
+  void_fp fp2 = fp;
+  fp2 = fp3;
+  fp2();
+}
+
+void main()
+{
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal16/test.desc b/regression/goto-analyzer/fp-removal16/test.desc
new file mode 100644
index 00000000000..9ea2dfbbc29
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal16/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--show-goto-functions
+^Removing function pointers and virtual functions$
+^\s*IF fp2 == f1 THEN GOTO 1$
+^\s*IF fp2 == f2 THEN GOTO 2$
+^\s*IF fp2 == f3 THEN GOTO 3$
+^\s*IF fp2 == f4 THEN GOTO 4$
+^\s*IF fp2 == f5 THEN GOTO 5$
+^\s*IF fp2 == f6 THEN GOTO 6$
+^\s*IF fp2 == f7 THEN GOTO 7$
+^\s*IF fp2 == f8 THEN GOTO 8$
+^\s*IF fp2 == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/fp-removal2/main.c b/regression/goto-analyzer/fp-removal2/main.c
index 5f44200511c..41180ee5321 100644
--- a/regression/goto-analyzer/fp-removal2/main.c
+++ b/regression/goto-analyzer/fp-removal2/main.c
@@ -19,7 +19,7 @@ const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
 void func()
 {
   void_fp fp = f2;
-  void_fp fp2 = fp;
+  const void_fp fp2 = fp;
   fp2();
 }
 
diff --git a/regression/goto-analyzer/fp-removal3/main.c b/regression/goto-analyzer/fp-removal3/main.c
index d822ace2460..4d057be3a08 100644
--- a/regression/goto-analyzer/fp-removal3/main.c
+++ b/regression/goto-analyzer/fp-removal3/main.c
@@ -20,7 +20,7 @@ const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
 
 void func()
 {
-  void_fp fp = fp_tbl[1];
+  const void_fp fp = fp_tbl[1];
   fp();
 }
 
diff --git a/regression/goto-analyzer/fp-removal4/main.c b/regression/goto-analyzer/fp-removal4/main.c
index d858ea7372a..10eee1f8ba3 100644
--- a/regression/goto-analyzer/fp-removal4/main.c
+++ b/regression/goto-analyzer/fp-removal4/main.c
@@ -21,7 +21,7 @@ const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
 void func()
 {
   int x = 1;
-  void_fp fp = fp_tbl[x];
+  const void_fp fp = fp_tbl[x];
   fp();
 }
 
diff --git a/regression/goto-analyzer/fp-removal5/main.c b/regression/goto-analyzer/fp-removal5/main.c
index b97343152ab..20cf98fb59a 100644
--- a/regression/goto-analyzer/fp-removal5/main.c
+++ b/regression/goto-analyzer/fp-removal5/main.c
@@ -17,7 +17,7 @@ const void_fp fp_tbl[] = {f2, f3 ,f4};
 const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
 
 void func(int i){
-   void_fp fp = fp_tbl[i];
+   const void_fp fp = fp_tbl[i];
    fp();
 }
 
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 9de2ff286c8..8d6ed2bc166 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -706,8 +706,19 @@ void remove_function_pointerst::remove_function_pointer(
     to_code_function_call(target->code).function()=precise_call;
     return;
   }
+
+  const c_qualifierst pointer_qualifers(pointer.type());
+
   found_functions=found_functions||try_get_from_address_of(pointer, functions);
-  found_functions=found_functions||try_get_call_from_symbol(pointer, functions);
+
+  // If it is a symbol (except in the case where the symbol is the function
+  // symbol itself) then the symbol must be const or else can be reassigned.
+  if(pointer_qualifers.is_constant)
+  {
+    found_functions=
+      found_functions||try_get_call_from_symbol(pointer, functions);
+  }
+
   found_functions=found_functions||try_get_call_from_index(pointer, functions);
 
   if(functions.size()==1)

From 991611b279ea11353ffabfbe92601f0bbb2806e2 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Tue, 24 Jan 2017 18:17:49 +0000
Subject: [PATCH 15/17] Removing handlers for the cases can't generate

Since I do not know the code that can be written to trigger these cases,
it is safer to not blindly optimize them (instead they will fall through
to the old case of all matching functions). It still matches all the
cases outlined in the regressions folder.
---
 regression/goto-analyzer/fp-removal17/main.c  | 29 +++++++++++++++++++
 .../goto-analyzer/fp-removal17/test.desc      |  8 +++++
 .../remove_function_pointers.cpp              | 11 ++-----
 3 files changed, 40 insertions(+), 8 deletions(-)
 create mode 100644 regression/goto-analyzer/fp-removal17/main.c
 create mode 100644 regression/goto-analyzer/fp-removal17/test.desc

diff --git a/regression/goto-analyzer/fp-removal17/main.c b/regression/goto-analyzer/fp-removal17/main.c
new file mode 100644
index 00000000000..16df50eeb11
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal17/main.c
@@ -0,0 +1,29 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  // There isn't an obvious reason to write this code, but perhaps some
+  // code can get transformed into this so we should still handle it.
+  (*(&f2))();
+}
+
+void main()
+{
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal17/test.desc b/regression/goto-analyzer/fp-removal17/test.desc
new file mode 100644
index 00000000000..c3065239e49
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal17/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*f2();
+--
+^warning: ignoring
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 8d6ed2bc166..762cd7eaed0 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -698,17 +698,14 @@ void remove_function_pointerst::remove_function_pointer(
 
   const exprt &pointer=function.op0();
 
-  exprt precise_call;
   functionst functions;
   bool found_functions=false;
-  if(try_get_precise_call(pointer, precise_call))
-  {
-    to_code_function_call(target->code).function()=precise_call;
-    return;
-  }
 
   const c_qualifierst pointer_qualifers(pointer.type());
 
+  // This can happen for example with
+  // (*(&f2))();
+  // In this case we don't need constant check - implict
   found_functions=found_functions||try_get_from_address_of(pointer, functions);
 
   // If it is a symbol (except in the case where the symbol is the function
@@ -719,8 +716,6 @@ void remove_function_pointerst::remove_function_pointer(
       found_functions||try_get_call_from_symbol(pointer, functions);
   }
 
-  found_functions=found_functions||try_get_call_from_index(pointer, functions);
-
   if(functions.size()==1)
   {
     to_code_function_call(target->code).function()=functions.front();

From 49c4b040dd1f9db853a62c85a68587a837dcd404 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Tue, 24 Jan 2017 14:49:21 +0000
Subject: [PATCH 16/17] Adding tests for missing features

The function pointer optimsation can be further improved by dealing
with things like structs and pointers to function pointers. More
detail is outlined in https://github.com/diffblue/cbmc/issues/476
---
 regression/goto-analyzer/fp-removal12/main.c  | 38 ++++++++++++++++++
 .../goto-analyzer/fp-removal12/test.desc      | 15 +++++++
 regression/goto-analyzer/fp-removal13/main.c  | 40 +++++++++++++++++++
 .../goto-analyzer/fp-removal13/test.desc      | 15 +++++++
 regression/goto-analyzer/fp-removal14/main.c  | 28 +++++++++++++
 .../goto-analyzer/fp-removal14/test.desc      | 15 +++++++
 6 files changed, 151 insertions(+)
 create mode 100644 regression/goto-analyzer/fp-removal12/main.c
 create mode 100644 regression/goto-analyzer/fp-removal12/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal13/main.c
 create mode 100644 regression/goto-analyzer/fp-removal13/test.desc
 create mode 100644 regression/goto-analyzer/fp-removal14/main.c
 create mode 100644 regression/goto-analyzer/fp-removal14/test.desc

diff --git a/regression/goto-analyzer/fp-removal12/main.c b/regression/goto-analyzer/fp-removal12/main.c
new file mode 100644
index 00000000000..6598e892c5a
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal12/main.c
@@ -0,0 +1,38 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+typedef struct fp_container
+{
+  const void_fp fp_tbl[3];
+} fp_container;
+
+
+
+void func(){
+  fp_container container = { .fp_tbl = {f2 ,f3, f4} };
+  fp_container container2 = { .fp_tbl = {f5 ,f6, f7} };
+  // Illegal:
+  // container = container2;
+  void_fp fp = container.fp_tbl[1];
+  fp();
+}
+
+void main(){
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal12/test.desc b/regression/goto-analyzer/fp-removal12/test.desc
new file mode 100644
index 00000000000..63ff819792f
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal12/test.desc
@@ -0,0 +1,15 @@
+KNOWNBUG
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*f3();$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test is marked as a KNOWNBUG as it is possible for the function
+pointer to be optimized away. Currently goto-analyzer falls back to
+assuming it could be any type compatible function.
+
+Issue: https://github.com/diffblue/cbmc/issues/476
diff --git a/regression/goto-analyzer/fp-removal13/main.c b/regression/goto-analyzer/fp-removal13/main.c
new file mode 100644
index 00000000000..9df8dfaca35
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal13/main.c
@@ -0,0 +1,40 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+typedef struct fp_container
+{
+  void_fp fp_tbl[3];
+} fp_container;
+
+
+
+void func(){
+  const fp_container container = { .fp_tbl = {f2 ,f3, f4} };
+  fp_container container2 = { .fp_tbl = {f5 ,f6, f7} };
+  const void_fp alternatate_fp_tbl[] = {f5 ,f6, f7};
+  // Illegal:
+  // container = container2;
+  // container.fp_tbl = alternatate_fp_tbl;
+  void_fp fp = container.fp_tbl[1];
+  fp();
+}
+
+void main(){
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal13/test.desc b/regression/goto-analyzer/fp-removal13/test.desc
new file mode 100644
index 00000000000..63ff819792f
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal13/test.desc
@@ -0,0 +1,15 @@
+KNOWNBUG
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*f3();$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test is marked as a KNOWNBUG as it is possible for the function
+pointer to be optimized away. Currently goto-analyzer falls back to
+assuming it could be any type compatible function.
+
+Issue: https://github.com/diffblue/cbmc/issues/476
diff --git a/regression/goto-analyzer/fp-removal14/main.c b/regression/goto-analyzer/fp-removal14/main.c
new file mode 100644
index 00000000000..d2d58d107c7
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal14/main.c
@@ -0,0 +1,28 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(){
+  const void_fp fp = f3;
+  const void_fp* p2fp = &fp;
+  (*p2fp)();
+}
+
+void main(){
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal14/test.desc b/regression/goto-analyzer/fp-removal14/test.desc
new file mode 100644
index 00000000000..63ff819792f
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal14/test.desc
@@ -0,0 +1,15 @@
+KNOWNBUG
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*f3();$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test is marked as a KNOWNBUG as it is possible for the function
+pointer to be optimized away. Currently goto-analyzer falls back to
+assuming it could be any type compatible function.
+
+Issue: https://github.com/diffblue/cbmc/issues/476

From dc10ca0b85ac3064260bebd661668b2e02d7dd61 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Wed, 25 Jan 2017 16:54:22 +0000
Subject: [PATCH 17/17] Lint fixes

---
 .../remove_function_pointers.cpp              | 22 ++++++++++---------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 762cd7eaed0..6fa0a651fdc 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -102,7 +102,6 @@ class remove_function_pointerst
 
   bool try_get_array_from_index(
     const index_exprt &index_expr, array_exprt &out_array_expr);
-
 };
 
 /*******************************************************************\
@@ -266,11 +265,11 @@ bool remove_function_pointerst::try_get_call_from_symbol(
     }
     bool found_functions=false;
     found_functions=
-      found_functions||try_get_from_address_of(looked_up_val, out_functions);
+      found_functions || try_get_from_address_of(looked_up_val, out_functions);
     found_functions=
-      found_functions||try_get_call_from_index(looked_up_val, out_functions);
+      found_functions || try_get_call_from_index(looked_up_val, out_functions);
     found_functions=
-      found_functions||try_get_call_from_symbol(looked_up_val, out_functions);
+      found_functions || try_get_call_from_symbol(looked_up_val, out_functions);
     return found_functions;
   }
   else
@@ -330,9 +329,11 @@ bool remove_function_pointerst::try_get_call_from_index(
           }
           bool found_functions=false;
           found_functions=
-            found_functions||try_get_from_address_of(func_expr, out_functions);
+            found_functions ||
+              try_get_from_address_of(func_expr, out_functions);
           found_functions=
-            found_functions||try_get_call_from_symbol(func_expr, out_functions);
+            found_functions ||
+              try_get_call_from_symbol(func_expr, out_functions);
 
           return found_functions;
         }
@@ -349,9 +350,9 @@ bool remove_function_pointerst::try_get_call_from_index(
             }
             bool found_functions=false;
             found_functions=
-              found_functions||try_get_from_address_of(op, out_functions);
+              found_functions || try_get_from_address_of(op, out_functions);
             found_functions=
-              found_functions||try_get_call_from_symbol(op, out_functions);
+              found_functions || try_get_call_from_symbol(op, out_functions);
           }
           return out_functions.size() > 0;
         }
@@ -706,14 +707,15 @@ void remove_function_pointerst::remove_function_pointer(
   // This can happen for example with
   // (*(&f2))();
   // In this case we don't need constant check - implict
-  found_functions=found_functions||try_get_from_address_of(pointer, functions);
+  found_functions=found_functions ||
+    try_get_from_address_of(pointer, functions);
 
   // If it is a symbol (except in the case where the symbol is the function
   // symbol itself) then the symbol must be const or else can be reassigned.
   if(pointer_qualifers.is_constant)
   {
     found_functions=
-      found_functions||try_get_call_from_symbol(pointer, functions);
+      found_functions || try_get_call_from_symbol(pointer, functions);
   }
 
   if(functions.size()==1)