Revamp function contracts interface

This commit adds four new flags to goto-instrument that allow CBMC to
check or take advantage of function contracts in the target codebase.
It prepares for a series of commits that will improve the soundness of
this functionality and add support for loop invariants.

The motivation behind this patch series is to improve scalability of
code verification. Given the following code:

  foo()
  __CPROVER_ensures(P)
  __CPROVER_ensures(Q)
  { ... }

  bar()
  {
    foo();
  }

the user can pass `--replace-call-with-contract foo` to goto-instrument,
which will change the body of `bar` so that it can be verified more
scalably:

  bar()
  {
    assert(P);
    assume(Q);
  }

The user should then separately pass `--enforce-contract foo` to
goto-instrument. This instruments `foo` so that it looks like this:

  foo()
  {
    assume(P);
    // original body
    assert(Q);
  }

Running `cbmc --function foo` on the instrumented binary then checks
that `foo` actually abides by its contract, regardless of its calling
context.

Users can also pass `--enforce-all-contracts` and
`--replace-all-calls-with-contracts` to avoid naming every function.

Author: karkhaz

regression/contracts/CMakeLists.txt

@@ -1,7 +1,7 @@
 if(WIN32)
-    set(is_windows true)
+  set(is_windows true)
 else()
-    set(is_windows false)
+  set(is_windows false)
 endif()
 
 add_test_pl_tests(

regression/contracts/function_apply_01/main.c

@@ -6,8 +6,7 @@
 
 #include <assert.h>
 
-int foo() 
-  __CPROVER_ensures(__CPROVER_return_value == 0)
+int foo() __CPROVER_ensures(__CPROVER_return_value == 0)
 {
   return 1;
 }

regression/contracts/function_apply_01/test.desc

@@ -1,9 +1,12 @@
-KNOWNBUG
+CORE
 main.c
---apply-code-contracts
+--replace-all-calls-with-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+^warning: ignoring
 --
-Applying code contracts currently also checks them.
+This code is purposely unsound (the function does not abide by its
+contract). Verifying the function in isolation should fail, and
+verifying its caller should succeed.

regression/contracts/function_check_01/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-code-contracts
 ^EXIT=0$

regression/contracts/function_check_04/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-code-contracts
 ^EXIT=10$

regression/contracts/function_no_apply_01/main.c

@@ -0,0 +1,19 @@
+// function_apply_01
+
+// Note that this test is supposed to have an incorrect contract.
+// We verify that applying (without checking) the contract yields success,
+// and that checking the contract yields failure.
+
+#include <assert.h>
+
+int foo() __CPROVER_ensures(__CPROVER_return_value == 0)
+{
+  return 1;
+}
+
+int main()
+{
+  int x = foo();
+  assert(x == 0);
+  return 0;
+}

regression/contracts/function_no_apply_01/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] line 17 assertion x == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+We don't actually replace the function call with its contract here, so
+CBMC should notice that the program is unsound.

regression/contracts/invar_check_01/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-code-contracts
 ^EXIT=0$

regression/contracts/invar_check_02/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-code-contracts
 ^EXIT=0$

regression/contracts/invar_check_03/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-code-contracts
 ^EXIT=0$

regression/contracts/invar_check_04/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-code-contracts
 ^EXIT=10$