Adds test to code contracts regression

New test checks whether CBMC properly verify function contracts
with functions. At this point, we still don't check for purity,
i.e., if functions in contracts are only predicates.

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/assigns_enforce_functions_in_contracts/header.h

@@ -0,0 +1,11 @@
+#include "utility.h"
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(int *x) __CPROVER_requires(s2n_result_is_ok(validity3(x)))
+  __CPROVER_assigns(*x) __CPROVER_ensures(
+    __CPROVER_return_value == *x + 5 && s2n_result_is_ok(validity3(x)))
+{
+  *x = *x + 0;
+  return *x + 5;
+}

regression/contracts/assigns_enforce_functions_in_contracts/main.c

@@ -0,0 +1,9 @@
+#include "header.h"
+
+int main()
+{
+  int *n = malloc(sizeof(*n));
+  *n = foo(n);
+
+  return 0;
+}

regression/contracts/assigns_enforce_functions_in_contracts/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks whether verification succeeds when requires and ensures
+contain functions.
+
+Note: We still don't check for function purity, i.e.,
+functions in contracts must only work as predicates.

regression/contracts/assigns_enforce_functions_in_contracts/utility.h

@@ -0,0 +1,40 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+/* Function return code  */
+#define S2N_SUCCESS 0
+#define S2N_FAILURE -1
+
+/* A value which indicates the outcome of a function */
+typedef struct
+{
+  int __error_signal;
+} s2n_result;
+
+#define S2N_RESULT s2n_result
+#define S2N_RESULT_OK ((s2n_result){S2N_SUCCESS})
+#define S2N_RESULT_ERROR ((s2n_result){S2N_FAILURE})
+
+bool s2n_result_is_ok(s2n_result result)
+{
+  return result.__error_signal == S2N_SUCCESS;
+}
+
+bool validity1(int *x)
+{
+  return (x > 0);
+}
+
+bool validity2(int *x)
+{
+  return (x == 0);
+}
+
+S2N_RESULT validity3(int *x)
+{
+  if(x == NULL)
+    return S2N_RESULT_ERROR;
+  if(!validity1(x))
+    return S2N_RESULT_ERROR;
+  return S2N_RESULT_OK;
+}