Byte-operator lowering: use lambda_exprt for non-constant width

Arrays with non-constant size are now encoded using lambda expressions.
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