Adds test to cover contracts and function pointers support

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/contracts_with_function_pointers/main.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+#include <stddef.h>
+
+int x = 0;
+
+void foo(int *y)
+{
+  *y = 1;
+}
+
+int *baz()
+{
+  return &x;
+}
+
+void bar(void (*fun_ptr)(), int *x) __CPROVER_requires(fun_ptr != NULL)
+  __CPROVER_requires(x != NULL) __CPROVER_assigns(*x) __CPROVER_ensures(*x == 1)
+{
+  *(baz()) = 1;
+  fun_ptr(x);
+}
+
+int main()
+{
+  assert(x == 0);
+  void (*fun_ptr)() = foo;
+  bar(fun_ptr, &x);
+  assert(x == 1);
+  return 0;
+}

regression/contracts/contracts_with_function_pointers/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-contract bar
+^EXIT=0$
+^SIGNAL=0$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[bar.\d+\] line \d+ Check that \*return\_value\_baz is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+Checks whether CBMC properly instrument functions with function pointers
+during contract enforcement.

src/goto-instrument/contracts/contracts.cpp

@@ -673,19 +673,8 @@ void code_contractst::instrument_call_statement(
     "The first argument of instrument_call_statement should always be "
     "a function call");
 
-  irep_idt called_function;
-  if(instruction_it->call_function().id() == ID_dereference)
-  {
-    called_function =
-      to_symbol_expr(
-        to_dereference_expr(instruction_it->call_function()).pointer())
-        .get_identifier();
-  }
-  else
-  {
-    called_function =
-      to_symbol_expr(instruction_it->call_function()).get_identifier();
-  }
+  irep_idt called_function =
+    to_symbol_expr(instruction_it->call_function()).get_identifier();
 
   if(called_function == "malloc")
   {