From e8202d946c7b314b2d8b6c3bc10078f545d2d196 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Wed, 17 May 2017 16:52:50 +0100
Subject: [PATCH 1/5] Added test for array containing a zero struct

Uninitialized entries in an array are set to zero (i.e. the struct
contains zero and a null pointer). The output should still generate the
possible valid if statements as it does with an array of function
pointers containing null (as demonstrated in
approx-const-fp-array-variable-const-fp-with-null).
---
 .../main.c                                    | 42 +++++++++++++++++++
 .../test.desc                                 | 17 ++++++++
 2 files changed, 59 insertions(+)
 create mode 100644 regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/main.c
 create mode 100644 regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc

diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/main.c b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/main.c
new file mode 100644
index 00000000000..bc7c67957e2
--- /dev/null
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/main.c
@@ -0,0 +1,42 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i\n", 1); }
+void f2 (void) { printf("%i\n", 2); }
+void f3 (void) { printf("%i\n", 3); }
+void f4 (void) { printf("%i\n", 4); }
+void f5 (void) { printf("%i\n", 5); }
+void f6 (void) { printf("%i\n", 6); }
+void f7 (void) { printf("%i\n", 7); }
+void f8 (void) { printf("%i\n", 8); }
+void f9 (void) { printf("%i\n", 9); }
+
+typedef void(*void_fp)(void);
+
+struct action
+{
+  int x;
+  void_fp fun;
+};
+
+// Array with an empty final element
+const struct action fp_tbl[5] = {{1, f2}, {2, f3} ,{3, 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].fun;
+  fp();
+}
+
+int main()
+{
+  for(int i=0;i<3;i++)
+  {
+    func(i);
+  }
+
+  return 0;
+}
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
new file mode 100644
index 00000000000..b716801b6ee
--- /dev/null
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
@@ -0,0 +1,17 @@
+KNOWNBUG
+main.c
+--show-goto-functions --verbosity 10 --pointer-check
+^Removing function pointers and virtual functions$
+^\s*IF fp == f2 THEN GOTO [0-9]$
+^\s*IF fp == f3 THEN GOTO [0-9]$
+^\s*IF fp == f4 THEN GOTO [0-9]$
+^\s*ASSERT FALSE // invalid function pointer$
+^SIGNAL=0$
+--
+^warning: ignoring
+^\s*IF fp == f1 THEN GOTO [0-9]$
+^\s*IF fp == f5 THEN GOTO [0-9]$
+^\s*IF fp == f6 THEN GOTO [0-9]$
+^\s*IF fp == f7 THEN GOTO [0-9]$
+^\s*IF fp == f8 THEN GOTO [0-9]$
+^\s*IF fp == f9 THEN GOTO [0-9]$

From ab236842ff8fd0bfcd1f9c3f465f9fd7d77aa54b Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Tue, 13 Jun 2017 16:38:39 +0100
Subject: [PATCH 2/5] Improved the interface of remove_const_functions

It is more logical that the functor operator takes the expression it is
considering as it would allow the same object to be reused for multiple
function pointer resolutions.
---
 src/goto-programs/remove_const_function_pointers.cpp | 11 +++++------
 src/goto-programs/remove_const_function_pointers.h   |  4 +---
 src/goto-programs/remove_function_pointers.cpp       |  4 ++--
 3 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp
index 3e9824cad30..0c6cbf8f8e4 100644
--- a/src/goto-programs/remove_const_function_pointers.cpp
+++ b/src/goto-programs/remove_const_function_pointers.cpp
@@ -9,12 +9,12 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com
 /// \file
 /// Goto Programs
 
+#include "remove_const_function_pointers.h"
+
 #include <ansi-c/c_qualifiers.h>
 #include <util/simplify_expr.h>
 #include <util/arith_tools.h>
 
-#include "remove_const_function_pointers.h"
-
 #define LOG(message, irep) \
   debug() << "Case " << __LINE__ << " : " << message << "\n" \
           << irep.pretty() << eom;
@@ -22,16 +22,13 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com
 /// To take a function call on a function pointer, and if possible resolve it to
 /// a small collection of possible values.
 /// \param message_handler: The message handler for messaget
-/// \param base_expression: The function call through a function pointer
 /// \param ns: The namespace to use to resolve types
 /// \param symbol_table: The symbol table to look up symbols in
 remove_const_function_pointerst::remove_const_function_pointerst(
   message_handlert &message_handler,
-  const exprt &base_expression,
   const namespacet &ns,
   const symbol_tablet &symbol_table):
     messaget(message_handler),
