Merge pull request #7150 from tautschnig/bugfixes/7135-empty-reason

Function pointer restrictions: fix empty reason in error reporting

Author: kroening

regression/goto-instrument/restrict-function-pointer-error-reporting/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int foo()
+{
+  return 10;
+}
+
+int bar()
+{
+  return 5;
+}
+
+int main()
+{
+  int (*fun_ptr)() = nondet_bool() ? &foo : &bar;
+  assert(fun_ptr() == 10);
+}

regression/goto-instrument/restrict-function-pointer-error-reporting/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--restrict-function-pointer fun_ptr.function_pointer_call.1/foo
+^Reason: fun_ptr.function_pointer_call.1 not found in the symbol table$
+^EXIT=1$
+^SIGNAL=0$
+--
+^Reason:\s*$
+--
+This test checks that invalid usage results in meaningful error reports.

src/goto-programs/restrict_function_pointers.cpp

@@ -485,7 +485,9 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options(
   catch(const invalid_restriction_exceptiont &e)
   {
     throw invalid_command_line_argument_exceptiont{
-      e.reason, "--" RESTRICT_FUNCTION_POINTER_OPT, e.correct_format};
+      static_cast<cprover_exception_baset>(e).what(),
+      "--" RESTRICT_FUNCTION_POINTER_OPT,
+      e.correct_format};
   }
 
   restrictionst file_restrictions;
@@ -514,7 +516,9 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options(
   catch(const invalid_restriction_exceptiont &e)
   {
     throw invalid_command_line_argument_exceptiont{
-      e.reason, "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT, e.correct_format};
+      static_cast<cprover_exception_baset>(e).what(),
+      "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT,
+      e.correct_format};
   }
 
   return {merge_function_pointer_restrictions(

src/goto-programs/restrict_function_pointers.h

@@ -79,7 +79,6 @@ class invalid_restriction_exceptiont : public cprover_exception_baset
 
   std::string what() const override;
 
-  std::string reason;
   std::string correct_format;
 };