Refactor restrict function pointers regression tests

Author: danpoe

regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c

@@ -10,9 +10,6 @@ void use_fg(int choice, fptr_t fptr, fptr_t gptr)
   assert((choice ? fptr : gptr)(10) == 10 + choice);
 }
 
-// this is just here to distinguish the behavior from FP removal, which'd include g
-int g_always_false_cond = 0;
-
 int main(void)
 {
   use_fg(0, get_f(), get_g());
@@ -34,9 +31,14 @@ int h(int x)
   return x / 2;
 }
 
+// Below we take the address of f, g, and h. Thus remove_function_pointers()
+// would create a case distinction involving f, g, and h in the function
+// use_fg() above.
+int always_false_cond = 0;
+
 fptr_t get_f(void)
 {
-  if(!g_always_false_cond)
+  if(!always_false_cond)
   {
     return f;
   }
@@ -48,7 +50,7 @@ fptr_t get_f(void)
 
 fptr_t get_g(void)
 {
-  if(!g_always_false_cond)
+  if(!always_false_cond)
   {
     return g;
   }

regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc

@@ -5,3 +5,7 @@ test.c
 \[use_fg.assertion.1\] line \d+ dereferenced function pointer at use_fg.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
+--
+--
+This test checks that the selected function pointer is replaced by a case
+distinction over both functions f and g.

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.c

@@ -25,37 +25,41 @@ int f(int x)
 {
   return x + 1;
 }
+
 int g(int x)
 {
   return x;
 }
+
 int h(int x)
 {
   return x - 1;
 }
 
-int g_select_function = 0;
+int select_function = 0;
 
 void select_f(void)
 {
-  g_select_function = 0;
+  select_function = 0;
 }
+
 void select_g(void)
 {
-  g_select_function = 1;
+  select_function = 1;
 }
+
 void select_h(void)
 {
-  g_select_function = 2;
+  select_function = 2;
 }
 
 fptr_t get_f(void)
 {
-  if(g_select_function == 0)
+  if(select_function == 0)
   {
     return f;
   }
-  else if(g_select_function == 1)
+  else if(select_function == 1)
   {
     return g;
   }

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc

@@ -7,3 +7,6 @@ g\(10\)
 ^SIGNAL=0$
 --
 h\(10\)
+--
+This test checks that no call to g appears in the goto program after the
+transformation by the restrict function pointer feature.

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.c

@@ -27,10 +27,12 @@ int f(int x)
 {
   return x + 1;
 }
+
 int g(int x)
 {
   return x;
 }
+
 int h(int x)
 {
   return x - 1;
@@ -42,10 +44,12 @@ void select_f(void)
 {
   g_select_function = 0;
 }
+
 void select_g(void)
 {
   g_select_function = 1;
 }
+
 void select_h(void)
 {
   g_select_function = 2;

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc

@@ -4,3 +4,15 @@ test.c
 \[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
 ^EXIT=10$
 ^SIGNAL=0$
+--
+--
+This test checks that multiple restrictions for a given function pointer can be
+given.
+
+The test further checks that the correct safety assertions are generated. The
+function pointer restriction feature outputs safety assertions for all calls
+that it replaces. That is, when it replaces a call with a case distinction over
+a given set of functions, it adds an assertion checking that in the original
+program, indeed no other function could have been called at that location. In
+this case, the function h could also be called, but the given restrictions only
+include f and g, hence the safety assertion fails.

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

@@ -27,37 +27,41 @@ int f(int x)
 {
   return x + 1;
 }
+
 int g(int x)
 {
   return x;
 }
+
 int h(int x)
 {
   return x - 1;
 }
 
-int g_select_function = 0;
+int select_function = 0;
 
 void select_f(void)
 {
-  g_select_function = 0;
+  select_function = 0;
 }
+
 void select_g(void)
 {
-  g_select_function = 1;
+  select_function = 1;
 }
+
 void select_h(void)
 {
-  g_select_function = 2;
+  select_function = 2;
 }
 
 fptr_t get_f(void)
 {
-  if(g_select_function == 0)
+  if(select_function == 0)
   {
     return f;
   }
-  else if(g_select_function == 1)
+  else if(select_function == 1)
   {
     return g;
   }

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

@@ -4,3 +4,15 @@ test.c
 \[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
 ^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 test further checks that the correct safety assertions are generated. The
+function pointer restriction feature outputs safety assertions for all calls
+that it replaces. That is, when it replaces a call with a case distinction over
+a given set of functions, it adds an assertion checking that in the original
+program, indeed no other function could have been called at that location. In
+this case, the function h could also be called, but the given restrictions only
+include f and g, hence the safety assertion fails.

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

@@ -27,37 +27,41 @@ int f(int x)
 {
   return x + 1;
 }
+
 int g(int x)
 {
   return x;
 }
+
 int h(int x)
 {
   return x - 1;
 }
 
-int g_select_function = 0;
+int select_function = 0;
 
 void select_f(void)
 {
-  g_select_function = 0;
+  select_function = 0;
 }
+
 void select_g(void)
 {
-  g_select_function = 1;
+  select_function = 1;
 }
+
 void select_h(void)
 {
-  g_select_function = 2;
+  select_function = 2;
 }
 
 fptr_t get_f(void)
 {
-  if(g_select_function == 0)
+  if(select_function == 0)
   {
     return f;
   }
-  else if(g_select_function == 1)
+  else if(select_function == 1)
   {
     return g;
   }

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

@@ -4,3 +4,15 @@ test.c
 \[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
 ^EXIT=10$
 ^SIGNAL=0$
+--
+--
+This test checks the reading of function pointer restrictions from a given json
+file.
+
+The test further checks that the correct safety assertions are generated. The
+function pointer restriction feature outputs safety assertions for all calls
+that it replaces. That is, when it replaces a call with a case distinction over
+a given set of functions, it adds an assertion checking that in the original
+program, indeed no other function could have been called at that location. In
+this case, the function h could also be called, but the given restrictions only
+include f and g, hence the safety assertion fails.