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.

Author: thk123

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

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$

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

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

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

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

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

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

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);
             }
           }
         }

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)
     {