add three contract tests

Author: kroening

regression/cprover/contracts/check_assigns4.c

@@ -0,0 +1,29 @@
+struct S
+{
+  int x, y;
+} global;
+
+void my_function1(void)
+  __CPROVER_assigns(global) // passes
+{
+  global.x = 10;
+  global.y = 10;
+}
+
+void my_function2(void)
+  __CPROVER_assigns(global.x) // passes
+{
+  global.x = 10;
+}
+
+void my_function3(void)
+  __CPROVER_assigns(global.y) // passes
+{
+  global.y = 10;
+}
+
+void my_function4(void)
+  __CPROVER_assigns(global.y) // fails
+{
+  global.x = 10;
+}

regression/cprover/contracts/check_assigns4.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+check_assigns4.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[my_function1\.assigns\.1\] line \d+ assigns clause: SUCCESS$
+^\[my_function1\.assigns\.2\] line \d+ assigns clause: SUCCESS$
+^\[my_function2\.assigns\.1\] line \d+ assigns clause: SUCCESS$
+^\[my_function3\.assigns\.1\] line \d+ assigns clause: SUCCESS$
+^\[my_function4\.assigns\.1\] line \d+ assigns clause: REFUTED$
+--

regression/cprover/contracts/check_assigns5.c

@@ -0,0 +1,29 @@
+struct S
+{
+  int x, y;
+};
+
+void my_function1(struct S *s)
+  __CPROVER_assigns(*s) // passes
+{
+  s->x = 10;
+  s->y = 10;
+}
+
+void my_function2(struct S *s)
+  __CPROVER_assigns(s->x) // passes
+{
+  s->x = 10;
+}
+
+void my_function3(struct S *s)
+  __CPROVER_assigns(s->y) // passes
+{
+  s->y = 10;
+}
+
+void my_function4(struct S *s)
+  __CPROVER_assigns(s->y) // fails
+{
+  s->x = 10;
+}

regression/cprover/contracts/check_assigns5.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+check_assigns5.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[my_function1\.assigns\.1\] line \d+ assigns clause: SUCCESS$
+^\[my_function1\.assigns\.2\] line \d+ assigns clause: SUCCESS$
+^\[my_function2\.assigns\.1\] line \d+ assigns clause: SUCCESS$
+^\[my_function3\.assigns\.1\] line \d+ assigns clause: SUCCESS$
+^\[my_function4\.assigns\.1\] line \d+ assigns clause: REFUTED$
+--

regression/cprover/contracts/check_assigns6.c

@@ -0,0 +1,15 @@
+int global;
+_Bool flag;
+
+void my_function1()
+  __CPROVER_assigns(flag: global) // passes
+{
+  if(flag)
+    global = 10;
+}
+
+void my_function2()
+  __CPROVER_assigns(flag: global) // fails
+{
+  global = 10;
+}

regression/cprover/contracts/check_assigns6.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+check_assigns6.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[my_function1\.assigns\.1\] line \d+ assigns clause: SUCCESS$
+^\[my_function2\.assigns\.1\] line \d+ assigns clause: REFUTED$
+--