Merge pull request #7355 from remi-delmas-3000/obeys-contract-predicate

CONTRACTS: add __CPROVER_obeys_contract predicate

Author: remi-delmas-3000

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

@@ -0,0 +1,45 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+// type of functions that manipulate arrays
+typedef void (*arr_fun_t)(char *arr, size_t size);
+
+// A contract for the arr_fun_t type
+// requires a fresh array and positive size
+// resets the first element to zero
+void arr_fun_contract(char *arr, size_t size)
+  // clang-format off
+__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(arr[0])
+__CPROVER_ensures(arr[0] == 0)
+  // clang-format on
+  ;
+
+// Testing pre-conditions constructs
+// Takes a function pointer as input, uses it if its preconditions are met
+// to establish post-conditions
+int foo(char *arr, size_t size, arr_fun_t arr_fun)
+  // clang-format off
+__CPROVER_requires(arr == NULL || __CPROVER_is_fresh(arr, size))
+__CPROVER_requires(__CPROVER_obeys_contract(arr_fun, arr_fun_contract))
+__CPROVER_assigns(arr && size > 0 : arr[0])
+__CPROVER_ensures((__CPROVER_return_value == 0) ==> (arr[0] == 0))
+// clang-format on
+{
+  int retval = -1;
+  if(arr && size > 0)
+  {
+  CALL:
+    arr_fun(arr, size);
+    retval = 0;
+  }
+  return retval;
+}
+
+void main()
+{
+  size_t size;
+  char *arr;
+  arr_fun_t fun;
+  foo(arr, size, fun);
+}

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

@@ -0,0 +1,12 @@
+CORE
+main.c
+--restrict-function-pointer foo.CALL/arr_fun_contract --dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks that when a function taking a function pointer as input satisfying a given
+contract is checked against its contract, the function pointer can be called
+like a regular function pointer and establishes the post conditions specified
+by its contract.