CONTRACTS: Allow NULL function pointers

regression/contracts-dfcc/function-pointer-contracts-enforce-1/main.c

@@ -0,0 +1,52 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+typedef int (*fun_t)(int);
+
+int add_one(int x)
+  __CPROVER_ensures(__CPROVER_return_value == __CPROVER_old(x) + 1);
+
+int foo(fun_t f_in, int x, fun_t *f_out)
+  // clang-format off
+__CPROVER_requires_contract(f_in, add_one, NULL)
+__CPROVER_assigns(f_out)
+__CPROVER_ensures(f_in ==>__CPROVER_return_value == __CPROVER_old(x) + 1)
+__CPROVER_ensures(!f_in ==>__CPROVER_return_value == __CPROVER_old(x))
+__CPROVER_ensures_contract(*f_out, add_one, NULL)
+// clang-format on
+{
+  *f_out = NULL;
+  if(f_in)
+  {
+    *f_out = f_in;
+    // this branch must be reachable
+    __CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
+  CALL_F_IN:
+    return f_in(x);
+  }
+  else
+  {
+    // this branch must be reachable
+    __CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
+    return x;
+  }
+}
+
+int main()
+{
+  fun_t f_in;
+  int x;
+  fun_t f_out;
+  foo(f_in, x, &f_out);
+  if(f_out)
+  {
+    __CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
+  CALL_F_OUT:
+    __CPROVER_assert(f_out(1) == 2, "f_out satisfies add_one");
+  }
+  else
+  {
+    __CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
+  }
+}

regression/contracts-dfcc/function-pointer-contracts-enforce-1/test.desc

@@ -0,0 +1,31 @@
+CORE
+main.c
+--restrict-function-pointer foo.CALL_F_IN/add_one --restrict-function-pointer main.CALL_F_OUT/add_one --dfcc main --enforce-contract foo
+main.c function foo
+^\[foo.postcondition.\d+\] line 14 Check ensures clause of contract contract::foo for function foo: SUCCESS$
+^\[foo.postcondition.\d+\] line 15 Check ensures clause of contract contract::foo for function foo: SUCCESS$
+^\[foo.postcondition.\d+\] line 16 Assert function pointer '\*f_out_wrapper' obeys contract 'add_one' or '\(fun_t\)NULL': SUCCESS$
+^\[foo.assigns.\d+\] line 19 Check that \*f_out is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 22 Check that \*f_out is assignable: FAILURE$
+^\[foo.assertion.\d+\] line 24 then branch is reachable, expecting FAILURE: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 26 dereferenced function pointer must be add_one: SUCCESS$
+^\[foo.assertion.\d+\] line 31 else branch is reachable, expecting FAILURE: FAILURE$
+^\[main.assertion.\d+\] line 44 then branch is reachable, expecting FAILURE: FAILURE$
+^\[main.assertion.\d+\] line 46 f_out satisfies add_one: SUCCESS$
+^\[main.pointer_dereference.\d+\] line 46 dereferenced function pointer must be add_one: SUCCESS$
+^\[main.assertion.\d+\] line 50 else branch is reachable, expecting FAILURE: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+foo requires that function pointer f_in satisfies the contract add_one or is NULL.
+When f_in is not NULL, foo calls f_in and the post condition of foo is that
+of add_one `__CPROVER_return_value == old(x) + 1`.
+When f_in is not NULL, foo returns x directly post condition of foo is that
+of add_one `__CPROVER_return_value == old(x)`.
+The function pointer f_out is ensured to satisfy the add_one contract or be NULL
+as a post condition.
+The main program calls f_out on a particular value if it is not null and asserts
+that the add_one post condition holds for a particular value.
+Assertions `assert(false)` are added to all branches to demonstrate reachability.

regression/contracts-dfcc/function-pointer-contracts-replace-1/main.c

@@ -0,0 +1,57 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+typedef int (*fun_t)(int);
+
+int add_one(int x)
+  __CPROVER_ensures(__CPROVER_return_value == __CPROVER_old(x) + 1);
+
+// returns either a pointer to a function that satisfies add_one or NULL
+fun_t get_add_one()
+  __CPROVER_ensures_contract(__CPROVER_return_value, add_one, NULL);
+
+int foo(int x, fun_t *f_out)
+  // clang-format off
+__CPROVER_assigns(*f_out)
+__CPROVER_ensures(
+  __CPROVER_return_value == __CPROVER_old(x) + 1 ||
+  __CPROVER_return_value == __CPROVER_old(x))
+__CPROVER_ensures_contract(*f_out, add_one, NULL)
+// clang-format on
+{
+  *f_out = NULL;
+  // obtain a pointer to a function that satisfies add_one;
+  fun_t f_in = get_add_one();
+  if(f_in)
+  {
+    *f_out = f_in;
+    // this branch must be reachable
+    __CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
+  CALL_F_IN:
+    return f_in(x);
+  }
+  else
+  {
+    // this branch must be reachable
+    __CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
+    return x;
+  }
+}
+
+int main()
+{
+  int x;
+  fun_t f_out;
+  foo(x, &f_out);
+  if(f_out)
+  {
+    __CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
+  CALL_F_OUT:
+    __CPROVER_assert(f_out(1) == 2, "f_out satisfies add_one");
+  }
+  else
+  {
+    __CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
+  }
+}

