Merge pull request #4944 from smowton/smowton/admin/field-sensitivity-tests

Add field-sensitivity tests

Author: smowton

regression/cbmc/field-sensitivity1/test.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a;
+  a.x = argc;
+  a.y = argc + 1;
+  assert(a.x == argc);
+}

regression/cbmc/field-sensitivity1/test.desc

@@ -0,0 +1,13 @@
+CORE
+test.c
+--show-vcc
+main::1::a!0@1#2\.\.x = main::argc!0@1#1
+main::1::a!0@1#2\.\.y = 1 \+ main::argc!0@1#1
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a!\d+@\d+#\d+\.x
+main::1::a!\d+@\d+#\d+\.y
+--
+Fields A::x and A::y should be referred to as atomic symbols (a..x and a..y) but not using
+member operators (a.x and a.y).

regression/cbmc/field-sensitivity10/test.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+  int z;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2;
+  char *field = (argc % 2 ? (char *)&a1.y : (char *)&a2.z) + 1;
+  *field = (char)argc;
+  assert(a1.y == argc);
+  assert(a2.z == argc);
+}

regression/cbmc/field-sensitivity10/test.desc

@@ -0,0 +1,15 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.y =
+main::1::a2!0@1#2\.\.z =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a[12]!\d+@\d+#\d+\.[xyz]
+--
+Fields A::y and A::z should be referred to as atomic symbols (a[12]..y and a[12]..z) but not using
+member operators (a[12].[xyz]).
+While the field is aliased with a different type, the typecast is successfully reduced to address just
+one field, rather than using a byte-update operation against the whole structure.
+This is like field-sensitivity8 except the pointer leads into the middle of a field.

regression/cbmc/field-sensitivity11/test.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2;
+  a1.x = argc;
+  a1.y = argc + 1;
+  a2 = a1;
+  assert(a2.x == argc);
+}

regression/cbmc/field-sensitivity11/test.desc

@@ -0,0 +1,15 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.x = main::argc!0@1#1
+main::1::a1!0@1#2\.\.y = 1 \+ main::argc!0@1#1
+main::1::a2!0@1#2\.\.x = main::1::a1!0@1#2\.\.x
+main::1::a2!0@1#2\.\.y = main::1::a1!0@1#2\.\.y
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a[12]!\d+@\d+#\d+\.[xy]
+--
+Fields A::x and A::y should be referred to as atomic symbols (a[12]..x and a[12]..y) but not using
+member operators (a[12].x and a[12].y).
+This test looks at the particular case of whole-struct assignment.

regression/cbmc/field-sensitivity12/test.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A a1, a2;
+  a1.x = argc;
+  a1.y = argc + 1;
+  struct A *aptr = argc % 2 ? &a1 : &a2;
+  *aptr = a1;
+  assert(a2.x == argc);
+}

regression/cbmc/field-sensitivity12/test.desc

@@ -0,0 +1,18 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.x = main::argc!0@1#1
+main::1::a1!0@1#2\.\.y = 1 \+ main::argc!0@1#1
+main::1::a1!0@1#3\.\.x = main::1::a1!0@1#2\.\.x
+main::1::a1!0@1#3\.\.y = main::1::a1!0@1#2\.\.y
+main::1::a2!0@1#2\.\.x =
+main::1::a2!0@1#2\.\.y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::a[12]!\d+@\d+#\d+\.[xy]
+--
+Fields A::x and A::y should be referred to as atomic symbols (a[12]..x and a[12]..y) but not using
+member operators (a[12].x and a[12].y).
+This test looks at the particular case of whole-struct assignment when the target of the assignment
+is uncertain due to pointer indirection.

regression/cbmc/field-sensitivity13/test.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+struct B
+{
+  struct A a;
+  int z;
+};
+
+int main(int argc, char **argv)
+{
+  struct B b1, b2;
+  b1.a.x = argc;
+  b1.a.y = argc + 1;
+  struct A *aptr = argc % 2 ? &b1.a : &b2.a;
+  *aptr = b1.a;
+  assert(b2.a.x == argc);
+}

regression/cbmc/field-sensitivity13/test.desc

@@ -0,0 +1,18 @@
+CORE
+test.c
+--show-vcc
+main::1::b1!0@1#2\.\.a\.\.x = main::argc!0@1#1
+main::1::b1!0@1#2\.\.a\.\.y = 1 \+ main::argc!0@1#1
+main::1::b1!0@1#3\.\.a\.\.x = main::1::b1!0@1#2\.\.a\.\.x
+main::1::b1!0@1#3\.\.a\.\.y = main::1::b1!0@1#2\.\.a\.\.y
+main::1::b2!0@1#2\.\.a\.\.x =
+main::1::b2!0@1#2\.\.a\.\.y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::b[12]!\d+@\d+#\d+\.a
+--
+Fields A::x and A::y should be referred to as atomic symbols (b[12]..a..x and b[12]..a..y) but not using
+member operators (b[12].a.x and b[12].a.y).
+This test looks at the particular case of whole-struct assignment when the target of the assignment
+is uncertain due to pointer indirection.