Byte-operator lowering: use array comprehensions for non-constant width

Arrays with non-constant size are now encoded using array
comprehensions.  This lifts the prior limit of only being able to
perform byte updates when at least the size of the update or the size of
the target was known.

Author: tautschnig

regression/cbmc-library/memcpy-04/main.c

@@ -0,0 +1,32 @@
+#include <stdlib.h>
+#include <string.h>
+
+typedef struct
+{
+  size_t len;
+  char *name;
+} info_t;
+
+void publish(info_t *info)
+{
+  size_t size;
+  __CPROVER_assume(size >= info->len);
+  unsigned char *buffer = malloc(size);
+  memcpy(buffer, info->name, info->len);
+  if(info->len > 42)
+  {
+    __CPROVER_assert(buffer[42] == 42, "should pass");
+    __CPROVER_assert(buffer[41] == 42, "should fail");
+  }
+}
+
+void main()
+{
+  info_t info;
+  size_t name_len;
+  info.name = malloc(name_len);
+  info.len = name_len;
+  if(name_len > 42)
+    info.name[42] = 42;
+  publish(&info);
+}

regression/cbmc-library/memcpy-04/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^\[publish.assertion.1\] line 18 should pass: SUCCESS$
+^\[publish.assertion.2\] line 19 should fail: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring