new test

Author: Remi Delmas

regression/contracts-dfcc/user-defined-memory-predicates-replace/main.c

@@ -0,0 +1,94 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+typedef struct list_t
+{
+  int value;
+  struct list_t *next;
+} list_t;
+
+// true iff list of len max_len with values in [-10,10]
+bool is_list(list_t *l, size_t len)
+{
+  if(len == 0)
+    return l == NULL;
+  else
+    return __CPROVER_is_fresh(l, sizeof(*l)) &&
+           (-10 <= l->value && l->value <= 10) && is_list(l->next, len - 1);
+}
+
+typedef struct buffer_t
+{
+  size_t size;
+  char *arr;
+  char *cursor;
+} buffer_t;
+
+typedef struct double_buffer_t
+{
+  buffer_t *first;
+  buffer_t *second;
+} double_buffer_t;
+
+bool is_sized_array(char *arr, size_t size)
+{
+  return __CPROVER_is_fresh(arr, size);
+}
+
+bool is_ranged_cursor(char *cursor, char *arr, size_t size)
+{
+  void *lb = arr;
+  void *ub = arr + size;
+  return __CPROVER_pointer_in_range_dfcc(lb, cursor, ub);
+}
+
+bool is_buffer(buffer_t *b)
+{
+  return __CPROVER_is_fresh(b, sizeof(*b)) && (0 < b->size && b->size <= 10) &&
+         is_sized_array(b->arr, b->size) &&
+         is_ranged_cursor(b->cursor, b->arr, b->size);
+}
+
+bool is_double_buffer(double_buffer_t *b)
+{
+  return __CPROVER_is_fresh(b, sizeof(*b)) && is_buffer(b->first) &&
+         is_buffer(b->second);
+}
+
+int bar(list_t *l)
+  // clang-format off
+  __CPROVER_requires(is_list(l, 3))
+  __CPROVER_ensures(-30 <= __CPROVER_return_value &&
+                    __CPROVER_return_value <= 30)
+// clang-format on
+{
+  return l->value + l->next->value + l->next->next->value;
+}
+
+int baz(double_buffer_t *b)
+  // clang-format off
+  __CPROVER_requires(is_double_buffer(b))
+  __CPROVER_ensures(2 <= __CPROVER_return_value &&
+                    __CPROVER_return_value <= 20)
+// clang-format on
+{
+  return b->first->size + b->second->size;
+}
+
+int foo(list_t *l, double_buffer_t *b)
+  // clang-format off
+  __CPROVER_requires(is_list(l, 3))
+  __CPROVER_requires(is_double_buffer(b))
+  __CPROVER_ensures(-28 <= __CPROVER_return_value &&
+                    __CPROVER_return_value <= 50)
+// clang-format on
+{
+  return bar(l) + baz(b);
+}
+
+int main()
+{
+  list_t *l;
+  double_buffer_t *b;
+  int return_value = foo(l, b);
+}

regression/contracts-dfcc/user-defined-memory-predicates-replace/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks if user-defined predicates work;