goto-instrument: function pointer removal with value_set_fi

This adds a new option to goto-instrument for removing function pointers.
The points-to analysis is done using flow-insensitive value sets, which is
more precise than using the signature of the function to identify the
points-to set.

Author: Daniel Kroening

regression/goto-instrument/value-set-fi-fp-removal/test.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+typedef void (*fp_t)();
+
+void f()
+{
+}
+
+void g()
+{
+}
+
+int main(void)
+{
+  fp_t fp = f;
+  fp();
+
+  // this would fool an analysis that looks for functions whose address is taken
+  fp_t other_fp = g;
+}

regression/goto-instrument/value-set-fi-fp-removal/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^  function: f$
+--
+^  function: g$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.

regression/goto-instrument/value-set-fi-fp-removal2/test.c

@@ -0,0 +1,30 @@
+
+typedef void (*fp_t)(int, int);
+
+void add(int a, int b) 
+{ 
+    
+} 
+void subtract(int a, int b) 
+{ 
+   
+} 
+void multiply(int a, int b) 
+{ 
+     
+} 
+  
+int main() 
+{ 
+    // fun_ptr_arr is an array of function pointers 
+    void (*fun_ptr_arr[])(int, int) = {add, subtract, add}; 
+
+    // Multiply should not be added into the value set
+    fp_t other_fp = multiply;
+    void (*fun_ptr_arr2[])(int, int) = {multiply, subtract, add}; 
+
+    // the fp removal over-approximates and assumes this could be any pointer in the array
+    (*fun_ptr_arr[0])(1, 1); 
+
+    return 0; 
+} 

regression/goto-instrument/value-set-fi-fp-removal2/test.desc

@@ -0,0 +1,13 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^  function: add$
+^  function: subtract$
+--
+^  function: multiply$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.

regression/goto-instrument/value-set-fi-fp-removal3/test.c

@@ -0,0 +1,34 @@
+typedef void (*fp_t)(int, int);
+
+void add(int a, int b) 
+{ 
+    
+} 
+void subtract(int a, int b) 
+{ 
+   
+} 
+void multiply(int a, int b) 
+{ 
+     
+} 
+  
+int main() 
+{ 
+    // fun_ptr_arr is an array of function pointers 
+    struct my_struct{
+    	fp_t first_pointer;
+    	fp_t second_pointer;
+    } struct1;
+
+    struct1.first_pointer=add;
+
+    // Multiply and subtract should not be added into the value set
+    fp_t other_fp = multiply;
+    struct1.second_pointer=subtract;
+
+    // this pointer can only be "add"
+    struct1.first_pointer(1,1);
+
+    return 0; 
+} 

regression/goto-instrument/value-set-fi-fp-removal3/test.desc

@@ -0,0 +1,13 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^  function: add$
+--
+^  function: multiply$
+^  function: subtract$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.

regression/goto-instrument/value-set-fi-fp-removal4/test.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+typedef void (*fp_t)();
+
+void f()
+{
+}
+
+void g()
+{
+}
+
+int main(void)
+{
+  fp_t fp;
+  fp();
+
+  // the value set is empty, defaults to standard function pointer removal behaviour
+  fp_t other_fp = g;
+  other_fp = f;
+}

regression/goto-instrument/value-set-fi-fp-removal4/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^file test.c line 16 function main: replacing function pointer by 2 possible targets$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.

regression/goto-instrument/value-set-fi-fp-removal5/test.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+typedef void (*fp_t)();
+
+void f(int x)
+{
+}
+
+void g(int y)
+{
+}
+
+int main(void)
+{
+  fp_t fp;
+  fp();
+
+  // the value set is empty, defaults to standard function pointer removal behaviour
+  fp_t other_fp = g;
+}

regression/goto-instrument/value-set-fi-fp-removal5/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^file test.c line 16 function main: replacing function pointer by 0 possible targets$
+
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.