Adding more tests on what expressions shall be accepted/rejected in assigns clauses.

Author: Remi Delmas

regression/contracts/assigns_enforce_address_of/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(int *x) __CPROVER_assigns(&x)
+{
+  *x = 0;
+  return 0;
+}
+
+int main()
+{
+  int x;
+  foo(&x);
+  return 0;
+}

regression/contracts/assigns_enforce_address_of/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=(1|64)$
+^SIGNAL=0$
+^.*error: illegal target in assigns clause$
+^CONVERSION ERROR$
+--
+--
+Check that address_of expressions are rejected in assigns clauses.

regression/contracts/assigns_enforce_elvis_1/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(bool a, int *x, int *y, int *z) __CPROVER_assigns(*(a ? x : y))
+{
+  if(a)
+    *x = 0; // must pass
+  else
+    *y = 0; // must pass
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+  int z;
+
+  foo(a, &x, &y, &z);
+  return 0;
+}

regression/contracts/assigns_enforce_elvis_1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+main.c function foo
+^\[foo.1] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo.2] line \d+ Check that \*y is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Check that Elvis operator expressions '*(cond ? if_true : if_false)' are accepted in assigns clauses and work as expected.

regression/contracts/assigns_enforce_elvis_2/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(bool a, int *x, int *y, int *z) __CPROVER_assigns(*(a ? x : y))
+{
+  if(a)
+    *x = 0; // must pass
+  else
+    *z = 0; // must fail
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+  int z;
+
+  foo(a, &x, &y, &z);
+  return 0;
+}

regression/contracts/assigns_enforce_elvis_2/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=10$
+^SIGNAL=0$
+main.c function foo
+^\[foo.1] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo.2] line \d+ Check that \*z is assignable: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Check that Elvis operator expressions '*(cond ? if_true : if_false)' are accepted in assigns clauses and work as expected.

regression/contracts/assigns_enforce_elvis_3/main.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(bool a, int *x, int *y, int *z) __CPROVER_assigns(*(a ? x : y))
+{
+  if(a)
+  {
+    *x = 0; // must pass
+  }
+  else
+  {
+    // must pass because in the context of main, this branch is dead
+    // so foo never attempts to write to *z.
+    *z = 0;
+  }
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+  int z;
+
+  foo(true, &x, &y, &z);
+  return 0;
+}

regression/contracts/assigns_enforce_elvis_3/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+main.c function foo
+^\[foo.1] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo.2] line \d+ Check that \*z is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Check that Elvis operator expressions '*(cond ? if_true : if_false)' are accepted in assigns clauses.

regression/contracts/assigns_enforce_elvis_4/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(bool a, int *x, long long *y) __CPROVER_assigns(*(a ? x : y))
+{
+  if(a)
+  {
+    *x = 0;
+  }
+  else
+  {
+    *y = 0;
+  }
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  long y;
+
+  foo(true, &x, &y);
+  return 0;
+}

regression/contracts/assigns_enforce_elvis_4/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=(1|64)$
+^SIGNAL=0$
+^.*error: void-typed targets not permitted$
+--
+--
+Check that Elvis operator expressions '*(cond ? if_true : if_false)' with different types in true and false branches are rejected.