Add field-sensitivity tests

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.

regression/cbmc/field-sensitivity2/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;
+  struct A *aptr = argc % 2 ? &a1 : &a2;
+  aptr->x = argc;
+  aptr->y = argc + 1;
+  assert(a1.x == argc);
+  assert(a2.x == argc);
+}

regression/cbmc/field-sensitivity2/test.desc

@@ -0,0 +1,14 @@
+CORE
+test.c
+--show-vcc
+main::1::a1!0@1#2\.\.x =
+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).

regression/cbmc/field-sensitivity3/test.c

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

regression/cbmc/field-sensitivity3/test.desc

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

regression/cbmc/field-sensitivity4/test.c

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

regression/cbmc/field-sensitivity4/test.desc

@@ -0,0 +1,16 @@
+FUTURE
+test.c
+--show-vcc
+main::1::a!0@1#2\.\.x =
+main::1::a!0@1#2\.\.y =
+^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).
+Currently this generates a byte_update operation followed by field expansion; could be improved
+if value_sett kept track of a finite set of constant offsets rather than degrading to unknown-offset
+whenever multiple offsets into the same allocation are merged.

regression/cbmc/field-sensitivity5/test.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+struct A
+{
+  int head;
+  struct A *tail;
+};
+
+int main(int argc, char **argv)
+{
+  struct A node1, node2, node3;
+  node1.tail = argc % 2 ? &node2 : &node3;
+  node2.tail = argc % 3 ? &node1 : &node3;
+  node3.tail = argc % 5 ? &node1 : &node2;
+  node1.tail->tail->tail->head = argc;
+  assert(node1.head == argc);
+}

regression/cbmc/field-sensitivity5/test.desc

@@ -0,0 +1,14 @@
+CORE
+test.c
+--show-vcc
+main::1::node1!0@1#2\.\.head =
+main::1::node2!0@1#2\.\.head =
+main::1::node3!0@1#2\.\.head =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::node[123]!\d+@\d+#\d+\.head
+main::1::node[123]!\d+@\d+#\d+\.tail
+--
+Fields A::head and A::tail should be referred to as atomic symbols (node[123]..head and node[123]..tail)
+but not using member operators (node[123].(head)|(tail))

regression/cbmc/field-sensitivity6/test.c

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

regression/cbmc/field-sensitivity6/test.desc

@@ -0,0 +1,13 @@
+CORE
+test.c
+--show-vcc
+main::1::b1!0@1#2\.\.a\.\.x =
+main::1::b2!0@1#2\.\.a\.\.x =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::b1!\d+@\d+#\d+\.a
+main::1::b2!\d+@\d+#\d+\.a
+--
+Field A::x should be referred to as atomic symbols (b[12]..x) but not using
+member operators (b[12].a)

regression/cbmc/field-sensitivity7/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;
+  int *field = argc % 2 ? &a1.y : &a2.z;
+  *field = argc;
+  assert(a1.y == argc);
+  assert(a2.z == argc);
+}

regression/cbmc/field-sensitivity7/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]).
+Note the contrast with field-sensitivity4, where the fields the pointer may address are part of the
+same allocated object resulting in inability to resolve them, contrasting against this test where
+the fields belong to different objects.