CONTRACTS: add __CPROVER_obeys_contract predicate

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.

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

@@ -0,0 +1,38 @@
+#include <assert.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
+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
+  ;
+
+arr_fun_t foo(arr_fun_t infun, arr_fun_t *outfun)
+  // clang-format off
+__CPROVER_requires(__CPROVER_obeys_contract(infun, arr_fun_contract))
+__CPROVER_ensures(__CPROVER_obeys_contract(*outfun, arr_fun_contract))
+__CPROVER_ensures(__CPROVER_obeys_contract(__CPROVER_return_value, arr_fun_contract))
+// clang-format on
+{
+  *outfun = arr_fun_contract;
+  return infun;
+}
+
+void main()
+{
+  // establish pre-conditions before replacement
+  arr_fun_t infun = arr_fun_contract;
+
+  arr_fun_t outfun1 = NULL;
+  arr_fun_t outfun2 = foo(infun, &outfun1);
+
+  // checking post-conditions after replacement
+  assert(outfun1 == arr_fun_contract);
+  assert(outfun2 == arr_fun_contract);
+}

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

@@ -0,0 +1,14 @@
+CORE
+main.c
+--dfcc main --replace-call-with-contract foo
+^\[main.assertion.\d+\].*assertion outfun1 == arr_fun_contract: SUCCESS$
+^\[main.assertion.\d+\].*assertion outfun2 == arr_fun_contract: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that, when replacing a call by its contract,
+requires_contract clauses are translated to equality checks
+and that ensures_contract are translated to assignments of the function pointer
+variable to the contract symbol.

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

@@ -0,0 +1,66 @@
+#include <stdlib.h>
+
+// Type of functions that manipulate arrays of a given size
+typedef void (*arr_fun_t)(char *arr, size_t size);
+
+// A contract for the arr_fun_t type
+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
+  ;
+
+// Uses a function pointer
+int foo(char *arr, size_t size, arr_fun_t arr_fun)
+  // clang-format off
+__CPROVER_requires(arr ==> __CPROVER_is_fresh(arr, size))
+__CPROVER_requires(
+  arr_fun ==> __CPROVER_obeys_contract(arr_fun, arr_fun_contract))
+__CPROVER_assigns(arr && size > 0 && arr_fun: arr[0])
+__CPROVER_ensures(__CPROVER_return_value ==> (arr[0] == 0))
+// clang-format on
+{
+  if(arr && size > 0 && arr_fun)
+  {
+  CALL:
+    arr_fun(arr, size);
+    return 1;
+  }
+  return 0;
+}
+
+// returns function pointer satisfying arr_fun_contract
+arr_fun_t get_arr_fun()
+  // clang-format off
+__CPROVER_ensures(
+  __CPROVER_obeys_contract(__CPROVER_return_value, arr_fun_contract))
+  // clang-format on
+  ;
+
+// allocates an array and uses get_arr_fun and foo to initialise it
+char *bar(size_t size)
+  // clang-format off
+__CPROVER_ensures(
+  __CPROVER_return_value ==> size > 0 &&
+  __CPROVER_is_fresh(__CPROVER_return_value, size) &&
+  __CPROVER_return_value[0] == 0)
+// clang-format on
+{
+  if(size > 0)
+  {
+    char *arr;
+    arr = malloc(size);
+    if(arr && foo(arr, size, get_arr_fun()))
+      return arr;
+
+    return NULL;
+  }
+  return NULL;
+}
+
+void main()
+{
+  size_t size;
+  char *arr = bar(size);
+}

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

@@ -0,0 +1,11 @@
+CORE
+main.c
+--dfcc main --enforce-contract bar --replace-call-with-contract foo --replace-call-with-contract get_arr_fun
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks that when a function returning a function pointer satisfying a given
+contract is replaced by its contract, the returned function pointer can be
+passed to another function requiring the same contract.

regression/contracts-dfcc/function-pointer-contracts-typecheck-error-1/main.c

