CONTRACTS: store contracts in dedicated symbols

Contracts can now be placed on declarations or definitions, and result
in a fresh symbol being generated. That new symbol has its name prefixed
with "contracts::" to place them in a pseudo-namespace, and has
"is_property" set (which was an otherwise unused symbolt flag).

Co-authored-by: Remi Delmas <[email protected]>

Author: tautschnig

regression/contracts/named-contracts/main-contract-after-declaration.c

@@ -0,0 +1,28 @@
+int foo(int *arr, int size);
+
+int foo(int *arr, int size)
+  // clang-format off
+__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(
+  arr[0], arr[size-1];
+  size >= 10: arr[5];
+)
+__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0)
+__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value)
+  // clang-format on
+  ;
+
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/contracts/named-contracts/main-contract-after-definition.c

@@ -0,0 +1,26 @@
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  return size < 10 ? 0 : arr[5];
+}
+
+int foo(int *arr, int size)
+  // clang-format off
+__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(
+  arr[0], arr[size-1];
+  size >= 10: arr[5];
+)
+__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0)
+__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value)
+  // clang-format on
+  ;
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/contracts/named-contracts/main-contract-incomplete.c

@@ -0,0 +1,22 @@
+int foo(int *arr, int size);
+
+int foo()
+  // clang-format off
+__CPROVER_ensures(__CPROVER_return_value != 0)
+  // clang-format on
+  ;
+
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/contracts/named-contracts/main-contract-signature-conflict.c

@@ -0,0 +1,30 @@
+int foo(int *arr, int size);
+
+#if 0
+int foo()
+  // clang-format off
+__CPROVER_ensures(__CPROVER_return_value != 0)
+  // clang-format on
+  ;
+#endif
+
+void foo(int *arr, int size)
+  // clang-format off
+__CPROVER_requires(size > 0)
+  // clang-format on
+  ;
+
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/contracts/named-contracts/main-definition-after-contract.c

@@ -0,0 +1,26 @@
+int foo(int *arr, int size)
+  // clang-format off
+__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(
+  arr[0], arr[size-1];
+  size >= 10: arr[5];
+)
+__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0)
+__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value)
+  // clang-format on
+  ;
+
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/contracts/named-contracts/main-no-definition.c

@@ -0,0 +1,28 @@
+int foo(int *arr, int size)
+  // clang-format off
+__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(
+  arr[0], arr[size-1];
+  size >= 10: arr[5];
+)
+__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0)
+__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value)
+  // clang-format on
+  ;
+
+int main()
+{
+  int arr[10] = {10, 9, 8, 7, 6, 5, 4, 3, 2, 1};
+  int retval = foo(arr, 10);
+  assert(arr[0] == 0);
+  assert(arr[1] == 9);
+  assert(arr[2] == 8);
+  assert(arr[3] == 7);
+  assert(arr[4] == 6);
+  assert(arr[5] == retval);
+  assert(arr[6] == 4);
+  assert(arr[7] == 3);
+  assert(arr[8] == 2);
+  assert(arr[9] == 0);
+  return 0;
+}

regression/contracts/named-contracts/test-contract-after-declaration.desc

@@ -0,0 +1,10 @@
+CORE
+main-contract-after-declaration.c
+--replace-call-with-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can have a function declaration with a contract after
+having seen an earlier declaration of that same function.

regression/contracts/named-contracts/test-contract-after-definition.desc

@@ -0,0 +1,10 @@
+CORE
+main-contract-after-definition.c
+--replace-call-with-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can have a function declaration with a contract after
+having seen that function's definition.

regression/contracts/named-contracts/test-contract-incomplete.desc

@@ -0,0 +1,10 @@
+CORE
+main-contract-incomplete.c
+
+error: code contract on incomplete function re-declaration
+CONVERSION ERROR
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+This test checks that contracts on incomplete re-declarations are rejected.

regression/contracts/named-contracts/test-contract-signature-conflict.desc

@@ -0,0 +1,10 @@
+CORE
+main-contract-signature-conflict.c
+--enforce-contract foo
+^Contract of 'foo' has different signature\.$
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+This test checks that contracts on function declarations with a matching name
+but different type are rejected.

regression/contracts/named-contracts/test-definition-after-contract.desc

@@ -0,0 +1,11 @@
+CORE
+main-definition-after-contract.c
+--replace-call-with-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can have a function declaration with a contract and
+without body, then the function definition, and successfully replace a call to
+the function by the contract.

regression/contracts/named-contracts/test-no-definition.desc

@@ -0,0 +1,10 @@
+CORE
+main-no-definition.c
+--replace-call-with-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can have a function declaration with a contract and
+without body and replace a call to the function by the contract.