-    original_expression(base_expression),
     ns(ns),
     symbol_table(symbol_table)
 {}
@@ -41,16 +38,18 @@ remove_const_function_pointerst::remove_const_function_pointerst(
 /// that are const and: - assigned directly to a function - assigned to a value
 /// in an array of functions - assigned to a const struct component Or
 /// variations within.
+/// \param base_expression: The function call through a function pointer
 /// \param out_functions: The functions that (symbols of type ID_code) the base
 /// expression could take.
 /// \return Returns true if it was able to resolve the call, false if not. If it
 ///   returns true, out_functions will be populated by all the possible values
 ///   the function pointer could be.
 bool remove_const_function_pointerst::operator()(
+  const exprt &base_expression,
   functionst &out_functions)
 {
   // Replace all const symbols with their values
-  exprt non_symbol_expression=replace_const_symbols(original_expression);
+  exprt non_symbol_expression=replace_const_symbols(base_expression);
   return try_resolve_function_call(non_symbol_expression, out_functions);
 }
 
diff --git a/src/goto-programs/remove_const_function_pointers.h b/src/goto-programs/remove_const_function_pointers.h
index 45ed1c16fba..469deaec032 100644
--- a/src/goto-programs/remove_const_function_pointers.h
+++ b/src/goto-programs/remove_const_function_pointers.h
@@ -27,11 +27,10 @@ class remove_const_function_pointerst:public messaget
   typedef std::list<exprt> expressionst;
   remove_const_function_pointerst(
     message_handlert &message_handler,
-    const exprt &base_expression,
     const namespacet &ns,
     const symbol_tablet &symbol_table);
 
-  bool operator()(functionst &out_functions);
+  bool operator()(const exprt &base_expression, functionst &out_functions);
 
 private:
   exprt replace_const_symbols(const exprt &expression) const;
@@ -93,7 +92,6 @@ class remove_const_function_pointerst:public messaget
   exprt get_component_value(
     const struct_exprt &struct_expr, const member_exprt &member_expr);
 
-  const exprt original_expression;
   const namespacet &ns;
   const symbol_tablet &symbol_table;
 };
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index d62d1b62c87..8ee1f01bcc8 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -292,9 +292,9 @@ void remove_function_pointerst::remove_function_pointer(
   else
   {
     remove_const_function_pointerst fpr(
-    get_message_handler(), pointer, ns, symbol_table);
+    get_message_handler(), ns, symbol_table);
 
-    found_functions=fpr(functions);
+    found_functions=fpr(pointer, functions);
 
     // Either found_functions is true therefore the functions should not
     // be empty

From e2049b0ab30ad87ad1e6e78a2de0e4e41c0c5103 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Tue, 13 Jun 2017 17:07:01 +0100
Subject: [PATCH 3/5] Making the approx and precise FP removal tests more
 precise

We now exclude the line that would catch if the function is replaced by
all 9 possibilities.
---
 .../goto-analyzer/approx-array-variable-const-fp/test.desc       | 1 +
 .../approx-const-fp-array-variable-cast-const-fp/test.desc       | 1 +
 .../approx-const-fp-array-variable-const-fp-with-null/test.desc  | 1 +
 .../approx-const-fp-array-variable-const-fp/test.desc            | 1 +
 .../test.desc                                                    | 1 +
 .../test.desc                                                    | 1 +
 .../test.desc                                                    | 1 +
 .../test.desc                                                    | 1 +
 .../goto-analyzer/precise-array-calculation-const-fp/test.desc   | 1 +
 .../goto-analyzer/precise-array-literal-const-fp/test.desc       | 1 +
 .../precise-const-fp-array-const-variable-const-fp/test.desc     | 1 +
 .../precise-const-fp-array-literal-const-fp-run-time/test.desc   | 1 +
 .../precise-const-fp-array-literal-const-fp/test.desc            | 1 +
 .../test.desc                                                    | 1 +
 .../test.desc                                                    | 1 +
 regression/goto-analyzer/precise-const-fp-const-fp/test.desc     | 1 +
 .../test.desc                                                    | 1 +
 .../test.desc                                                    | 1 +
 .../precise-const-fp-const-struct-non-const-fp/test.desc         | 1 +
 .../test.desc                                                    | 1 +
 regression/goto-analyzer/precise-const-fp/test.desc              | 1 +
 .../precise-const-pointer-const-struct-fp/test.desc              | 1 +
 .../goto-analyzer/precise-const-struct-non-const-fp/test.desc    | 1 +
 .../precise-derefence-const-pointer-const-fp/test.desc           | 1 +
 regression/goto-analyzer/precise-derefence/test.desc             | 1 +
 .../precise-dereference-address-pointer-const-fp/test.desc       | 1 +
 .../test.desc                                                    | 1 +
 .../test.desc                                                    | 1 +
 .../precise-dereference-const-struct-pointer-const-fp/test.desc  | 1 +
 29 files changed, 29 insertions(+)

diff --git a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc
index 38027f70600..c0e6ab6bfc2 100644
--- a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc
@@ -14,3 +14,4 @@ main.c
 ^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f8 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f9 THEN GOTO [0-9]$
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc
index e6f1f4b5752..0d2ddf970da 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc
@@ -14,3 +14,4 @@ main.c
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc
index e6f1f4b5752..0d2ddf970da 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc
@@ -14,3 +14,4 @@ main.c
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc
index e6f1f4b5752..0d2ddf970da 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc
@@ -14,3 +14,4 @@ main.c
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
index e6f1f4b5752..0d2ddf970da 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
@@ -14,3 +14,4 @@ main.c
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc
index e6f1f4b5752..0d2ddf970da 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc
@@ -14,3 +14,4 @@ main.c
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc
index 661ac93a14f..b2f2a12d4ee 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc
@@ -14,3 +14,4 @@ main.c
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
 ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
index b716801b6ee..50fc1d4e137 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
@@ -15,3 +15,4 @@ main.c
 ^\s*IF fp == f7 THEN GOTO [0-9]$
 ^\s*IF fp == f8 THEN GOTO [0-9]$
 ^\s*IF fp == f9 THEN GOTO [0-9]$
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc
index ab2a0acefba..bb3ac1b5cf1 100644
--- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc
@@ -5,3 +5,4 @@ main.c
 ^\s*f3\(\);$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
index 90cd2485ce1..153ca97de3b 100644
--- a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc
index 40361f6ccc2..27df5bd2f67 100644
--- a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc
index 90cd2485ce1..153ca97de3b 100644
--- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp/test.desc
index 4dd6e7fd098..402774c29b7 100644
--- a/regression/goto-analyzer/precise-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp/test.desc
@@ -5,3 +5,4 @@ main.c
 ^\s*f2\(\);
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc
index 40361f6ccc2..27df5bd2f67 100644
--- a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc
index 90cd2485ce1..153ca97de3b 100644
--- a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-derefence/test.desc b/regression/goto-analyzer/precise-derefence/test.desc
index 4dd6e7fd098..402774c29b7 100644
--- a/regression/goto-analyzer/precise-derefence/test.desc
+++ b/regression/goto-analyzer/precise-derefence/test.desc
@@ -5,3 +5,4 @@ main.c
 ^\s*f2\(\);
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc
index fad0e6c7a1d..98fc0ff815c 100644
--- a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc
@@ -6,3 +6,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+function \w+: replacing function pointer by 9 possible targets

From d7e4a3540e29cba8afe9cd72f9c75a36ea769fe4 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Tue, 13 Jun 2017 17:32:54 +0100
Subject: [PATCH 4/5] Fixed null pointer related bug

We now allow finding a null pointer at any point in the removal process
(previously we were just excepting it in an array of pointers). This
fixes diffblue/cbmc-toyota#128

This slightly changes the behaviour in the event we can precisely
resolve a null pointer. Previously we would have replaced the function
pointer with a branch on all valid function pointers. Now we will
(providing --pointer-check is enabled) simply assert false.

This behaviour is more desirable - if we know a pointer is NULL then the
previous if statements that were generated would all be ignored anyway,
so this just reduces the size of the goto program with no impact on its
behaviour.

Pointers to not functions still cause a rejection, so tests that exibit
this have been modified to require this.
---
 .../test.desc                                 |  1 +
 .../test.desc                                 |  2 +-
 .../test.desc                                 |  1 +
 .../no-match-const-fp-const-fp-null/test.desc |  1 +
 .../test.desc                                 |  1 +
 .../test.desc                                 |  1 +
 .../no-match-const-fp-null/test.desc          |  1 +
 .../test.desc                                 |  1 +
 .../remove_const_function_pointers.cpp        | 19 +++++++++++++++----
 .../remove_function_pointers.cpp              |  9 +++++----
 10 files changed, 28 insertions(+), 9 deletions(-)

diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc
index 0d2ddf970da..383f5ad956c 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc
@@ -5,6 +5,7 @@ main.c
 ^\s*IF fp == f2 THEN GOTO [0-9]$
 ^\s*IF fp == f3 THEN GOTO [0-9]$
 ^\s*IF fp == f4 THEN GOTO [0-9]$
+replacing function pointer by 3 possible targets
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
index 50fc1d4e137..fab84bc077c 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$
diff --git a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc
index 4786993cade..90a60c56a40 100644
--- a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc
+++ b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc
@@ -4,5 +4,6 @@ main.c
 ^Removing function pointers and virtual functions$
 ^\s*ASSERT FALSE // invalid function pointer$
 ^SIGNAL=0$
+function func: replacing function pointer by 0 possible targets
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc
index 4786993cade..1299353033d 100644
--- a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc
@@ -4,5 +4,6 @@ main.c
 ^Removing function pointers and virtual functions$
 ^\s*ASSERT FALSE // invalid function pointer$
 ^SIGNAL=0$
+replacing function pointer by 0 possible targets
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc
index 4786993cade..40a2b941d75 100644
--- a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc
@@ -3,6 +3,7 @@ main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$
 ^\s*ASSERT FALSE // invalid function pointer$
+replacing function pointer by 9 possible targets
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc
index 4786993cade..40a2b941d75 100644
--- a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc
@@ -3,6 +3,7 @@ main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$
 ^\s*ASSERT FALSE // invalid function pointer$
+replacing function pointer by 9 possible targets
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/no-match-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-null/test.desc
index d8e8d833238..bea1fb7c356 100644
--- a/regression/goto-analyzer/no-match-const-fp-null/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-null/test.desc
@@ -3,5 +3,6 @@ main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$
 ^\s*ASSERT FALSE // invalid function pointer$
+function func: replacing function pointer by 0 possible targets
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc
index 4786993cade..1299353033d 100644
--- a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc
+++ b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc
@@ -4,5 +4,6 @@ main.c
 ^Removing function pointers and virtual functions$
 ^\s*ASSERT FALSE // invalid function pointer$
 ^SIGNAL=0$
+replacing function pointer by 0 possible targets
 --
 ^warning: ignoring
diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp
index 0c6cbf8f8e4..de5649892f2 100644
--- a/src/goto-programs/remove_const_function_pointers.cpp
+++ b/src/goto-programs/remove_const_function_pointers.cpp
@@ -164,6 +164,20 @@ bool remove_const_function_pointerst::try_resolve_function_call(
       resolved=false;
     }
   }