regression/contracts-dfcc/function-pointer-contracts-replace-1/test.desc

@@ -0,0 +1,28 @@
+CORE
+main.c
+--restrict-function-pointer foo.CALL_F_IN/add_one --restrict-function-pointer main.CALL_F_OUT/add_one --dfcc main --enforce-contract foo --replace-call-with-contract get_add_one
+^\[foo.postcondition.\d+\] line 18 Check ensures clause of contract contract::foo for function foo: SUCCESS$
+^\[foo.postcondition.\d+\] line 20 Assert function pointer '\*f_out_wrapper' obeys contract 'add_one' or '\(fun_t\)NULL': SUCCESS$
+^\[foo.assertion.\d+\] line 30 then branch is reachable, expecting FAILURE: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 32 dereferenced function pointer must be add_one: SUCCESS$
+^\[foo.assertion.\d+\] line 37 else branch is reachable, expecting FAILURE: FAILURE$
+^\[main.assertion.\d+\] line 49 then branch is reachable, expecting FAILURE: FAILURE$
+^\[main.assertion.\d+\] line 51 f_out satisfies add_one: SUCCESS$
+^\[main.pointer_dereference.\d+\] line 51 dereferenced function pointer must be add_one: SUCCESS$
+^\[main.assertion.\d+\] line 55 else branch is reachable, expecting FAILURE: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+foo obtains function pointer f_in through get_add_one, which is replaced by
+its contract.
+When f_in is not NULL, foo calls f_in and the post condition of foo is that
+of add_one `__CPROVER_return_value == old(x) + 1`.
+When f_in is not NULL, foo returns x directly post condition of foo is that
+of add_one `__CPROVER_return_value == old(x)`.
+The function pointer f_out is ensured to satisfy the add_one contract or be NULL
+as a post condition.
+The main program calls f_out on a particular value if it is not null and asserts
+that the add_one post condition holds for a particular value.
+Assertions `assert(false)` are added to all branches to demonstrate reachability.

regression/contracts/function-pointer-contracts-enforce/test.desc

@@ -1,9 +1,9 @@
 CORE
 main.c
 --enforce-contract foo --restrict-function-pointer foo.function_pointer_call.1/contract --replace-call-with-contract contract --replace-call-with-contract bar
-^EXIT=0$
+^file main.c line 23: require_contracts or ensures_contract clauses are not supported$
+^EXIT=6$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 --
 This test checks that we can require that a function pointer satisfies some named

regression/contracts/function-pointer-contracts-replace/test.desc

@@ -1,12 +1,9 @@
 CORE
 main.c
 --replace-call-with-contract foo
-^\[foo.precondition.\d+] line 19 Assert function pointer 'infun' obeys contract 'contract': SUCCESS$
-^\[main.assertion.\d+].* assertion outfun1 == contract: SUCCESS$
-^\[main.assertion.\d+].* assertion outfun2 == contract: SUCCESS$
-^EXIT=0$
+^file main.c line 19 function foo: require_contracts or ensures_contract clauses are not supported$
+^EXIT=6$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 --
 This test checks that, when replacing a call by its contract,

src/ansi-c/c_expr.h

@@ -329,11 +329,11 @@ class function_pointer_obeys_contract_exprt : public exprt
 public:
   explicit function_pointer_obeys_contract_exprt(
     exprt _function_pointer,
-    exprt _contract)
+    exprt _contract_pointers)
     : exprt(ID_function_pointer_obeys_contract, empty_typet{})
   {
     add_to_operands(std::move(_function_pointer));
-    add_to_operands(std::move(_contract));
+    add_to_operands(std::move(_contract_pointers));
   }
 
   static void check(
@@ -344,6 +344,13 @@ class function_pointer_obeys_contract_exprt : public exprt
       vm,
       expr.operands().size() == 2,
       "function pointer obeys contract expression must have two operands");
+
+    DATA_CHECK(
+      vm,
+      expr.operands()[1].id() == ID_expression_list,
+      "function pointer obeys contract expression second operand must be an "
+      "ID_expression_list expression, found " +
+        id2string(expr.operands()[1].id()));
   }
 
   static void validate(
@@ -364,24 +371,14 @@ class function_pointer_obeys_contract_exprt : public exprt
     return op0();
   }
 
-  const symbol_exprt &contract_symbol_expr() const
-  {
-    return to_symbol_expr(op1().operands().at(0));
-  }
-
-  symbol_exprt &contract_symbol_expr()
+  const exprt::operandst &contract_pointers() const
   {
-    return to_symbol_expr(op1().operands().at(0));
-  }
-
-  const exprt &address_of_contract() const
-  {
-    return op1();
+    return op1().operands();
   }
 
-  exprt &address_of_contract()
+  exprt::operandst &contract_pointers()
   {
-    return op1();
+    return op1().operands();
   }
 };