Restrict function pointers by name

regression/goto-instrument/restrict-function-pointer-by-name-global/test.c

@@ -0,0 +1,28 @@
+int f(void)
+{
+  return 1;
+}
+
+int g(void)
+{
+  return 2;
+}
+
+int h(void)
+{
+  return 3;
+}
+
+typedef int (*fp_t)(void);
+
+fp_t fp;
+
+void main()
+{
+  int cond;
+  fp = cond ? f : g;
+  int res = fp();
+  __CPROVER_assert(res == 1, "");
+  __CPROVER_assert(res == 2, "");
+  __CPROVER_assert(res == 1 || res == 2, "");
+}

regression/goto-instrument/restrict-function-pointer-by-name-global/test.desc

@@ -0,0 +1,15 @@
+CORE
+test.c
+--restrict-function-pointer-by-name fp/f,g
+\[main\.assertion\.1\] line \d+ dereferenced function pointer at main\.function_pointer_call\.1 must be one of \[(f, g)|(g, f)\]: SUCCESS
+\[main.assertion.2\] line \d+ assertion: FAILURE
+\[main.assertion.3\] line \d+ assertion: FAILURE
+\[main.assertion.4\] line \d+ assertion: SUCCESS
+f\(\)
+g\(\)
+^EXIT=10$
+^SIGNAL=0$
+--
+h\(\)
+--
+Check that a call to a global function pointer is correctly restricted

regression/goto-instrument/restrict-function-pointer-by-name-local/test.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int f(void)
+{
+  return 1;
+}
+
+int g(void)
+{
+  return 2;
+}
+
+typedef int (*fp_t)(void);
+
+void main()
+{
+  fp_t fp = f;
+  assert(fp() == 1);
+}

regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--restrict-function-pointer-by-name main::1::fp/f
+\[main\.assertion\.1\] line \d+ dereferenced function pointer at main\.function_pointer_call\.1 must be f: SUCCESS
+\[main\.assertion\.2\] line \d+ assertion fp\(\) == 1: SUCCESS
+f\(\)
+^EXIT=0$
+^SIGNAL=0$
+--
+g\(\)
+--
+Check that a call to a local function pointer is correctly restricted

regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int f(void)
+{
+  return 1;
+}
+
+int g(void)
+{
+  return 2;
+}
+
+typedef int (*fp_t)(void);
+
+void use_fp(fp_t fp)
+{
+  assert(fp() == 1);
+}
+
+void main()
+{
+  use_fp(f);
+}

regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--restrict-function-pointer-by-name use_fp::fp/f
+\[use_fp\.assertion\.1\] line \d+ dereferenced function pointer at use_fp\.function_pointer_call\.1 must be f: SUCCESS
+\[use_fp\.assertion\.2\] line \d+ assertion fp\(\) == 1: SUCCESS
+f\(\)
+^EXIT=0$
+^SIGNAL=0$
+--
+g\(\)
+--
+Check that a call to a function pointer parameter is correctly restricted

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c

@@ -2,30 +2,14 @@
 
 typedef int (*fptr_t)(int);
 
-fptr_t get_f(void);
-
 void use_f(fptr_t fptr)
 {
-  assert(fptr(10) >= 10);
-}
-
-void select_f(void);
-void select_g(void);
-void select_h(void);
-
-int main(void)
-{
-  select_f();
-  use_f(get_f());
-  select_g();
-  use_f(get_f());
-  select_h();
-  use_f(get_f());
+  fptr(1);
 }
 
 int f(int x)
 {
-  return x + 1;
+  return x;
 }
 
 int g(int x)
@@ -35,38 +19,19 @@ int g(int x)
 
 int h(int x)
 {
-  return x - 1;
-}
-
-int select_function = 0;
-
-void select_f(void)
-{
-  select_function = 0;
+  return x;
 }
 
-void select_g(void)
+int other(int x)
 {
-  select_function = 1;
+  return x;
 }
 
-void select_h(void)
+int main(void)
 {
-  select_function = 2;
+  use_f(f);
+  use_f(g);
+  use_f(h);
+  use_f(other);
 }
 
-fptr_t get_f(void)
-{
-  if(select_function == 0)
-  {
-    return f;
-  }
-  else if(select_function == 1)
-  {
-    return g;
-  }
-  else
-  {
-    return h;
-  }
-}

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc

@@ -1,13 +1,14 @@
 CORE
 test.c
---function-pointer-restrictions-file restrictions.json --restrict-function-pointer use_f.function_pointer_call.1/g
-\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: FAILURE
+--function-pointer-restrictions-file restrictions.json --restrict-function-pointer use_f.function_pointer_call.1/g --restrict-function-pointer-by-name use_f::fptr/h
+\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g|h), (f|g|h), (f|g|h)\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --
 --
 This test checks that the restrictions for a function pointer are the union of
-the restrictions given in a file and on the command line.
+the restrictions given in a file and on the command line (both with functions
+pointers being numbered and named)
 
 The test further checks that the correct safety assertions are generated. The
 function pointer restriction feature outputs safety assertions for all calls

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1037,13 +1037,17 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   {
     parse_function_pointer_restriction_options_from_cmdline(cmdline, options);
 
-    const auto function_pointer_restrictions =
-      function_pointer_restrictionst::from_options(
-        options, log.get_message_handler());
-
-    if(!function_pointer_restrictions.restrictions.empty())
+    if(
+      options.is_set(RESTRICT_FUNCTION_POINTER_OPT) ||
+      options.is_set(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) ||
+      options.is_set(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT))
     {
       label_function_pointer_call_sites(goto_model);
+
+      const auto function_pointer_restrictions =
+        function_pointer_restrictionst::from_options(
+          options, goto_model, log.get_message_handler());
+
       restrict_function_pointers(goto_model, function_pointer_restrictions);
     }
   }