@@ -0,0 +1,21 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+// type of functions that manipulate arrays
+typedef void (*fun_t)(char *arr, size_t size);
+
+void contract(char *arr, size_t size);
+
+int foo(char *arr, size_t size, fun_t fun)
+  __CPROVER_requires(__CPROVER_obeys_contract(fun, contract, contract))
+{
+  return 0;
+}
+
+void main()
+{
+  size_t size;
+  char *arr;
+  fun_t fun;
+  foo(arr, size, fun);
+}

regression/contracts-dfcc/function-pointer-contracts-typecheck-error-1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo
+^.*error: expected 2 arguments for __CPROVER_obeys_contract, found 3$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that malformed __CPROVER_obeys_contract predicate expressions are rejected.

regression/contracts-dfcc/function-pointer-contracts-typecheck-error-2/main.c

@@ -0,0 +1,21 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+// type of functions that manipulate arrays
+typedef void (*fun_t)(char *arr, size_t size);
+
+void contract(char *arr, size_t size);
+
+int foo(char *arr, size_t size, fun_t fun)
+  __CPROVER_requires(__CPROVER_obeys_contract(true ? fun : fun, contract))
+{
+  return 0;
+}
+
+void main()
+{
+  size_t size;
+  char *arr;
+  fun_t fun;
+  foo(arr, size, fun);
+}

regression/contracts-dfcc/function-pointer-contracts-typecheck-error-2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo
+^.*error: the first argument of __CPROVER_obeys_contract must have no ternary operator$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that malformed __CPROVER_obeys_contract predicate expressions are rejected.

regression/contracts-dfcc/function-pointer-contracts-typecheck-error-3/main.c

@@ -0,0 +1,28 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+// type of functions that manipulate arrays
+typedef void (*fun_t)(char *arr, size_t size);
+
+void contract(char *arr, size_t size);
+
+typedef void (*voidfun_t)(void);
+
+voidfun_t identity(voidfun_t fun)
+{
+  return fun;
+}
+
+int foo(char *arr, size_t size, fun_t fun)
+  __CPROVER_requires(__CPROVER_obeys_contract(identity(fun), contract))
+{
+  return 0;
+}
+
+void main()
+{
+  size_t size;
+  char *arr;
+  fun_t fun;
+  foo(arr, size, fun);
+}

regression/contracts-dfcc/function-pointer-contracts-typecheck-error-3/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo
+^.*error: the first argument of __CPROVER_obeys_contract must be a function pointer lvalue expression$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that malformed __CPROVER_obeys_contract predicate expressions are rejected.

regression/contracts-dfcc/function-pointer-contracts-typecheck-error-4/main.c

@@ -0,0 +1,28 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+// type of functions that manipulate arrays
+typedef void (*fun_t)(char *arr, size_t size);
+
+void contract(char *arr, size_t size, bool b);
+
+typedef void (*voidfun_t)(void);
+
+voidfun_t identity(voidfun_t fun)
+{
+  return fun;
+}
+
+int foo(char *arr, size_t size, fun_t fun)
+  __CPROVER_requires(__CPROVER_obeys_contract(fun, contract))
+{
+  return 0;
+}
+
+void main()
+{
+  size_t size;
+  char *arr;
+  fun_t fun;
+  foo(arr, size, fun);
+}

regression/contracts-dfcc/function-pointer-contracts-typecheck-error-4/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo
+^.*error: the first and second arguments of __CPROVER_obeys_contract must have the same function pointer type$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that malformed __CPROVER_obeys_contract predicate expressions are rejected.

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

@@ -0,0 +1,44 @@
+#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)
+;
+
+// 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/function-pointer-contracts-enforce/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo --restrict-function-pointer foo.CALL/arr_fun_contract --replace-call-with-contract arr_fun_contract
+^file main.c line 23 function foo: __CPROVER_obeys_contract is not supported in this version
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+This test checks uses of the unsupported __CPROVER_obeys_contract predicate
+trigger errors.