New test checking that __CPROVER_havoc_object are detected as writes by assigns clause checking

Author: Remi Delmas

regression/contracts/assigns_enforce_havoc_object/main.c

@@ -0,0 +1,59 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int x = 0;
+typedef struct stc
+{
+  int i;
+  int j;
+} stc;
+
+typedef struct stb
+{
+  stc *c;
+} stb;
+
+typedef struct sta
+{
+  union {
+    stb *b;
+    int i;
+    int j;
+  } u;
+} sta;
+
+int nondet_int();
+
+void bar(sta *a)
+{
+  if(nondet_bool())
+    return;
+  __CPROVER_havoc_object(a->u.b->c);
+  return;
+}
+
+void foo(sta *a1, sta *a2)
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a1->u.b->c))
+{
+  bar(a1);
+  bar(a2);
+  return;
+}
+
+sta *allocate_sta()
+{
+  stc *c = malloc(sizeof(*c));
+  stb *b = malloc(sizeof(*b));
+  sta *a = malloc(sizeof(*a));
+  b->c = c;
+  a->u.b = b;
+  return a;
+}
+
+int main()
+{
+  sta *a1 = allocate_sta();
+  sta *a2 = allocate_sta();
+  foo(a1, a2);
+  return 0;
+}

regression/contracts/assigns_enforce_havoc_object/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=10$
+^SIGNAL=0$
+^\[bar.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: SUCCESS$
+^\[bar.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks that __CPROVER_havoc_object(x) is detected as a write to POINTER_OBJECT(x).