diff --git a/regression/goto-analyzer/fp-removal1/main.c b/regression/goto-analyzer/fp-removal1/main.c
new file mode 100644
index 00000000000..f9b5908bce2
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal1/main.c
@@ -0,0 +1,27 @@
+#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;
+  fp();
+}
+
+void main(){
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal1/test.desc b/regression/goto-analyzer/fp-removal1/test.desc
new file mode 100644
index 00000000000..c3065239e49
--- /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*f2();
+--
+^warning: ignoring
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-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
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
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-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/regression/goto-analyzer/fp-removal2/main.c b/regression/goto-analyzer/fp-removal2/main.c
new file mode 100644
index 00000000000..41180ee5321
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal2/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()
+{
+  void_fp fp = f2;
+  const void_fp fp2 = fp;
+  fp2();
+}
+
+void main()
+{
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal2/test.desc b/regression/goto-analyzer/fp-removal2/test.desc
new file mode 100644
index 00000000000..9ba26c84989
--- /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*f2();$
+^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..4d057be3a08
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal3/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);
+
+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
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  const void_fp fp = fp_tbl[1];
+  fp();
+}
+
+void main(){
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal3/test.desc b/regression/goto-analyzer/fp-removal3/test.desc
new file mode 100644
index 00000000000..a36fb208c69
--- /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*f3();$
+^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..10eee1f8ba3
--- /dev/null
+++ b/regression/goto-analyzer/fp-removal4/main.c
@@ -0,0 +1,30 @@
+#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);
+
+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
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  int x = 1;
+  const void_fp fp = fp_tbl[x];
+  fp();
+}
+
+void main(){
+  func();
+}
diff --git a/regression/goto-analyzer/fp-removal4/test.desc b/regression/goto-analyzer/fp-removal4/test.desc
new file mode 100644
index 00000000000..a36fb208c69
--- /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*f3();$
+^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..20cf98fb59a
--- /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);
+
+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
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(int i){
+   const void_fp fp = fp_tbl[i];
+   fp();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func(i);
+   }
+}
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
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
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 7a25def3823..6fa0a651fdc 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>
@@ -17,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"
@@ -80,6 +82,26 @@ class remove_function_pointerst
       compute_address_taken_functions(s.second.value, address_taken);
   }
 
+private:
+  typedef std::list<exprt> functionst;
+
+  bool try_get_precise_call(
+    const exprt &expr, exprt &out_function);
+
+  bool try_get_from_address_of(
+    const exprt &expr, 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);
+
+  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);
 };
 
 /*******************************************************************\
@@ -140,6 +162,319 @@ symbolt &remove_function_pointerst::new_tmp_symbol()
 
 /*******************************************************************\
 
+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 &expr,
+  exprt &out_function)
+{
+  if(expr.id()==ID_symbol && expr.type().id()==ID_code)
+  {
+    out_function=to_symbol_expr(expr);
+    return true;
+  }
+  else
+  {
+    return false;
+  }
+}
+
+/*******************************************************************\
+
+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 &expr, functionst &out_functions)
+{
+  if(expr.id()==ID_address_of)
+  {
+    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))
+    {
+      out_functions.push_back(precise_expr);
+      return true;
+    }
+    else
+    {
+      return try_get_call_from_symbol(address_of_expr.object(), out_functions);
+    }
+  }
+  else
+  {
+    return false;
+  }
+}
+
+/*******************************************************************\
+
+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)
+{
+  if(symbol_expr.id()==ID_symbol)
+  {
+    const symbolt &symbol=
+      symbol_table.lookup(symbol_expr.get(ID_identifier));
+    const 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);
+      return true;
+    }
+    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
+  {
+    return false;
+  }
+}
+
+/*******************************************************************\
+
+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)
+{
+  if(expr.id()==ID_index)
+  {
+    const index_exprt &index_expr=to_index_expr(expr);
+
+    array_exprt array_expr;
+    if(try_get_array_from_index(index_expr, array_expr))
+    {
+      // 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)
+      {
+        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);
+            return true;
+          }
+          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
+        {
+          // 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);
+            }
+            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;
+        }
+      }
+      else
+      {
+        return false;
+      }
+    }
+    else
+    {
+      return false;
+    }
+  }
+  else
+  {
+    return false;
+  }
+}
+
+/*******************************************************************\
+
+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)
+{
+  if(index_value_expr.id()==ID_constant)
+  {
+    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)
+    {
+      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;
+  }
+}
+
+/*******************************************************************\
+
+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)
+{
+  const 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
+  {
+    return false;
+  }
+}
+
+/*******************************************************************\
+
 Function: remove_function_pointerst::arg_is_type_compatible
 
   Inputs:
@@ -364,39 +699,61 @@ 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)
+  functionst functions;
+  bool found_functions=false;
+
+  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
+  // symbol itself) then the symbol must be const or else can be reassigned.
+  if(pointer_qualifers.is_constant)
   {
-    to_code_function_call(target->code).function()=
-      to_address_of_expr(pointer).object();
-    return;
+    found_functions=
+      found_functions || try_get_call_from_symbol(pointer, functions);
   }
 
-  typedef std::list<exprt> functionst;
-  functionst functions;
-
-  bool return_value_used=code.lhs().is_not_nil();
+  if(functions.size()==1)
+  {
+    to_code_function_call(target->code).function()=functions.front();
+    return;
+  }
 
-  // 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(!found_functions)
   {
-    // address taken?
-    if(address_taken.find(t.first)==address_taken.end())
-      continue;
+    bool return_value_used=code.lhs().is_not_nil();
+
+    // 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;
 
-    // type-compatible?
-    if(!is_type_compatible(return_value_used, call_type, t.second))
-      continue;
+      // type-compatible?
+      if(!is_type_compatible(return_value_used, call_type, t.second))
+        continue;
 
-    if(t.first=="pthread_mutex_cleanup")
-      continue;
+      if(t.first=="pthread_mutex_cleanup")
+        continue;
 
-    symbol_exprt expr;
-    expr.type()=t.second;
-    expr.set_identifier(t.first);
-    functions.push_back(expr);
+      symbol_exprt expr;
+      expr.type()=t.second;
+      expr.set_identifier(t.first);
+      functions.push_back(expr);
+    }
+  }
+  else
+  {
+    assert(functions.size()>0);
   }
 
   // the final target is a skip