Merge pull request #5220 from karkhaz/kk-fix-ignored-return-contract

Revamp function contracts command line interface

Author: chrisr-diffblue

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/ignored_return_value/main.c

@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+int get_at_idx(int const *const arr, const size_t len, const size_t idx)
+  __CPROVER_requires(__CPROVER_r_ok(arr, len) && idx < len)
+    __CPROVER_ensures(__CPROVER_return_value == arr[idx])
+{
+  return arr[idx];
+}
+
+void main()
+{
+  int a[5] = {0};
+  get_at_idx(a, 5, 3);
+}

regression/contracts/ignored_return_value/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test exposes a bug where CBMC would crash on a program where a function
+with a return value has a postcondition that mentions __CPROVER_return_value,
+but the caller does not assign the return value to anything.

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$

regression/contracts/used_return_value/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int get_at_idx(int const *const arr, const size_t len, const size_t idx)
+  __CPROVER_requires(__CPROVER_r_ok(arr, len) && idx < len)
+    __CPROVER_ensures(__CPROVER_return_value == arr[idx])
+{
+  return arr[idx];
+}
+
+void main()
+{
+  int a[5] = {0};
+  a[3] = 7;
+  int x = get_at_idx(a, 5, 3);
+  assert(x == 7);
+}

regression/contracts/used_return_value/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--