Add Duff's device

regression/cbmc/loop-duffs-device/main.c

@@ -0,0 +1,44 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdio.h>
+
+#define ARRAYMAX 256
+
+uint8_t *strndfy (uint8_t *dest, const uint8_t *src, size_t n) {
+  int i = 0;
+  int j = 0;
+
+  switch (n & 0x3) {
+    do {
+      case 0 :   dest[i++] = src[j++];
+      case 1 :   dest[i++] = src[j++];
+      case 2 :   dest[i++] = src[j++];
+      case 3 :   dest[i++] = src[j++];
+    } while (j < n);
+  }
+
+  return dest;
+}
+
+
+int main (int argc, char **argv) {
+  uint8_t src[ARRAYMAX];
+  uint8_t dest[ARRAYMAX];
+
+  int length = 0;  
+  scanf("%u", &length);
+
+  if (length <= ARRAYMAX) {
+    for (int i = 0; i < length; ++i) {
+      src[i] = (uint8_t)i;
+    }
+
+    strndfy(dest, src, length);
+
+    for (int i = 0; i < length; ++i) {
+      assert(dest[i] == (uint8_t)i);
+    }
+  }
+
+  return 0;
+}

regression/cbmc/loop-duffs-device/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--unwind 257
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion 0: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion history == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This checks whether Duff's device is handled correctly.