+  else if(simplified_expr.id()==ID_constant)
+  {
+    if(simplified_expr.is_zero())
+    {
+      // We have the null pointer - no need to throw everything away
+      // but we don't add any functions either
+      resolved=true;
+    }
+    else
+    {
+      LOG("Non-zero constant value found", simplified_expr);
+      resolved=false;
+    }
+  }
   else
   {
     LOG("Unrecognised expression", simplified_expr);
@@ -555,10 +569,7 @@ bool remove_const_function_pointerst::try_resolve_index_of(
 
             for(const exprt &resolved_array_entry : array_contents)
             {
-              if(!resolved_array_entry.is_zero())
-              {
-                out_expressions.push_back(resolved_array_entry);
-              }
+              out_expressions.push_back(resolved_array_entry);
             }
           }
         }
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 8ee1f01bcc8..e7ee1ae20da 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -296,10 +296,11 @@ void remove_function_pointerst::remove_function_pointer(
 
     found_functions=fpr(pointer, functions);
 
-    // Either found_functions is true therefore the functions should not
-    // be empty
-    // Or found_functions is false therefore the functions should be empty
-    assert(found_functions != functions.empty());
+    // if found_functions is false, functions should be empty
+    // however, it is possible for found_functions to be true and functions
+    // to be empty (this happens if the pointer can only resolve to the null
+    // pointer)
+    assert(found_functions || functions.empty());
 
     if(functions.size()==1)
     {

From 8ec1890da538d478dd450f8f915818f3e64b22d9 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Tue, 13 Jun 2017 18:20:35 +0100
Subject: [PATCH 5/5] Replace assert with appropriate invariant

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

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index e7ee1ae20da..f9b9a3bd313 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_type.h>
 #include <ansi-c/c_qualifiers.h>
 #include <analyses/does_remove_const.h>
+#include <util/invariant.h>
 
 #include <util/c_types.h>
 
@@ -300,7 +301,7 @@ void remove_function_pointerst::remove_function_pointer(
     // however, it is possible for found_functions to be true and functions
     // to be empty (this happens if the pointer can only resolve to the null
     // pointer)
-    assert(found_functions || functions.empty());
+    CHECK_RETURN(found_functions || functions.empty());
 
     if(functions.size()==1)
     {